let G be _Graph; :: thesis: for E1, E2 being RepDEdgeSelection of G ex f being one-to-one Function st
( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds
( e DJoins v,w,G iff f . e DJoins v,w,G ) ) )

let E1, E2 be RepDEdgeSelection of G; :: thesis: ex f being one-to-one Function st
( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds
( e DJoins v,w,G iff f . e DJoins v,w,G ) ) )

defpred S1[ object , object ] means ( \$2 in E2 & ex v, w being object st
( \$1 DJoins v,w,G & \$2 DJoins v,w,G ) );
A1: for x, y1, y2 being object st x in E1 & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( x in E1 & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume A2: ( x in E1 & S1[x,y1] & S1[x,y2] ) ; :: thesis: y1 = y2
then consider v1, w1 being object such that
A3: ( x DJoins v1,w1,G & y1 DJoins v1,w1,G ) ;
consider v2, w2 being object such that
A4: ( x DJoins v2,w2,G & y2 DJoins v2,w2,G ) by A2;
consider e2 being object such that
( e2 DJoins v1,w1,G & e2 in E2 ) and
A5: for e9 being object st e9 DJoins v1,w1,G & e9 in E2 holds
e9 = e2 by ;
A6: y1 = e2 by A2, A3, A5;
( v1 = v2 & w1 = w2 ) by A3, A4, Th6;
hence y1 = y2 by A2, A4, A5, A6; :: thesis: verum
end;
A7: for x being object st x in E1 holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in E1 implies ex y being object st S1[x,y] )
set v = () . x;
set w = () . x;
assume A8: x in E1 ; :: thesis: ex y being object st S1[x,y]
then consider e2 being object such that
A9: ( e2 DJoins () . x,() . x,G & e2 in E2 ) and
for e9 being object st e9 DJoins () . x,() . x,G & e9 in E2 holds
e9 = e2 by ;
take e2 ; :: thesis: S1[x,e2]
thus e2 in E2 by A9; :: thesis: ex v, w being object st
( x DJoins v,w,G & e2 DJoins v,w,G )

take () . x ; :: thesis: ex w being object st
( x DJoins () . x,w,G & e2 DJoins () . x,w,G )

take () . x ; :: thesis: ( x DJoins () . x,() . x,G & e2 DJoins () . x,() . x,G )
thus ( x DJoins () . x,() . x,G & e2 DJoins () . x,() . x,G ) by ; :: thesis: verum
end;
consider f being Function such that
A10: ( dom f = E1 & ( for x being object st x in E1 holds
S1[x,f . x] ) ) from
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A11: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider v1, w1 being object such that
A12: ( x1 DJoins v1,w1,G & f . x1 DJoins v1,w1,G ) by A10;
consider v2, w2 being object such that
A13: ( x2 DJoins v2,w2,G & f . x2 DJoins v2,w2,G ) by ;
consider e1 being object such that
( e1 DJoins v1,w1,G & e1 in E1 ) and
A14: for e9 being object st e9 DJoins v1,w1,G & e9 in E1 holds
e9 = e1 by ;
A15: x1 = e1 by A10, A11, A12, A14;
( v1 = v2 & w1 = w2 ) by A11, A12, A13, Th6;
hence x1 = x2 by A10, A11, A13, A14, A15; :: thesis: verum
end;
then reconsider f = f as one-to-one Function by FUNCT_1:def 4;
take f ; :: thesis: ( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds
( e DJoins v,w,G iff f . e DJoins v,w,G ) ) )

thus dom f = E1 by A10; :: thesis: ( rng f = E2 & ( for e, v, w being object st e in E1 holds
( e DJoins v,w,G iff f . e DJoins v,w,G ) ) )

now :: thesis: for y being object holds
( ( y in rng f implies y in E2 ) & ( y in E2 implies y in rng f ) )
let y be object ; :: thesis: ( ( y in rng f implies y in E2 ) & ( y in E2 implies y in rng f ) )
hereby :: thesis: ( y in E2 implies y in rng f )
assume y in rng f ; :: thesis: y in E2
then consider x being object such that
A16: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
thus y in E2 by ; :: thesis: verum
end;
assume A17: y in E2 ; :: thesis: y in rng f
set v = () . y;
set w = () . y;
consider e1 being object such that
A18: ( e1 DJoins () . y,() . y,G & e1 in E1 ) and
for e9 being object st e9 DJoins () . y,() . y,G & e9 in E1 holds
e9 = e1 by ;
consider e2 being object such that
( e2 DJoins () . y,() . y,G & e2 in E2 ) and
A19: for e9 being object st e9 DJoins () . y,() . y,G & e9 in E2 holds
e9 = e2 by ;
consider v0, w0 being object such that
A20: ( e1 DJoins v0,w0,G & f . e1 DJoins v0,w0,G ) by ;
( v0 = () . y & w0 = () . y ) by ;
then A21: f . e1 = e2 by A10, A18, A19, A20;
y DJoins () . y,() . y,G by ;
then y = e2 by ;
hence y in rng f by ; :: thesis: verum
end;
hence rng f = E2 by TARSKI:2; :: thesis: for e, v, w being object st e in E1 holds
( e DJoins v,w,G iff f . e DJoins v,w,G )

let e, v, w be object ; :: thesis: ( e in E1 implies ( e DJoins v,w,G iff f . e DJoins v,w,G ) )
assume e in E1 ; :: thesis: ( e DJoins v,w,G iff f . e DJoins v,w,G )
then consider v0, w0 being object such that
A22: ( e DJoins v0,w0,G & f . e DJoins v0,w0,G ) by A10;
hereby :: thesis: ( f . e DJoins v,w,G implies e DJoins v,w,G )
assume e DJoins v,w,G ; :: thesis: f . e DJoins v,w,G
then ( v0 = v & w0 = w ) by ;
hence f . e DJoins v,w,G by A22; :: thesis: verum
end;
assume f . e DJoins v,w,G ; :: thesis: e DJoins v,w,G
then ( v0 = v & w0 = w ) by ;
hence e DJoins v,w,G by A22; :: thesis: verum