let G3, G4 be _Graph; :: thesis: for v1, v3 being Vertex of G3
for v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
let v1, v3 be Vertex of G3; :: thesis: for v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
let v2, v4 be Vertex of G4; :: thesis: for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
let e1, e2 be object ; :: thesis: for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
let G1 be addEdge of G3,v1,e1,v3; :: thesis: for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
let G2 be addEdge of G4,v2,e2,v4; :: thesis: for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
let F0 be PGraphMapping of G3,G4; :: thesis: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 implies ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) ) )
assume that
A1: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 ) and
A2: ( v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) ; :: thesis: ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
consider F being PGraphMapping of G1,G2 such that
A3: F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] and
A4: ( F0 is total implies F is total ) and
A5: ( F0 is onto implies F is onto ) and
A6: ( F0 is one-to-one implies F is one-to-one ) by A1, A2, Th152;
take F ; :: thesis: ( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
thus F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] by A3; :: thesis: ( ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
set f = F _V ;
set g = F _E ;
A7: dom (F _E) = (dom (F0 _E)) \/ (dom (e1 .--> e2)) by A3, FUNCT_4:def 1
.= (dom (F0 _E)) \/ (dom ({e1} --> e2)) by FUNCOP_1:def 9
.= (dom (F0 _E)) \/ {e1} ;
not e1 in dom (F0 _E) by A1;
then dom (F0 _E) misses {e1} by ZFMISC_1:50;
then dom (F0 _E) misses dom ({e1} --> e2) ;
then A8: dom (F0 _E) misses dom (e1 .--> e2) by FUNCOP_1:def 9;
A9: (dom (F _E)) /\ (the_Edges_of G3) = ((dom (F0 _E)) /\ (the_Edges_of G3)) \/ ({e1} /\ (the_Edges_of G3)) by A7, XBOOLE_1:23
.= (dom (F0 _E)) \/ ({e1} /\ (the_Edges_of G3)) by XBOOLE_1:28
.= (dom (F0 _E)) \/ {} by A1, ZFMISC_1:50, XBOOLE_0:def 7 ;
thus ( F0 is directed implies F is directed ) :: thesis: ( F0 is Disomorphism implies F is Disomorphism )

proof

assume A10: F0 is directed ; :: thesis: F is directed

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

let e, v, w be object ; :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 implies (F _E) . b₁ DJoins (F _V) . b₂,(F _V) . b₃,G2 )
assume A11: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( e DJoins v,w,G1 implies (F _E) . b₁ DJoins (F _V) . b₂,(F _V) . b₃,G2 )
assume A12: e DJoins v,w,G1 ; :: thesis: (F _E) . b₁ DJoins (F _V) . b₂,(F _V) . b₃,G2
then A13: e Joins v,w,G1 by GLIB_000:16;

per cases ( e DJoins v,w,G3 or not e in the_Edges_of G3 ) by A12, GLIB_006:71;

suppose A14: e DJoins v,w,G3 ; :: thesis: (F _E) . b₁ DJoins (F _V) . b₂,(F _V) . b₃,G2

then e in the_Edges_of G3 by GLIB_000:def 14;
then A15: e in dom (F0 _E) by A9, A11, XBOOLE_0:def 4;
not e in dom (e1 .--> e2)

proof

assume e in dom (e1 .--> e2) ; :: thesis: contradiction
then e in (dom (F0 _E)) /\ (dom (e1 .--> e2)) by A15, XBOOLE_0:def 4;
hence contradiction by A8, XBOOLE_0:def 7; :: thesis: verum

end;

then A16: (F _E) . e = (F0 _E) . e by A3, FUNCT_4:11;
( v in dom (F0 _V) & w in dom (F0 _V) ) by A3, A11;
then (F _E) . e DJoins (F _V) . v,(F _V) . w,G4 by A3, A10, A14, A15, A16;
hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by GLIB_006:70; :: thesis: verum

end;

suppose not e in the_Edges_of G3 ; :: thesis: (F _E) . b₁ DJoins (F _V) . b₂,(F _V) . b₃,G2

then A17: e = e1 by A1, A13, GLIB_006:106;
then e in {e1} by TARSKI:def 1;
then e in dom ({e1} --> e2) ;
then A18: e in dom (e1 .--> e2) by FUNCOP_1:def 9;
A19: e2 = (e1 .--> e2) . e by A17, FUNCOP_1:72
.= (F _E) . e by A18, A3, FUNCT_4:13 ;
e2 DJoins v2,v4,G2 by A1, GLIB_006:105;
then A20: (F _E) . e DJoins (F0 _V) . v1,(F0 _V) . v3,G2 by A2, A19;
e DJoins v1,v3,G1 by A1, A17, GLIB_006:105;
then ( v1 = v & v3 = w ) by A12, GLIB_000:125;
hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A3, A20; :: thesis: verum

end;

end;

end;

hence F is directed ; :: thesis: verum

end;

hence ( F0 is Disomorphism implies F is Disomorphism ) by A4, A5, A6; :: thesis: verum