let G be _Graph; 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; 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 ;
( x in E1 & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume A2:
(
x in E1 &
S1[
x,
y1] &
S1[
x,
y2] )
;
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 A3, Def6;
A6:
y1 = e2
by A2, A3, A5;
(
v1 = v2 &
w1 = w2 )
by A3, A4, Th6;
hence
y1 = y2
by A2, A4, A5, A6;
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 ;
( x in E1 implies ex y being object st S1[x,y] )
set v =
(the_Source_of G) . x;
set w =
(the_Target_of G) . x;
assume A8:
x in E1
;
ex y being object st S1[x,y]
then consider e2 being
object such that A9:
(
e2 DJoins (the_Source_of G) . x,
(the_Target_of G) . x,
G &
e2 in E2 )
and
for
e9 being
object st
e9 DJoins (the_Source_of G) . x,
(the_Target_of G) . x,
G &
e9 in E2 holds
e9 = e2
by Def6, GLIB_000:def 14;
take
e2
;
S1[x,e2]
thus
e2 in E2
by A9;
ex v, w being object st
( x DJoins v,w,G & e2 DJoins v,w,G )
take
(the_Source_of G) . x
;
ex w being object st
( x DJoins (the_Source_of G) . x,w,G & e2 DJoins (the_Source_of G) . x,w,G )
take
(the_Target_of G) . x
;
( x DJoins (the_Source_of G) . x,(the_Target_of G) . x,G & e2 DJoins (the_Source_of G) . x,(the_Target_of G) . x,G )
thus
(
x DJoins (the_Source_of G) . x,
(the_Target_of G) . x,
G &
e2 DJoins (the_Source_of G) . x,
(the_Target_of G) . x,
G )
by A8, A9, GLIB_000:def 14;
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 FUNCT_1:sch 2(A1, A7);
now for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( 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 )
;
x1 = x2then 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 A10, A11;
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 A12, Def6;
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;
verum end;
then reconsider f = f as one-to-one Function by FUNCT_1:def 4;
take
f
; ( 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; ( 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 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 ;
( ( y in rng f implies y in E2 ) & ( y in E2 implies y in rng f ) )hereby ( y in E2 implies y in rng f )
end; assume A17:
y in E2
;
y in rng fset v =
(the_Source_of G) . y;
set w =
(the_Target_of G) . y;
consider e1 being
object such that A18:
(
e1 DJoins (the_Source_of G) . y,
(the_Target_of G) . y,
G &
e1 in E1 )
and
for
e9 being
object st
e9 DJoins (the_Source_of G) . y,
(the_Target_of G) . y,
G &
e9 in E1 holds
e9 = e1
by A17, Def6, GLIB_000:def 14;
consider e2 being
object such that
(
e2 DJoins (the_Source_of G) . y,
(the_Target_of G) . y,
G &
e2 in E2 )
and A19:
for
e9 being
object st
e9 DJoins (the_Source_of G) . y,
(the_Target_of G) . y,
G &
e9 in E2 holds
e9 = e2
by A17, Def6, GLIB_000:def 14;
consider v0,
w0 being
object such that A20:
(
e1 DJoins v0,
w0,
G &
f . e1 DJoins v0,
w0,
G )
by A10, A18;
(
v0 = (the_Source_of G) . y &
w0 = (the_Target_of G) . y )
by A18, A20, Th6;
then A21:
f . e1 = e2
by A10, A18, A19, A20;
y DJoins (the_Source_of G) . y,
(the_Target_of G) . y,
G
by A17, GLIB_000:def 14;
then
y = e2
by A17, A19;
hence
y in rng f
by A10, A18, A21, FUNCT_1:3;
verum end;
hence
rng f = E2
by TARSKI:2; 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 ; ( e in E1 implies ( e DJoins v,w,G iff f . e DJoins v,w,G ) )
assume
e in E1
; ( 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;
assume
f . e DJoins v,w,G
; e DJoins v,w,G
then
( v0 = v & w0 = w )
by A22, Th6;
hence
e DJoins v,w,G
by A22; verum