let G3, G4 be _Graph; :: thesis: for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let v3 be Vertex of G3; :: thesis: for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let v4 be Vertex of G4; :: thesis: for e1, e2, v1, v2 being object
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let e1, e2, v1, v2 be object ; :: thesis: for G1 being addAdjVertex of G3,v3,e1,v1
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let G2 be addAdjVertex of G4,v4,e2,v2; :: thesis: for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 implies ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) ) )

assume that
A1: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 ) and
A2: ( v3 in dom (F0 _V) & (F0 _V) . v3 = v4 ) ; :: thesis: ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

consider G5 being addVertex of G3,v1 such that
A3: G1 is addEdge of G5,v3,e1,v1 by ;
consider G6 being addVertex of G4,v2 such that
A4: G2 is addEdge of G6,v4,e2,v2 by ;
consider F1 being PGraphMapping of G5,G6 such that
A5: F1 = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] and
A6: ( F0 is total implies F1 is total ) and
A7: ( F0 is onto implies F1 is onto ) and
A8: ( F0 is one-to-one implies F1 is one-to-one ) and
A9: ( F0 is directed implies F1 is directed ) and
( F0 is semi-continuous implies F1 is semi-continuous ) and
( F0 is continuous implies F1 is continuous ) and
( F0 is semi-Dcontinuous implies F1 is semi-Dcontinuous ) and
( F0 is Dcontinuous implies F1 is Dcontinuous ) by ;
A10: ( v1 in dom (F1 _V) & v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )
proof
v1 in {v1} by TARSKI:def 1;
then v1 in dom ({v1} --> v2) ;
then A11: v1 in dom (v1 .--> v2) by FUNCOP_1:def 9;
hence v1 in dom (F1 _V) by ; :: thesis: ( v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )
thus v3 in dom (F1 _V) by ; :: thesis: ( (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )
thus (F1 _V) . v1 = (v1 .--> v2) . v1 by
.= v2 by FUNCOP_1:72 ; :: thesis: (F1 _V) . v3 = v4
v3 <> v1 by A1;
then not v3 in {v1} by TARSKI:def 1;
then not v3 in dom (v1 .--> v2) ;
hence (F1 _V) . v3 = v4 by ; :: thesis: verum
end;
A12: ( not e1 in the_Edges_of G5 & not e2 in the_Edges_of G6 ) by ;
( v2 in rng (F1 _V) & v4 in rng (F1 _V) ) by ;
then A13: ( v2 is Vertex of G6 & v4 is Vertex of G6 ) ;
then consider F2 being PGraphMapping of G1,G2 such that
A14: F2 = [(F1 _V),((F1 _E) +* (e1 .--> e2))] and
A15: ( F1 is total implies F2 is total ) and
A16: ( F1 is onto implies F2 is onto ) and
A17: ( F1 is one-to-one implies F2 is one-to-one ) by A3, A4, A10, A12, Th152;
take F2 ; :: thesis: ( F2 = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F2 is total ) & ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )
thus F2 = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] by ; :: thesis: ( ( F0 is total implies F2 is total ) & ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )
thus ( F0 is total implies F2 is total ) by ; :: thesis: ( ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )
thus ( F0 is onto implies F2 is onto ) by ; :: thesis: ( ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )
thus ( F0 is one-to-one implies F2 is one-to-one ) by ; :: thesis: ( F0 is directed implies F2 is directed )
consider F3 being PGraphMapping of G1,G2 such that
A18: F3 = [(F1 _V),((F1 _E) +* (e1 .--> e2))] and
A19: ( F1 is directed implies F3 is directed ) and
( F1 is Disomorphism implies F3 is Disomorphism ) by A3, A4, A10, A12, A13, Th154;
thus ( F0 is directed implies F2 is directed ) by A9, A14, A18, A19; :: thesis: verum