let G3, G4 be _Graph; for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex 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 & 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let v3 be Vertex of G3; for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex 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 & 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let v4 be Vertex of G4; for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex 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 & 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let e1, e2, v1, v2 be object ; for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex 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 & 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let G1 be addAdjVertex of G3,v3,e1,v1; for G2 being addAdjVertex 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 & 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let G2 be addAdjVertex 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 & 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let F0 be PGraphMapping of G3,G4; ( 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) )
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 )
; 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 weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
consider G5 being addVertex of G3,v1 such that
A3:
G1 is addEdge of G5,v3,e1,v1
by A1, GLIB_006:125;
consider G6 being addVertex of G4,v2 such that
A4:
G2 is addEdge of G6,v2,e2,v4
by A1, GLIB_006:126;
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
( 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 A1, Th148;
A9:
( v1 in dom (F1 _V) & v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )
A11:
( not e1 in the_Edges_of G5 & not e2 in the_Edges_of G6 )
by A1, GLIB_006:def 10;
( v2 in rng (F1 _V) & v4 in rng (F1 _V) )
by A9, FUNCT_1:3;
then
( v2 is Vertex of G6 & v4 is Vertex of G6 )
;
then consider F2 being PGraphMapping of G1,G2 such that
A12:
F2 = [(F1 _V),((F1 _E) +* (e1 .--> e2))]
and
A13:
( F1 is total implies F2 is total )
and
A14:
( F1 is onto implies F2 is onto )
and
A15:
( F1 is one-to-one implies F2 is one-to-one )
by A3, A4, A9, A11, Th152;
take
F2
; ( 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 weak_SG-embedding implies F2 is weak_SG-embedding ) & ( F0 is isomorphism implies F2 is isomorphism ) )
thus
F2 = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))]
by A5, A12; ( ( 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 weak_SG-embedding implies F2 is weak_SG-embedding ) & ( F0 is isomorphism implies F2 is isomorphism ) )
thus A16:
( F0 is total implies F2 is total )
by A6, A13; ( ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is weak_SG-embedding implies F2 is weak_SG-embedding ) & ( F0 is isomorphism implies F2 is isomorphism ) )
thus A17:
( F0 is onto implies F2 is onto )
by A7, A14; ( ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is weak_SG-embedding implies F2 is weak_SG-embedding ) & ( F0 is isomorphism implies F2 is isomorphism ) )
thus A18:
( F0 is one-to-one implies F2 is one-to-one )
by A8, A15; ( ( F0 is weak_SG-embedding implies F2 is weak_SG-embedding ) & ( F0 is isomorphism implies F2 is isomorphism ) )
thus
( F0 is weak_SG-embedding implies F2 is weak_SG-embedding )
by A16, A18; ( F0 is isomorphism implies F2 is isomorphism )
thus
( F0 is isomorphism implies F2 is isomorphism )
by A16, A17, A18; verum