let G1 be _Graph; :: thesis: for G2 being G1 -Disomorphic _Graph

for G3 being b_{1} -Disomorphic _Graph

for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

let G2 be G1 -Disomorphic _Graph; :: thesis: for G3 being G2 -Disomorphic _Graph

for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

let G3 be G2 -Disomorphic _Graph; :: thesis: for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

let F be DIsomorphism of G1,G2; :: thesis: ( G1 == G3 implies F " is DIsomorphism of G2,G3 )

assume A1: G1 == G3 ; :: thesis: F " is DIsomorphism of G2,G3

then reconsider F2 = F " as PGraphMapping of G2,G3 by Th9;

A2: F2 is total

hence F " is DIsomorphism of G2,G3 by A2, A3, A4; :: thesis: verum

for G3 being b

for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

let G2 be G1 -Disomorphic _Graph; :: thesis: for G3 being G2 -Disomorphic _Graph

for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

let G3 be G2 -Disomorphic _Graph; :: thesis: for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

let F be DIsomorphism of G1,G2; :: thesis: ( G1 == G3 implies F " is DIsomorphism of G2,G3 )

assume A1: G1 == G3 ; :: thesis: F " is DIsomorphism of G2,G3

then reconsider F2 = F " as PGraphMapping of G2,G3 by Th9;

A2: F2 is total

proof

A3:
F2 is onto
thus dom (F2 _V) =
rng (F _V)
by FUNCT_1:33

.= the_Vertices_of G2 by Def12 ; :: according to GLIB_010:def 11 :: thesis: dom (F2 _E) = the_Edges_of G2

thus dom (F2 _E) = rng (F _E) by FUNCT_1:33

.= the_Edges_of G2 by Def12 ; :: thesis: verum

end;.= the_Vertices_of G2 by Def12 ; :: according to GLIB_010:def 11 :: thesis: dom (F2 _E) = the_Edges_of G2

thus dom (F2 _E) = rng (F _E) by FUNCT_1:33

.= the_Edges_of G2 by Def12 ; :: thesis: verum

proof

A4:
F2 is one-to-one
;
thus rng (F2 _V) =
dom (F _V)
by FUNCT_1:33

.= the_Vertices_of G1 by Def11

.= the_Vertices_of G3 by A1, GLIB_000:def 34 ; :: according to GLIB_010:def 12 :: thesis: rng (F2 _E) = the_Edges_of G3

thus rng (F2 _E) = dom (F _E) by FUNCT_1:33

.= the_Edges_of G1 by Def11

.= the_Edges_of G3 by A1, GLIB_000:def 34 ; :: thesis: verum

end;.= the_Vertices_of G1 by Def11

.= the_Vertices_of G3 by A1, GLIB_000:def 34 ; :: according to GLIB_010:def 12 :: thesis: rng (F2 _E) = the_Edges_of G3

thus rng (F2 _E) = dom (F _E) by FUNCT_1:33

.= the_Edges_of G1 by Def11

.= the_Edges_of G3 by A1, GLIB_000:def 34 ; :: thesis: verum

now :: thesis: for e, v, w being object st e in dom (F2 _E) & v in dom (F2 _V) & w in dom (F2 _V) & e DJoins v,w,G2 holds

((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3

then
F2 is directed
;((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3

let e, v, w be object ; :: thesis: ( e in dom (F2 _E) & v in dom (F2 _V) & w in dom (F2 _V) & e DJoins v,w,G2 implies ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3 )

assume ( e in dom (F2 _E) & v in dom (F2 _V) & w in dom (F2 _V) ) ; :: thesis: ( e DJoins v,w,G2 implies ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3 )

then A5: ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) ) ;

assume e DJoins v,w,G2 ; :: thesis: ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3

then ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 by A5, Def14;

hence ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3 by A1, GLIB_000:88; :: thesis: verum

end;assume ( e in dom (F2 _E) & v in dom (F2 _V) & w in dom (F2 _V) ) ; :: thesis: ( e DJoins v,w,G2 implies ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3 )

then A5: ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) ) ;

assume e DJoins v,w,G2 ; :: thesis: ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3

then ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 by A5, Def14;

hence ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3 by A1, GLIB_000:88; :: thesis: verum

hence F " is DIsomorphism of G2,G3 by A2, A3, A4; :: thesis: verum