let G1 be _Graph; for G2 being G1 -Disomorphic _Graph
for G3 being b1 -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; 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; for F being DIsomorphism of G1,G2 st G1 == G3 holds
F " is DIsomorphism of G2,G3
let F be DIsomorphism of G1,G2; ( G1 == G3 implies F " is DIsomorphism of G2,G3 )
assume A1:
G1 == G3
; F " is DIsomorphism of G2,G3
then reconsider F2 = F " as PGraphMapping of G2,G3 by Th9;
A2:
F2 is total
A3:
F2 is onto
A4:
F2 is one-to-one
;
now 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,G3let e,
v,
w be
object ;
( 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) )
;
( 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
;
((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G3then
((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;
verum end;
then
F2 is directed
;
hence
F " is DIsomorphism of G2,G3
by A2, A3, A4; verum