let G1 be _Graph; :: thesis: for G2 being G1 -Disomorphic _Graph
for G3 being b₁ -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

proof

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;

A3: F2 is onto

proof

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;

A4: F2 is one-to-one ;

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

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;

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