let G be _Graph; :: thesis: for E1, E2 being RepEdgeSelection 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 Joins v,w,G iff f . e Joins v,w,G ) ) )

let E1, E2 be RepEdgeSelection 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 Joins v,w,G iff f . e Joins v,w,G ) ) )

defpred S_{1}[ object , object ] means ( $2 in E2 & ex v, w being object st

( $1 Joins v,w,G & $2 Joins v,w,G ) );

A1: for x, y1, y2 being object st x in E1 & S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2

ex y being object st S_{1}[x,y]

A10: ( dom f = E1 & ( for x being object st x in E1 holds

S_{1}[x,f . x] ) )
from FUNCT_1:sch 2(A1, A7);

take f ; :: thesis: ( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds

( e Joins v,w,G iff f . e Joins 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 Joins v,w,G iff f . e Joins v,w,G ) ) )

( e Joins v,w,G iff f . e Joins v,w,G )

let e, v, w be object ; :: thesis: ( e in E1 implies ( e Joins v,w,G iff f . e Joins v,w,G ) )

assume e in E1 ; :: thesis: ( e Joins v,w,G iff f . e Joins v,w,G )

then consider v0, w0 being object such that

A23: ( e Joins v0,w0,G & f . e Joins v0,w0,G ) by A10;

then ( ( v0 = v & w0 = w ) or ( v0 = w & w0 = v ) ) by A23, GLIB_000:15;

hence e Joins v,w,G by A23, GLIB_000:14; :: thesis: verum

( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds

( e Joins v,w,G iff f . e Joins v,w,G ) ) )

let E1, E2 be RepEdgeSelection 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 Joins v,w,G iff f . e Joins v,w,G ) ) )

defpred S

( $1 Joins v,w,G & $2 Joins v,w,G ) );

A1: for x, y1, y2 being object st x in E1 & S

y1 = y2

proof

A7:
for x being object st x in E1 holds
let x, y1, y2 be object ; :: thesis: ( x in E1 & S_{1}[x,y1] & S_{1}[x,y2] implies y1 = y2 )

assume A2: ( x in E1 & S_{1}[x,y1] & S_{1}[x,y2] )
; :: thesis: y1 = y2

then consider v1, w1 being object such that

A3: ( x Joins v1,w1,G & y1 Joins v1,w1,G ) ;

consider v2, w2 being object such that

A4: ( x Joins v2,w2,G & y2 Joins v2,w2,G ) by A2;

consider e2 being object such that

( e2 Joins v1,w1,G & e2 in E2 ) and

A5: for e9 being object st e9 Joins v1,w1,G & e9 in E2 holds

e9 = e2 by A3, Def5;

A6: y1 = e2 by A2, A3, A5;

( ( v1 = v2 & w1 = w2 ) or ( v1 = w2 & w1 = v2 ) ) by A3, A4, GLIB_000:15;

hence y1 = y2 by A2, A4, A5, A6, GLIB_000:14; :: thesis: verum

end;assume A2: ( x in E1 & S

then consider v1, w1 being object such that

A3: ( x Joins v1,w1,G & y1 Joins v1,w1,G ) ;

consider v2, w2 being object such that

A4: ( x Joins v2,w2,G & y2 Joins v2,w2,G ) by A2;

consider e2 being object such that

( e2 Joins v1,w1,G & e2 in E2 ) and

A5: for e9 being object st e9 Joins v1,w1,G & e9 in E2 holds

e9 = e2 by A3, Def5;

A6: y1 = e2 by A2, A3, A5;

( ( v1 = v2 & w1 = w2 ) or ( v1 = w2 & w1 = v2 ) ) by A3, A4, GLIB_000:15;

hence y1 = y2 by A2, A4, A5, A6, GLIB_000:14; :: thesis: verum

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in E1 implies ex y being object st S_{1}[x,y] )

set v = (the_Source_of G) . x;

set w = (the_Target_of G) . x;

assume x in E1 ; :: thesis: ex y being object st S_{1}[x,y]

then A8: x Joins (the_Source_of G) . x,(the_Target_of G) . x,G by GLIB_000:def 13;

then consider e2 being object such that

A9: ( e2 Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e2 in E2 ) and

for e9 being object st e9 Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e9 in E2 holds

e9 = e2 by Def5;

take e2 ; :: thesis: S_{1}[x,e2]

thus e2 in E2 by A9; :: thesis: ex v, w being object st

( x Joins v,w,G & e2 Joins v,w,G )

take (the_Source_of G) . x ; :: thesis: ex w being object st

( x Joins (the_Source_of G) . x,w,G & e2 Joins (the_Source_of G) . x,w,G )

take (the_Target_of G) . x ; :: thesis: ( x Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e2 Joins (the_Source_of G) . x,(the_Target_of G) . x,G )

thus ( x Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e2 Joins (the_Source_of G) . x,(the_Target_of G) . x,G ) by A8, A9; :: thesis: verum

end;set v = (the_Source_of G) . x;

set w = (the_Target_of G) . x;

assume x in E1 ; :: thesis: ex y being object st S

then A8: x Joins (the_Source_of G) . x,(the_Target_of G) . x,G by GLIB_000:def 13;

then consider e2 being object such that

A9: ( e2 Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e2 in E2 ) and

for e9 being object st e9 Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e9 in E2 holds

e9 = e2 by Def5;

take e2 ; :: thesis: S

thus e2 in E2 by A9; :: thesis: ex v, w being object st

( x Joins v,w,G & e2 Joins v,w,G )

take (the_Source_of G) . x ; :: thesis: ex w being object st

( x Joins (the_Source_of G) . x,w,G & e2 Joins (the_Source_of G) . x,w,G )

take (the_Target_of G) . x ; :: thesis: ( x Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e2 Joins (the_Source_of G) . x,(the_Target_of G) . x,G )

thus ( x Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e2 Joins (the_Source_of G) . x,(the_Target_of G) . x,G ) by A8, A9; :: thesis: verum

A10: ( dom f = E1 & ( for x being object st x in E1 holds

S

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

then reconsider f = f as one-to-one Function by FUNCT_1:def 4;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 Joins v1,w1,G & f . x1 Joins v1,w1,G ) by A10;

consider v2, w2 being object such that

A13: ( x2 Joins v2,w2,G & f . x2 Joins v2,w2,G ) by A10, A11;

consider e1 being object such that

( e1 Joins v1,w1,G & e1 in E1 ) and

A14: for e9 being object st e9 Joins v1,w1,G & e9 in E1 holds

e9 = e1 by A12, Def5;

A15: x1 = e1 by A10, A11, A12, A14;

( ( v1 = v2 & w1 = w2 ) or ( v1 = w2 & w1 = v2 ) ) by A11, A12, A13, GLIB_000:15;

hence x1 = x2 by A10, A11, A13, A14, A15, GLIB_000:14; :: thesis: verum

end;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 Joins v1,w1,G & f . x1 Joins v1,w1,G ) by A10;

consider v2, w2 being object such that

A13: ( x2 Joins v2,w2,G & f . x2 Joins v2,w2,G ) by A10, A11;

consider e1 being object such that

( e1 Joins v1,w1,G & e1 in E1 ) and

A14: for e9 being object st e9 Joins v1,w1,G & e9 in E1 holds

e9 = e1 by A12, Def5;

A15: x1 = e1 by A10, A11, A12, A14;

( ( v1 = v2 & w1 = w2 ) or ( v1 = w2 & w1 = v2 ) ) by A11, A12, A13, GLIB_000:15;

hence x1 = x2 by A10, A11, A13, A14, A15, GLIB_000:14; :: thesis: verum

take f ; :: thesis: ( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds

( e Joins v,w,G iff f . e Joins 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 Joins v,w,G iff f . e Joins 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 ) )

hence
rng f = E2
by TARSKI:2; :: thesis: for e, v, w being object st e in E1 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 ) )

set v = (the_Source_of G) . y;

set w = (the_Target_of G) . y;

A18: y Joins (the_Source_of G) . y,(the_Target_of G) . y,G by A17, GLIB_000:def 13;

then consider e1 being object such that

A19: ( e1 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e1 in E1 ) and

for e9 being object st e9 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e9 in E1 holds

e9 = e1 by Def5;

consider e2 being object such that

( e2 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e2 in E2 ) and

A20: for e9 being object st e9 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e9 in E2 holds

e9 = e2 by A18, Def5;

consider v0, w0 being object such that

A21: ( e1 Joins v0,w0,G & f . e1 Joins v0,w0,G ) by A10, A19;

( ( v0 = (the_Source_of G) . y & w0 = (the_Target_of G) . y ) or ( v0 = (the_Target_of G) . y & w0 = (the_Source_of G) . y ) ) by A19, A21, GLIB_000:15;

then f . e1 Joins (the_Source_of G) . y,(the_Target_of G) . y,G by A21, GLIB_000:14;

then A22: f . e1 = e2 by A10, A19, A20;

y = e2 by A17, A18, A20;

hence y in rng f by A10, A19, A22, FUNCT_1:3; :: thesis: verum

end;hereby :: thesis: ( y in E2 implies y in rng f )

assume A17:
y in E2
; :: thesis: y in rng fassume
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 A10, A16; :: thesis: verum

end;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 A10, A16; :: thesis: verum

set v = (the_Source_of G) . y;

set w = (the_Target_of G) . y;

A18: y Joins (the_Source_of G) . y,(the_Target_of G) . y,G by A17, GLIB_000:def 13;

then consider e1 being object such that

A19: ( e1 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e1 in E1 ) and

for e9 being object st e9 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e9 in E1 holds

e9 = e1 by Def5;

consider e2 being object such that

( e2 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e2 in E2 ) and

A20: for e9 being object st e9 Joins (the_Source_of G) . y,(the_Target_of G) . y,G & e9 in E2 holds

e9 = e2 by A18, Def5;

consider v0, w0 being object such that

A21: ( e1 Joins v0,w0,G & f . e1 Joins v0,w0,G ) by A10, A19;

( ( v0 = (the_Source_of G) . y & w0 = (the_Target_of G) . y ) or ( v0 = (the_Target_of G) . y & w0 = (the_Source_of G) . y ) ) by A19, A21, GLIB_000:15;

then f . e1 Joins (the_Source_of G) . y,(the_Target_of G) . y,G by A21, GLIB_000:14;

then A22: f . e1 = e2 by A10, A19, A20;

y = e2 by A17, A18, A20;

hence y in rng f by A10, A19, A22, FUNCT_1:3; :: thesis: verum

( e Joins v,w,G iff f . e Joins v,w,G )

let e, v, w be object ; :: thesis: ( e in E1 implies ( e Joins v,w,G iff f . e Joins v,w,G ) )

assume e in E1 ; :: thesis: ( e Joins v,w,G iff f . e Joins v,w,G )

then consider v0, w0 being object such that

A23: ( e Joins v0,w0,G & f . e Joins v0,w0,G ) by A10;

hereby :: thesis: ( f . e Joins v,w,G implies e Joins v,w,G )

assume
f . e Joins v,w,G
; :: thesis: e Joins v,w,Gassume
e Joins v,w,G
; :: thesis: f . e Joins v,w,G

then ( ( v0 = v & w0 = w ) or ( v0 = w & w0 = v ) ) by A23, GLIB_000:15;

hence f . e Joins v,w,G by A23, GLIB_000:14; :: thesis: verum

end;then ( ( v0 = v & w0 = w ) or ( v0 = w & w0 = v ) ) by A23, GLIB_000:15;

hence f . e Joins v,w,G by A23, GLIB_000:14; :: thesis: verum

then ( ( v0 = v & w0 = w ) or ( v0 = w & w0 = v ) ) by A23, GLIB_000:15;

hence e Joins v,w,G by A23, GLIB_000:14; :: thesis: verum