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 )

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

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

end;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

hence
F is directed
; :: thesis: verum(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_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},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_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},G2 )

assume A12: e DJoins v,w,G1 ; :: thesis: (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},G2

then A13: e Joins v,w,G1 by GLIB_000:16;

end;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

assume A12: e DJoins v,w,G1 ; :: thesis: (F _E) . b

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;

end;

suppose A14:
e DJoins v,w,G3
; :: thesis: (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},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)

( 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;then A15: e in dom (F0 _E) by A9, A11, XBOOLE_0:def 4;

not e in dom (e1 .--> e2)

proof

then A16:
(F _E) . e = (F0 _E) . e
by A3, FUNCT_4:11;
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 e in (dom (F0 _E)) /\ (dom (e1 .--> e2)) by A15, XBOOLE_0:def 4;

hence contradiction by A8, XBOOLE_0:def 7; :: thesis: verum

( 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

suppose
not e in the_Edges_of G3
; :: thesis: (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},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_009:6;

hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A3, A20; :: thesis: verum

end;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_009:6;

hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A3, A20; :: thesis: verum