let G3, G4 be _Graph; :: thesis: for v1, v2 being object

for V1, V2 being set

for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 v1, v2 be object ; :: thesis: for V1, V2 being set

for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 V1, V2 be set ; :: thesis: for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 addAdjVertexAll of G3,v1,V1; :: thesis: for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 addAdjVertexAll of G4,v2,V2; :: thesis: for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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; :: thesis: ( V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 implies ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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: ( V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 ) and

A2: ( (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 ) )

A3: V1 c= dom (F0 _V)

A4: ( v1 is set & v2 is set ) by TARSKI:1;

A5: {v1} = dom ({v1} --> v2)

.= dom (v1 .--> v2) by FUNCOP_1:def 9 ;

A6: dom ((F0 _V) +* (v1 .--> v2)) = (dom (F0 _V)) \/ {v1} by A5, FUNCT_4:def 1;

not v1 in dom (F0 _V) by A1;

then A7: dom (F0 _V) misses dom (v1 .--> v2) by A5, ZFMISC_1:50;

dom ((F0 _V) +* (v1 .--> v2)) c= (the_Vertices_of G3) \/ {v1} by A6, XBOOLE_1:9;

then A8: dom ((F0 _V) +* (v1 .--> v2)) c= the_Vertices_of G1 by A1, GLIB_007:def 4;

not v2 in rng (F0 _V) by A1;

then rng (F0 _V) misses {v2} by ZFMISC_1:50;

then A9: rng (F0 _V) misses rng (v1 .--> v2) by A4, FUNCOP_1:88;

A10: rng ((F0 _V) +* (v1 .--> v2)) = (rng (F0 _V)) \/ (rng (v1 .--> v2)) by A7, NECKLACE:6

.= (rng (F0 _V)) \/ {v2} by A4, FUNCOP_1:88 ;

rng ((F0 _V) +* (v1 .--> v2)) c= (the_Vertices_of G4) \/ {v2} by A10, XBOOLE_1:9;

then rng ((F0 _V) +* (v1 .--> v2)) c= the_Vertices_of G2 by A1, GLIB_007:def 4;

then reconsider f = (F0 _V) +* (v1 .--> v2) as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) by A8, RELSET_1:4;

V1 c= V1 ;

then consider h1 being Function of V1,(G1 .edgesBetween (V1,{v1})) such that

A11: ( h1 is one-to-one & h1 is onto ) and

A12: for w being object st w in V1 holds

h1 . w Joins w,v1,G1 by A1, GLIB_007:57;

V2 c= V2 ;

then consider h2 being Function of V2,(G2 .edgesBetween (V2,{v2})) such that

A13: ( h2 is one-to-one & h2 is onto ) and

A14: for w being object st w in V2 holds

h2 . w Joins w,v2,G2 by A1, GLIB_007:57;

reconsider h1 = h1 as one-to-one Function by A11;

set g = (F0 _E) +* ((h2 * (F0 _V)) * (h1 "));

dom ((h2 * (F0 _V)) * (h1 ")) c= dom (h1 ") by RELAT_1:25;

then (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (dom (h1 ")) by XBOOLE_1:13;

then dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (dom (h1 ")) by FUNCT_4:def 1;

then dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (rng h1) by FUNCT_1:33;

then dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (G1 .edgesBetween (V1,{v1})) by A11, FUNCT_2:def 3;

then A15: dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= the_Edges_of G1 by A1, GLIB_007:59;

A16: rng ((h2 * (F0 _V)) * (h1 ")) c= rng (h2 * (F0 _V)) by RELAT_1:26;

rng (h2 * (F0 _V)) c= rng h2 by RELAT_1:26;

then rng ((h2 * (F0 _V)) * (h1 ")) c= rng h2 by A16, XBOOLE_1:1;

then A17: (rng (F0 _E)) \/ (rng ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G4) \/ (rng h2) by XBOOLE_1:13;

rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (rng (F0 _E)) \/ (rng ((h2 * (F0 _V)) * (h1 "))) by FUNCT_4:17;

then rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G4) \/ (rng h2) by A17, XBOOLE_1:1;

then rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G4) \/ (G2 .edgesBetween (V2,{v2})) by A13, FUNCT_2:def 3;

then rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= the_Edges_of G2 by A1, GLIB_007:59;

then reconsider g = (F0 _E) +* ((h2 * (F0 _V)) * (h1 ")) as PartFunc of (the_Edges_of G1),(the_Edges_of G2) by A15, RELSET_1:4;

A18: ( G1 .edgesBetween (V1,{v1}) misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ (G1 .edgesBetween (V1,{v1})) ) by A1, GLIB_007:59;

A19: dom (F0 _E) misses dom ((h2 * (F0 _V)) * (h1 "))

( card V1 = card E1 & E1 misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ E1 ) and

A25: for w1 being object st w1 in V1 holds

ex e1 being object st

( e1 in E1 & e1 Joins w1,v1,G1 & ( for e9 being object st e9 Joins w1,v1,G1 holds

e1 = e9 ) ) by A1, GLIB_007:def 4;

consider E2 being set such that

( card V2 = card E2 & E2 misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ E2 ) and

A26: for w2 being object st w2 in V2 holds

ex e2 being object st

( e2 in E2 & e2 Joins w2,v2,G2 & ( for e9 being object st e9 Joins w2,v2,G2 holds

e2 = e9 ) ) by A1, GLIB_007:def 4;

take F ; :: thesis: ( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 ) )

thus F _V = (F0 _V) +* (v1 .--> v2) ; :: thesis: ( (F _E) | (dom (F0 _E)) = F0 _E & ( 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 ) )

thus (F _E) | (dom (F0 _E)) = F0 _E by A19, FUNCT_4:33; :: thesis: ( ( 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 ) )

thus A58: ( F0 is total implies F is total ) :: thesis: ( ( 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 ) )

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A58, A122; :: thesis: ( F0 is isomorphism implies F is isomorphism )

thus ( F0 is isomorphism implies F is isomorphism ) by A58, A90, A122; :: thesis: verum

for V1, V2 being set

for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 v1, v2 be object ; :: thesis: for V1, V2 being set

for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 V1, V2 be set ; :: thesis: for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 addAdjVertexAll of G3,v1,V1; :: thesis: for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 addAdjVertexAll of G4,v2,V2; :: thesis: for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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; :: thesis: ( V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 implies ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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: ( V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 ) and

A2: ( (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 ) )

A3: V1 c= dom (F0 _V)

proof

set f = (F0 _V) +* (v1 .--> v2);
V1 = (dom (F0 _V)) /\ V1
by A2, RELAT_1:61;

hence V1 c= dom (F0 _V) by XBOOLE_1:17; :: thesis: verum

end;hence V1 c= dom (F0 _V) by XBOOLE_1:17; :: thesis: verum

A4: ( v1 is set & v2 is set ) by TARSKI:1;

A5: {v1} = dom ({v1} --> v2)

.= dom (v1 .--> v2) by FUNCOP_1:def 9 ;

A6: dom ((F0 _V) +* (v1 .--> v2)) = (dom (F0 _V)) \/ {v1} by A5, FUNCT_4:def 1;

not v1 in dom (F0 _V) by A1;

then A7: dom (F0 _V) misses dom (v1 .--> v2) by A5, ZFMISC_1:50;

dom ((F0 _V) +* (v1 .--> v2)) c= (the_Vertices_of G3) \/ {v1} by A6, XBOOLE_1:9;

then A8: dom ((F0 _V) +* (v1 .--> v2)) c= the_Vertices_of G1 by A1, GLIB_007:def 4;

not v2 in rng (F0 _V) by A1;

then rng (F0 _V) misses {v2} by ZFMISC_1:50;

then A9: rng (F0 _V) misses rng (v1 .--> v2) by A4, FUNCOP_1:88;

A10: rng ((F0 _V) +* (v1 .--> v2)) = (rng (F0 _V)) \/ (rng (v1 .--> v2)) by A7, NECKLACE:6

.= (rng (F0 _V)) \/ {v2} by A4, FUNCOP_1:88 ;

rng ((F0 _V) +* (v1 .--> v2)) c= (the_Vertices_of G4) \/ {v2} by A10, XBOOLE_1:9;

then rng ((F0 _V) +* (v1 .--> v2)) c= the_Vertices_of G2 by A1, GLIB_007:def 4;

then reconsider f = (F0 _V) +* (v1 .--> v2) as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) by A8, RELSET_1:4;

V1 c= V1 ;

then consider h1 being Function of V1,(G1 .edgesBetween (V1,{v1})) such that

A11: ( h1 is one-to-one & h1 is onto ) and

A12: for w being object st w in V1 holds

h1 . w Joins w,v1,G1 by A1, GLIB_007:57;

V2 c= V2 ;

then consider h2 being Function of V2,(G2 .edgesBetween (V2,{v2})) such that

A13: ( h2 is one-to-one & h2 is onto ) and

A14: for w being object st w in V2 holds

h2 . w Joins w,v2,G2 by A1, GLIB_007:57;

reconsider h1 = h1 as one-to-one Function by A11;

set g = (F0 _E) +* ((h2 * (F0 _V)) * (h1 "));

dom ((h2 * (F0 _V)) * (h1 ")) c= dom (h1 ") by RELAT_1:25;

then (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (dom (h1 ")) by XBOOLE_1:13;

then dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (dom (h1 ")) by FUNCT_4:def 1;

then dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (rng h1) by FUNCT_1:33;

then dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G3) \/ (G1 .edgesBetween (V1,{v1})) by A11, FUNCT_2:def 3;

then A15: dom ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= the_Edges_of G1 by A1, GLIB_007:59;

A16: rng ((h2 * (F0 _V)) * (h1 ")) c= rng (h2 * (F0 _V)) by RELAT_1:26;

rng (h2 * (F0 _V)) c= rng h2 by RELAT_1:26;

then rng ((h2 * (F0 _V)) * (h1 ")) c= rng h2 by A16, XBOOLE_1:1;

then A17: (rng (F0 _E)) \/ (rng ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G4) \/ (rng h2) by XBOOLE_1:13;

rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (rng (F0 _E)) \/ (rng ((h2 * (F0 _V)) * (h1 "))) by FUNCT_4:17;

then rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G4) \/ (rng h2) by A17, XBOOLE_1:1;

then rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= (the_Edges_of G4) \/ (G2 .edgesBetween (V2,{v2})) by A13, FUNCT_2:def 3;

then rng ((F0 _E) +* ((h2 * (F0 _V)) * (h1 "))) c= the_Edges_of G2 by A1, GLIB_007:59;

then reconsider g = (F0 _E) +* ((h2 * (F0 _V)) * (h1 ")) as PartFunc of (the_Edges_of G1),(the_Edges_of G2) by A15, RELSET_1:4;

A18: ( G1 .edgesBetween (V1,{v1}) misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ (G1 .edgesBetween (V1,{v1})) ) by A1, GLIB_007:59;

A19: dom (F0 _E) misses dom ((h2 * (F0 _V)) * (h1 "))

proof

A22:
rng (F0 _E) misses rng ((h2 * (F0 _V)) * (h1 "))
assume
dom (F0 _E) meets dom ((h2 * (F0 _V)) * (h1 "))
; :: thesis: contradiction

then (dom (F0 _E)) /\ (dom ((h2 * (F0 _V)) * (h1 "))) <> {} by XBOOLE_0:def 7;

then consider e being object such that

A20: e in (dom (F0 _E)) /\ (dom ((h2 * (F0 _V)) * (h1 "))) by XBOOLE_0:def 1;

A21: e in the_Edges_of G3 by A20;

e in dom ((h2 * (F0 _V)) * (h1 ")) by A20, XBOOLE_0:def 4;

then e in dom (h1 ") by FUNCT_1:11;

then e in rng h1 by FUNCT_1:33;

then e in G1 .edgesBetween (V1,{v1}) by A11, FUNCT_2:def 3;

then e in (the_Edges_of G3) /\ (G1 .edgesBetween (V1,{v1})) by A21, XBOOLE_0:def 4;

hence contradiction by A1, GLIB_007:59, XBOOLE_0:def 7; :: thesis: verum

end;then (dom (F0 _E)) /\ (dom ((h2 * (F0 _V)) * (h1 "))) <> {} by XBOOLE_0:def 7;

then consider e being object such that

A20: e in (dom (F0 _E)) /\ (dom ((h2 * (F0 _V)) * (h1 "))) by XBOOLE_0:def 1;

A21: e in the_Edges_of G3 by A20;

e in dom ((h2 * (F0 _V)) * (h1 ")) by A20, XBOOLE_0:def 4;

then e in dom (h1 ") by FUNCT_1:11;

then e in rng h1 by FUNCT_1:33;

then e in G1 .edgesBetween (V1,{v1}) by A11, FUNCT_2:def 3;

then e in (the_Edges_of G3) /\ (G1 .edgesBetween (V1,{v1})) by A21, XBOOLE_0:def 4;

hence contradiction by A1, GLIB_007:59, XBOOLE_0:def 7; :: thesis: verum

proof

consider E1 being set such that
assume
rng (F0 _E) meets rng ((h2 * (F0 _V)) * (h1 "))
; :: thesis: contradiction

then (rng (F0 _E)) /\ (rng ((h2 * (F0 _V)) * (h1 "))) <> {} by XBOOLE_0:def 7;

then consider e being object such that

A23: e in (rng (F0 _E)) /\ (rng ((h2 * (F0 _V)) * (h1 "))) by XBOOLE_0:def 1;

e in rng (F0 _E) by A23, XBOOLE_0:def 4;

then A24: e in the_Edges_of G4 ;

e in rng ((h2 * (F0 _V)) * (h1 ")) by A23, XBOOLE_0:def 4;

then e in rng (h2 * (F0 _V)) by RELAT_1:26, TARSKI:def 3;

then e in rng h2 by RELAT_1:26, TARSKI:def 3;

then e in (the_Edges_of G4) /\ (G2 .edgesBetween (V2,{v2})) by A24, XBOOLE_0:def 4;

hence contradiction by A1, GLIB_007:59, XBOOLE_0:def 7; :: thesis: verum

end;then (rng (F0 _E)) /\ (rng ((h2 * (F0 _V)) * (h1 "))) <> {} by XBOOLE_0:def 7;

then consider e being object such that

A23: e in (rng (F0 _E)) /\ (rng ((h2 * (F0 _V)) * (h1 "))) by XBOOLE_0:def 1;

e in rng (F0 _E) by A23, XBOOLE_0:def 4;

then A24: e in the_Edges_of G4 ;

e in rng ((h2 * (F0 _V)) * (h1 ")) by A23, XBOOLE_0:def 4;

then e in rng (h2 * (F0 _V)) by RELAT_1:26, TARSKI:def 3;

then e in rng h2 by RELAT_1:26, TARSKI:def 3;

then e in (the_Edges_of G4) /\ (G2 .edgesBetween (V2,{v2})) by A24, XBOOLE_0:def 4;

hence contradiction by A1, GLIB_007:59, XBOOLE_0:def 7; :: thesis: verum

( card V1 = card E1 & E1 misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ E1 ) and

A25: for w1 being object st w1 in V1 holds

ex e1 being object st

( e1 in E1 & e1 Joins w1,v1,G1 & ( for e9 being object st e9 Joins w1,v1,G1 holds

e1 = e9 ) ) by A1, GLIB_007:def 4;

consider E2 being set such that

( card V2 = card E2 & E2 misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ E2 ) and

A26: for w2 being object st w2 in V2 holds

ex e2 being object st

( e2 in E2 & e2 Joins w2,v2,G2 & ( for e9 being object st e9 Joins w2,v2,G2 holds

e2 = e9 ) ) by A1, GLIB_007:def 4;

now :: thesis: ( ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) )_{1} Joins f . b_{2},f . b_{3},G2 )

assume A29: ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G1 implies g . b_{1} Joins f . b_{2},f . b_{3},G2 )

assume A30: e Joins v,w,G1 ; :: thesis: g . b_{1} Joins f . b_{2},f . b_{3},G2

end;

then reconsider F = [f,g] as PGraphMapping of G1,G2 by Th8;( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) )

hereby :: thesis: for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . b_{4} Joins f . b_{5},f . b_{6},G2

let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e Joins v,w,G1 implies g . bg . b

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} in dom f ) )

assume e in dom g ; :: thesis: ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} in dom f )

then e in (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 "))) by FUNCT_4:def 1;

end;assume e in dom g ; :: thesis: ( (the_Source_of G1) . b

then e in (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 "))) by FUNCT_4:def 1;

per cases then
( e in dom (F0 _E) or e in dom ((h2 * (F0 _V)) * (h1 ")) )
by XBOOLE_0:def 3;

end;

suppose A27:
e in dom (F0 _E)
; :: thesis: ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} in dom f )

then
( (the_Source_of G1) . e = (the_Source_of G3) . e & (the_Target_of G1) . e = (the_Target_of G3) . e )
by GLIB_006:def 9;

then ( (the_Source_of G1) . e in dom (F0 _V) & (the_Target_of G1) . e in dom (F0 _V) ) by A27, Th5;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A6, XBOOLE_0:def 3; :: thesis: verum

end;then ( (the_Source_of G1) . e in dom (F0 _V) & (the_Target_of G1) . e in dom (F0 _V) ) by A27, Th5;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A6, XBOOLE_0:def 3; :: thesis: verum

suppose
e in dom ((h2 * (F0 _V)) * (h1 "))
; :: thesis: ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} in dom f )

then
e in dom (h1 ")
by RELAT_1:25, TARSKI:def 3;

then e in rng h1 by FUNCT_1:33;

then e in G1 .edgesBetween (V1,{v1}) by A11, FUNCT_2:def 3;

then e SJoins V1,{v1},G1 by GLIB_000:def 30;

then ( ( (the_Source_of G1) . e in V1 & (the_Target_of G1) . e in {v1} ) or ( (the_Source_of G1) . e in {v1} & (the_Target_of G1) . e in V1 ) ) by GLIB_000:def 15;

then A28: ( (the_Source_of G1) . e in V1 \/ {v1} & (the_Target_of G1) . e in V1 \/ {v1} ) by XBOOLE_0:def 3;

V1 \/ {v1} c= (dom (F0 _V)) \/ {v1} by A3, XBOOLE_1:9;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A6, A28; :: thesis: verum

end;then e in rng h1 by FUNCT_1:33;

then e in G1 .edgesBetween (V1,{v1}) by A11, FUNCT_2:def 3;

then e SJoins V1,{v1},G1 by GLIB_000:def 30;

then ( ( (the_Source_of G1) . e in V1 & (the_Target_of G1) . e in {v1} ) or ( (the_Source_of G1) . e in {v1} & (the_Target_of G1) . e in V1 ) ) by GLIB_000:def 15;

then A28: ( (the_Source_of G1) . e in V1 \/ {v1} & (the_Target_of G1) . e in V1 \/ {v1} ) by XBOOLE_0:def 3;

V1 \/ {v1} c= (dom (F0 _V)) \/ {v1} by A3, XBOOLE_1:9;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A6, A28; :: thesis: verum

assume A29: ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G1 implies g . b

assume A30: e Joins v,w,G1 ; :: thesis: g . b

per cases then
( e Joins v,w,G3 or not e in the_Edges_of G3 )
by GLIB_006:72;

end;

suppose A31:
e Joins v,w,G3
; :: thesis: g . b_{1} Joins f . b_{2},f . b_{3},G2

then A32:
e in the_Edges_of G3
by GLIB_000:def 13;

A33: not e in dom ((h2 * (F0 _V)) * (h1 "))

then A34: e in dom (F0 _E) by A33, XBOOLE_0:def 3;

( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by A31, GLIB_000:13;

then A35: ( not v in {v1} & not w in {v1} ) by A1, TARSKI:def 1;

then ( not v in dom (v1 .--> v2) & not w in dom (v1 .--> v2) ) ;

then A36: ( f . v = (F0 _V) . v & f . w = (F0 _V) . w ) by FUNCT_4:11;

( v in (dom (F0 _V)) \/ (dom (v1 .--> v2)) & w in (dom (F0 _V)) \/ (dom (v1 .--> v2)) ) by A29, FUNCT_4:def 1;

then ( v in dom (F0 _V) & w in dom (F0 _V) ) by A35, A5, XBOOLE_0:def 3;

then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A31, A34, Th4;

then g . e Joins f . v,f . w,G4 by A33, A36, FUNCT_4:11;

hence g . e Joins f . v,f . w,G2 by GLIB_006:70; :: thesis: verum

end;A33: not e in dom ((h2 * (F0 _V)) * (h1 "))

proof

e in (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 ")))
by A29, FUNCT_4:def 1;
assume
e in dom ((h2 * (F0 _V)) * (h1 "))
; :: thesis: contradiction

then e in dom (h1 ") by RELAT_1:25, TARSKI:def 3;

then e in rng h1 by FUNCT_1:33;

then e in G1 .edgesBetween (V1,{v1}) by A11, FUNCT_2:def 3;

then (the_Edges_of G3) /\ (G1 .edgesBetween (V1,{v1})) <> {} by A32, XBOOLE_0:def 4;

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

end;then e in dom (h1 ") by RELAT_1:25, TARSKI:def 3;

then e in rng h1 by FUNCT_1:33;

then e in G1 .edgesBetween (V1,{v1}) by A11, FUNCT_2:def 3;

then (the_Edges_of G3) /\ (G1 .edgesBetween (V1,{v1})) <> {} by A32, XBOOLE_0:def 4;

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

then A34: e in dom (F0 _E) by A33, XBOOLE_0:def 3;

( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by A31, GLIB_000:13;

then A35: ( not v in {v1} & not w in {v1} ) by A1, TARSKI:def 1;

then ( not v in dom (v1 .--> v2) & not w in dom (v1 .--> v2) ) ;

then A36: ( f . v = (F0 _V) . v & f . w = (F0 _V) . w ) by FUNCT_4:11;

( v in (dom (F0 _V)) \/ (dom (v1 .--> v2)) & w in (dom (F0 _V)) \/ (dom (v1 .--> v2)) ) by A29, FUNCT_4:def 1;

then ( v in dom (F0 _V) & w in dom (F0 _V) ) by A35, A5, XBOOLE_0:def 3;

then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A31, A34, Th4;

then g . e Joins f . v,f . w,G4 by A33, A36, FUNCT_4:11;

hence g . e Joins f . v,f . w,G2 by GLIB_006:70; :: thesis: verum

suppose A37:
not e in the_Edges_of G3
; :: thesis: g . b_{1} Joins f . b_{2},f . b_{3},G2

then A38:
( ( e in G1 .edgesBetween (V1,{v1}) & v = v1 & w in V1 ) or ( v in V1 & w = v1 ) )
by A1, A18, A30, GLIB_007:51;

A39: not e in dom (F0 _E) by A37;

e in (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 "))) by A29, FUNCT_4:def 1;

then A40: e in dom ((h2 * (F0 _V)) * (h1 ")) by A39, XBOOLE_0:def 3;

then A41: ( e in dom (h1 ") & (h1 ") . e in dom (h2 * (F0 _V)) ) by FUNCT_1:11;

A42: g . e = ((h2 * (F0 _V)) * (h1 ")) . e by A40, FUNCT_4:13

.= (h2 * (F0 _V)) . ((h1 ") . e) by A40, FUNCT_1:12

.= h2 . ((F0 _V) . ((h1 ") . e)) by A41, FUNCT_1:12 ;

e in rng h1 by A41, FUNCT_1:33;

then A43: G1 .edgesBetween (V1,{v1}) <> {} ;

end;A39: not e in dom (F0 _E) by A37;

e in (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 "))) by A29, FUNCT_4:def 1;

then A40: e in dom ((h2 * (F0 _V)) * (h1 ")) by A39, XBOOLE_0:def 3;

then A41: ( e in dom (h1 ") & (h1 ") . e in dom (h2 * (F0 _V)) ) by FUNCT_1:11;

A42: g . e = ((h2 * (F0 _V)) * (h1 ")) . e by A40, FUNCT_4:13

.= (h2 * (F0 _V)) . ((h1 ") . e) by A40, FUNCT_1:12

.= h2 . ((F0 _V) . ((h1 ") . e)) by A41, FUNCT_1:12 ;

e in rng h1 by A41, FUNCT_1:33;

then A43: G1 .edgesBetween (V1,{v1}) <> {} ;

per cases
( ( v = v1 & w in V1 ) or ( v in V1 & w = v1 ) )
by A38;

end;

suppose A44:
( v = v1 & w in V1 )
; :: thesis: g . b_{1} Joins f . b_{2},f . b_{3},G2

then
v in {v1}
by TARSKI:def 1;

then A45: f . v = (v1 .--> v2) . v by A5, FUNCT_4:13

.= v2 by A44, FUNCOP_1:72 ;

w <> v1 by A1, A44;

then not w in dom (v1 .--> v2) by TARSKI:def 1;

then A46: f . w = (F0 _V) . w by FUNCT_4:11;

consider e1 being object such that

( e1 in E1 & e1 Joins w,v1,G1 ) and

A47: for e2 being object st e2 Joins w,v1,G1 holds

e1 = e2 by A44, A25;

( h1 . w = e1 & e = e1 ) by A12, A30, A44, A47, GLIB_000:14;

then A48: h1 . w = e ;

w in dom h1 by A43, A44, FUNCT_2:def 1;

then A49: g . e = h2 . ((F0 _V) . w) by A42, A48, FUNCT_1:34;

A50: (F0 _V) . w = ((F0 _V) | V1) . w by A44, FUNCT_1:49;

w in dom ((F0 _V) | V1) by A3, A44, RELAT_1:57;

then h2 . ((F0 _V) . w) Joins (F0 _V) . w,v2,G2 by A2, A14, A50, FUNCT_1:3;

hence g . e Joins f . v,f . w,G2 by A45, A46, A49, GLIB_000:14; :: thesis: verum

end;then A45: f . v = (v1 .--> v2) . v by A5, FUNCT_4:13

.= v2 by A44, FUNCOP_1:72 ;

w <> v1 by A1, A44;

then not w in dom (v1 .--> v2) by TARSKI:def 1;

then A46: f . w = (F0 _V) . w by FUNCT_4:11;

consider e1 being object such that

( e1 in E1 & e1 Joins w,v1,G1 ) and

A47: for e2 being object st e2 Joins w,v1,G1 holds

e1 = e2 by A44, A25;

( h1 . w = e1 & e = e1 ) by A12, A30, A44, A47, GLIB_000:14;

then A48: h1 . w = e ;

w in dom h1 by A43, A44, FUNCT_2:def 1;

then A49: g . e = h2 . ((F0 _V) . w) by A42, A48, FUNCT_1:34;

A50: (F0 _V) . w = ((F0 _V) | V1) . w by A44, FUNCT_1:49;

w in dom ((F0 _V) | V1) by A3, A44, RELAT_1:57;

then h2 . ((F0 _V) . w) Joins (F0 _V) . w,v2,G2 by A2, A14, A50, FUNCT_1:3;

hence g . e Joins f . v,f . w,G2 by A45, A46, A49, GLIB_000:14; :: thesis: verum

suppose A51:
( v in V1 & w = v1 )
; :: thesis: g . b_{1} Joins f . b_{2},f . b_{3},G2

then
w in {v1}
by TARSKI:def 1;

then A52: f . w = (v1 .--> v2) . w by A5, FUNCT_4:13

.= v2 by A51, FUNCOP_1:72 ;

v in the_Vertices_of G3 by A1, A51;

then not v in {v1} by A1, TARSKI:def 1;

then not v in dom (v1 .--> v2) ;

then A53: f . v = (F0 _V) . v by FUNCT_4:11;

consider e1 being object such that

( e1 in E1 & e1 Joins v,v1,G1 ) and

A54: for e2 being object st e2 Joins v,v1,G1 holds

e1 = e2 by A51, A25;

( h1 . v = e1 & e = e1 ) by A12, A30, A51, A54;

then A55: h1 . v = e ;

v in dom h1 by A43, A51, FUNCT_2:def 1;

then A56: g . e = h2 . ((F0 _V) . v) by A42, A55, FUNCT_1:34;

A57: (F0 _V) . v = ((F0 _V) | V1) . v by A51, FUNCT_1:49;

v in dom ((F0 _V) | V1) by A3, A51, RELAT_1:57;

then h2 . ((F0 _V) . v) Joins (F0 _V) . v,v2,G2 by A2, A14, A57, FUNCT_1:3;

hence g . e Joins f . v,f . w,G2 by A52, A53, A56; :: thesis: verum

end;then A52: f . w = (v1 .--> v2) . w by A5, FUNCT_4:13

.= v2 by A51, FUNCOP_1:72 ;

v in the_Vertices_of G3 by A1, A51;

then not v in {v1} by A1, TARSKI:def 1;

then not v in dom (v1 .--> v2) ;

then A53: f . v = (F0 _V) . v by FUNCT_4:11;

consider e1 being object such that

( e1 in E1 & e1 Joins v,v1,G1 ) and

A54: for e2 being object st e2 Joins v,v1,G1 holds

e1 = e2 by A51, A25;

( h1 . v = e1 & e = e1 ) by A12, A30, A51, A54;

then A55: h1 . v = e ;

v in dom h1 by A43, A51, FUNCT_2:def 1;

then A56: g . e = h2 . ((F0 _V) . v) by A42, A55, FUNCT_1:34;

A57: (F0 _V) . v = ((F0 _V) | V1) . v by A51, FUNCT_1:49;

v in dom ((F0 _V) | V1) by A3, A51, RELAT_1:57;

then h2 . ((F0 _V) . v) Joins (F0 _V) . v,v2,G2 by A2, A14, A57, FUNCT_1:3;

hence g . e Joins f . v,f . w,G2 by A52, A53, A56; :: thesis: verum

take F ; :: thesis: ( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( 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 ) )

thus F _V = (F0 _V) +* (v1 .--> v2) ; :: thesis: ( (F _E) | (dom (F0 _E)) = F0 _E & ( 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 ) )

thus (F _E) | (dom (F0 _E)) = F0 _E by A19, FUNCT_4:33; :: thesis: ( ( 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 ) )

thus A58: ( F0 is total implies F is total ) :: thesis: ( ( 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 ) )

proof

assume F0 is total ; :: thesis: F is total

then A88: ( dom (F0 _V) = the_Vertices_of G3 & dom (F0 _E) = the_Edges_of G3 ) ;

A89: dom (F _V) = (dom (F0 _V)) \/ {v1} by A5, FUNCT_4:def 1

.= the_Vertices_of G1 by A1, A88, GLIB_007:def 4 ;

dom (F _E) = the_Edges_of G1 by A18, A87, A88, FUNCT_4:def 1;

hence F is total by A89; :: thesis: verum

end;

thus A90:
( F0 is onto implies F is onto )
:: thesis: ( ( 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 ) )now :: thesis: for x being object holds

( ( x in dom ((h2 * (F0 _V)) * (h1 ")) implies x in G1 .edgesBetween (V1,{v1}) ) & ( x in G1 .edgesBetween (V1,{v1}) implies x in dom ((h2 * (F0 _V)) * (h1 ")) ) )

then A87:
dom ((h2 * (F0 _V)) * (h1 ")) = G1 .edgesBetween (V1,{v1})
by TARSKI:2;( ( x in dom ((h2 * (F0 _V)) * (h1 ")) implies x in G1 .edgesBetween (V1,{v1}) ) & ( x in G1 .edgesBetween (V1,{v1}) implies x in dom ((h2 * (F0 _V)) * (h1 ")) ) )

let x be object ; :: thesis: ( ( x in dom ((h2 * (F0 _V)) * (h1 ")) implies x in G1 .edgesBetween (V1,{v1}) ) & ( x in G1 .edgesBetween (V1,{v1}) implies b_{1} in dom ((h2 * (F0 _V)) * (h1 ")) ) )

set w2 = (the_Target_of G1) . x;

assume A64: x in G1 .edgesBetween (V1,{v1}) ; :: thesis: b_{1} in dom ((h2 * (F0 _V)) * (h1 "))

then G1 .edgesBetween (V1,{v1}) <> {} ;

then A65: dom h1 = V1 by FUNCT_2:def 1;

A66: x SJoins V1,{v1},G1 by A64, GLIB_000:def 30;

end;hereby :: thesis: ( x in G1 .edgesBetween (V1,{v1}) implies b_{1} in dom ((h2 * (F0 _V)) * (h1 ")) )

set w1 = (the_Source_of G1) . x;assume
x in dom ((h2 * (F0 _V)) * (h1 "))
; :: thesis: x in G1 .edgesBetween (V1,{v1})

then A59: ( x in dom (h1 ") & (h1 ") . x in dom (h2 * (F0 _V)) ) by FUNCT_1:11;

A60: x in rng h1 by A59, FUNCT_1:33;

then h1 <> {} ;

then G1 .edgesBetween (V1,{v1}) <> {} ;

then A61: dom h1 = V1 by FUNCT_2:def 1;

consider y being object such that

A62: ( y in dom h1 & h1 . y = x ) by A60, FUNCT_1:def 3;

A63: x Joins y,v1,G1 by A12, A61, A62;

v1 in {v1} by TARSKI:def 1;

then x SJoins V1,{v1},G1 by A61, A62, A63, GLIB_000:17;

hence x in G1 .edgesBetween (V1,{v1}) by GLIB_000:def 30; :: thesis: verum

end;then A59: ( x in dom (h1 ") & (h1 ") . x in dom (h2 * (F0 _V)) ) by FUNCT_1:11;

A60: x in rng h1 by A59, FUNCT_1:33;

then h1 <> {} ;

then G1 .edgesBetween (V1,{v1}) <> {} ;

then A61: dom h1 = V1 by FUNCT_2:def 1;

consider y being object such that

A62: ( y in dom h1 & h1 . y = x ) by A60, FUNCT_1:def 3;

A63: x Joins y,v1,G1 by A12, A61, A62;

v1 in {v1} by TARSKI:def 1;

then x SJoins V1,{v1},G1 by A61, A62, A63, GLIB_000:17;

hence x in G1 .edgesBetween (V1,{v1}) by GLIB_000:def 30; :: thesis: verum

set w2 = (the_Target_of G1) . x;

assume A64: x in G1 .edgesBetween (V1,{v1}) ; :: thesis: b

then G1 .edgesBetween (V1,{v1}) <> {} ;

then A65: dom h1 = V1 by FUNCT_2:def 1;

A66: x SJoins V1,{v1},G1 by A64, GLIB_000:def 30;

per cases then
( ( (the_Source_of G1) . x in V1 & (the_Target_of G1) . x in {v1} ) or ( (the_Source_of G1) . x in {v1} & (the_Target_of G1) . x in V1 ) )
by GLIB_000:def 15;

end;

suppose A67:
( (the_Source_of G1) . x in V1 & (the_Target_of G1) . x in {v1} )
; :: thesis: b_{1} in dom ((h2 * (F0 _V)) * (h1 "))

then consider e1 being object such that

( e1 in E1 & e1 Joins (the_Source_of G1) . x,v1,G1 ) and

A68: for e2 being object st e2 Joins (the_Source_of G1) . x,v1,G1 holds

e1 = e2 by A25;

( (the_Target_of G1) . x = v1 & x in the_Edges_of G1 ) by A66, A67, TARSKI:def 1, GLIB_000:def 15;

then A69: x Joins (the_Source_of G1) . x,v1,G1 by GLIB_000:def 13;

( h1 . ((the_Source_of G1) . x) = e1 & x = e1 ) by A12, A67, A68, A69;

then A70: h1 . ((the_Source_of G1) . x) = x ;

then x in rng h1 by A65, A67, FUNCT_1:3;

then A71: x in dom (h1 ") by FUNCT_1:33;

A72: (the_Source_of G1) . x in dom (F0 _V) by A3, A67;

then A73: (the_Source_of G1) . x in dom ((F0 _V) | V1) by A67, RELAT_1:57;

(F0 _V) . ((the_Source_of G1) . x) = ((F0 _V) | V1) . ((the_Source_of G1) . x) by A67, FUNCT_1:49;

then A74: (F0 _V) . ((the_Source_of G1) . x) in V2 by A2, A73, FUNCT_1:3;

then A75: h2 . ((F0 _V) . ((the_Source_of G1) . x)) Joins (F0 _V) . ((the_Source_of G1) . x),v2,G2 by A14;

v2 in {v2} by TARSKI:def 1;

then h2 . ((F0 _V) . ((the_Source_of G1) . x)) SJoins V2,{v2},G2 by A74, A75, GLIB_000:17;

then h2 . ((F0 _V) . ((the_Source_of G1) . x)) in G2 .edgesBetween (V2,{v2}) by GLIB_000:def 30;

then dom h2 = V2 by FUNCT_2:def 1;

then A76: (the_Source_of G1) . x in dom (h2 * (F0 _V)) by A72, A74, FUNCT_1:11;

(h1 ") . x = (the_Source_of G1) . x by A65, A67, A70, FUNCT_1:34;

hence x in dom ((h2 * (F0 _V)) * (h1 ")) by A71, A76, FUNCT_1:11; :: thesis: verum

end;( e1 in E1 & e1 Joins (the_Source_of G1) . x,v1,G1 ) and

A68: for e2 being object st e2 Joins (the_Source_of G1) . x,v1,G1 holds

e1 = e2 by A25;

( (the_Target_of G1) . x = v1 & x in the_Edges_of G1 ) by A66, A67, TARSKI:def 1, GLIB_000:def 15;

then A69: x Joins (the_Source_of G1) . x,v1,G1 by GLIB_000:def 13;

( h1 . ((the_Source_of G1) . x) = e1 & x = e1 ) by A12, A67, A68, A69;

then A70: h1 . ((the_Source_of G1) . x) = x ;

then x in rng h1 by A65, A67, FUNCT_1:3;

then A71: x in dom (h1 ") by FUNCT_1:33;

A72: (the_Source_of G1) . x in dom (F0 _V) by A3, A67;

then A73: (the_Source_of G1) . x in dom ((F0 _V) | V1) by A67, RELAT_1:57;

(F0 _V) . ((the_Source_of G1) . x) = ((F0 _V) | V1) . ((the_Source_of G1) . x) by A67, FUNCT_1:49;

then A74: (F0 _V) . ((the_Source_of G1) . x) in V2 by A2, A73, FUNCT_1:3;

then A75: h2 . ((F0 _V) . ((the_Source_of G1) . x)) Joins (F0 _V) . ((the_Source_of G1) . x),v2,G2 by A14;

v2 in {v2} by TARSKI:def 1;

then h2 . ((F0 _V) . ((the_Source_of G1) . x)) SJoins V2,{v2},G2 by A74, A75, GLIB_000:17;

then h2 . ((F0 _V) . ((the_Source_of G1) . x)) in G2 .edgesBetween (V2,{v2}) by GLIB_000:def 30;

then dom h2 = V2 by FUNCT_2:def 1;

then A76: (the_Source_of G1) . x in dom (h2 * (F0 _V)) by A72, A74, FUNCT_1:11;

(h1 ") . x = (the_Source_of G1) . x by A65, A67, A70, FUNCT_1:34;

hence x in dom ((h2 * (F0 _V)) * (h1 ")) by A71, A76, FUNCT_1:11; :: thesis: verum

suppose A77:
( (the_Source_of G1) . x in {v1} & (the_Target_of G1) . x in V1 )
; :: thesis: b_{1} in dom ((h2 * (F0 _V)) * (h1 "))

then consider e1 being object such that

( e1 in E1 & e1 Joins (the_Target_of G1) . x,v1,G1 ) and

A78: for e2 being object st e2 Joins (the_Target_of G1) . x,v1,G1 holds

e1 = e2 by A25;

( (the_Source_of G1) . x = v1 & x in the_Edges_of G1 ) by A66, A77, TARSKI:def 1, GLIB_000:def 15;

then A79: x Joins (the_Target_of G1) . x,v1,G1 by GLIB_000:def 13;

( h1 . ((the_Target_of G1) . x) = e1 & x = e1 ) by A12, A77, A78, A79;

then A80: h1 . ((the_Target_of G1) . x) = x ;

then x in rng h1 by A65, A77, FUNCT_1:3;

then A81: x in dom (h1 ") by FUNCT_1:33;

A82: (the_Target_of G1) . x in dom (F0 _V) by A3, A77;

then A83: (the_Target_of G1) . x in dom ((F0 _V) | V1) by A77, RELAT_1:57;

(F0 _V) . ((the_Target_of G1) . x) = ((F0 _V) | V1) . ((the_Target_of G1) . x) by A77, FUNCT_1:49;

then A84: (F0 _V) . ((the_Target_of G1) . x) in V2 by A2, A83, FUNCT_1:3;

then A85: h2 . ((F0 _V) . ((the_Target_of G1) . x)) Joins (F0 _V) . ((the_Target_of G1) . x),v2,G2 by A14;

v2 in {v2} by TARSKI:def 1;

then h2 . ((F0 _V) . ((the_Target_of G1) . x)) SJoins V2,{v2},G2 by A84, A85, GLIB_000:17;

then G2 .edgesBetween (V2,{v2}) <> {} by GLIB_000:def 30;

then (F0 _V) . ((the_Target_of G1) . x) in dom h2 by A84, FUNCT_2:def 1;

then A86: (the_Target_of G1) . x in dom (h2 * (F0 _V)) by A82, FUNCT_1:11;

(h1 ") . x = (the_Target_of G1) . x by A65, A77, A80, FUNCT_1:34;

hence x in dom ((h2 * (F0 _V)) * (h1 ")) by A81, A86, FUNCT_1:11; :: thesis: verum

end;( e1 in E1 & e1 Joins (the_Target_of G1) . x,v1,G1 ) and

A78: for e2 being object st e2 Joins (the_Target_of G1) . x,v1,G1 holds

e1 = e2 by A25;

( (the_Source_of G1) . x = v1 & x in the_Edges_of G1 ) by A66, A77, TARSKI:def 1, GLIB_000:def 15;

then A79: x Joins (the_Target_of G1) . x,v1,G1 by GLIB_000:def 13;

( h1 . ((the_Target_of G1) . x) = e1 & x = e1 ) by A12, A77, A78, A79;

then A80: h1 . ((the_Target_of G1) . x) = x ;

then x in rng h1 by A65, A77, FUNCT_1:3;

then A81: x in dom (h1 ") by FUNCT_1:33;

A82: (the_Target_of G1) . x in dom (F0 _V) by A3, A77;

then A83: (the_Target_of G1) . x in dom ((F0 _V) | V1) by A77, RELAT_1:57;

(F0 _V) . ((the_Target_of G1) . x) = ((F0 _V) | V1) . ((the_Target_of G1) . x) by A77, FUNCT_1:49;

then A84: (F0 _V) . ((the_Target_of G1) . x) in V2 by A2, A83, FUNCT_1:3;

then A85: h2 . ((F0 _V) . ((the_Target_of G1) . x)) Joins (F0 _V) . ((the_Target_of G1) . x),v2,G2 by A14;

v2 in {v2} by TARSKI:def 1;

then h2 . ((F0 _V) . ((the_Target_of G1) . x)) SJoins V2,{v2},G2 by A84, A85, GLIB_000:17;

then G2 .edgesBetween (V2,{v2}) <> {} by GLIB_000:def 30;

then (F0 _V) . ((the_Target_of G1) . x) in dom h2 by A84, FUNCT_2:def 1;

then A86: (the_Target_of G1) . x in dom (h2 * (F0 _V)) by A82, FUNCT_1:11;

(h1 ") . x = (the_Target_of G1) . x by A65, A77, A80, FUNCT_1:34;

hence x in dom ((h2 * (F0 _V)) * (h1 ")) by A81, A86, FUNCT_1:11; :: thesis: verum

assume F0 is total ; :: thesis: F is total

then A88: ( dom (F0 _V) = the_Vertices_of G3 & dom (F0 _E) = the_Edges_of G3 ) ;

A89: dom (F _V) = (dom (F0 _V)) \/ {v1} by A5, FUNCT_4:def 1

.= the_Vertices_of G1 by A1, A88, GLIB_007:def 4 ;

dom (F _E) = the_Edges_of G1 by A18, A87, A88, FUNCT_4:def 1;

hence F is total by A89; :: thesis: verum

proof

assume F0 is onto ; :: thesis: F is onto

then A119: ( rng (F0 _V) = the_Vertices_of G4 & rng (F0 _E) = the_Edges_of G4 ) ;

A120: ( v1 is set & v2 is set ) by TARSKI:1;

A121: rng (F _V) = (rng (F0 _V)) \/ (rng (v1 .--> v2)) by A7, NECKLACE:6

.= (the_Vertices_of G4) \/ {v2} by A119, A120, FUNCOP_1:88

.= the_Vertices_of G2 by A1, GLIB_007:def 4 ;

rng (F _E) = (rng (F0 _E)) \/ (rng ((h2 * (F0 _V)) * (h1 "))) by A19, NECKLACE:6

.= the_Edges_of G2 by A1, A118, A119, GLIB_007:59 ;

hence F is onto by A121; :: thesis: verum

end;

thus A122:
( F0 is one-to-one implies F is one-to-one )
by A9, A13, A22, FUNCT_4:92; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )now :: thesis: for x being object holds

( ( x in rng ((h2 * (F0 _V)) * (h1 ")) implies x in G2 .edgesBetween (V2,{v2}) ) & ( x in G2 .edgesBetween (V2,{v2}) implies x in rng ((h2 * (F0 _V)) * (h1 ")) ) )

then A118:
rng ((h2 * (F0 _V)) * (h1 ")) = G2 .edgesBetween (V2,{v2})
by TARSKI:2;( ( x in rng ((h2 * (F0 _V)) * (h1 ")) implies x in G2 .edgesBetween (V2,{v2}) ) & ( x in G2 .edgesBetween (V2,{v2}) implies x in rng ((h2 * (F0 _V)) * (h1 ")) ) )

let x be object ; :: thesis: ( ( x in rng ((h2 * (F0 _V)) * (h1 ")) implies x in G2 .edgesBetween (V2,{v2}) ) & ( x in G2 .edgesBetween (V2,{v2}) implies b_{1} in rng ((h2 * (F0 _V)) * (h1 ")) ) )

thus ( x in rng ((h2 * (F0 _V)) * (h1 ")) implies x in G2 .edgesBetween (V2,{v2}) ) ; :: thesis: ( x in G2 .edgesBetween (V2,{v2}) implies b_{1} in rng ((h2 * (F0 _V)) * (h1 ")) )

set w1 = (the_Source_of G2) . x;

set w2 = (the_Target_of G2) . x;

assume A91: x in G2 .edgesBetween (V2,{v2}) ; :: thesis: b_{1} in rng ((h2 * (F0 _V)) * (h1 "))

then A92: dom h2 = V2 by FUNCT_2:def 1;

A93: x SJoins V2,{v2},G2 by A91, GLIB_000:def 30;

end;thus ( x in rng ((h2 * (F0 _V)) * (h1 ")) implies x in G2 .edgesBetween (V2,{v2}) ) ; :: thesis: ( x in G2 .edgesBetween (V2,{v2}) implies b

set w1 = (the_Source_of G2) . x;

set w2 = (the_Target_of G2) . x;

assume A91: x in G2 .edgesBetween (V2,{v2}) ; :: thesis: b

then A92: dom h2 = V2 by FUNCT_2:def 1;

A93: x SJoins V2,{v2},G2 by A91, GLIB_000:def 30;

per cases then
( ( (the_Source_of G2) . x in V2 & (the_Target_of G2) . x in {v2} ) or ( (the_Source_of G2) . x in {v2} & (the_Target_of G2) . x in V2 ) )
by GLIB_000:def 15;

end;

suppose A94:
( (the_Source_of G2) . x in V2 & (the_Target_of G2) . x in {v2} )
; :: thesis: b_{1} in rng ((h2 * (F0 _V)) * (h1 "))

then A95:
h2 . ((the_Source_of G2) . x) Joins (the_Source_of G2) . x,v2,G2
by A14;

consider e2 being object such that

( e2 in E2 & e2 Joins (the_Source_of G2) . x,v2,G2 ) and

A96: for e9 being object st e9 Joins (the_Source_of G2) . x,v2,G2 holds

e2 = e9 by A94, A26;

( (the_Target_of G2) . x = v2 & x in the_Edges_of G2 ) by A93, A94, GLIB_000:def 15, TARSKI:def 1;

then x Joins (the_Source_of G2) . x,v2,G2 by GLIB_000:def 13;

then ( h2 . ((the_Source_of G2) . x) = e2 & x = e2 ) by A95, A96;

then A97: h2 . ((the_Source_of G2) . x) = x ;

(the_Source_of G2) . x in rng ((F0 _V) | V1) by A2, A94;

then consider z being object such that

A98: ( z in dom ((F0 _V) | V1) & ((F0 _V) | V1) . z = (the_Source_of G2) . x ) by FUNCT_1:def 3;

A99: z in V1 by A98;

then A100: h1 . z Joins z,v1,G1 by A12;

v1 in {v1} by TARSKI:def 1;

then h1 . z SJoins V1,{v1},G1 by A99, A100, GLIB_000:17;

then h1 . z in G1 .edgesBetween (V1,{v1}) by GLIB_000:def 30;

then dom h1 = V1 by FUNCT_2:def 1;

then z in rng (h1 ") by A99, FUNCT_1:33;

then consider y being object such that

A101: ( y in dom (h1 ") & (h1 ") . y = z ) by FUNCT_1:def 3;

(h1 ") . y in V1 by A99, A101;

then A102: y in dom ((F0 _V) * (h1 ")) by A3, A101, FUNCT_1:11;

then A103: ((F0 _V) * (h1 ")) . y = (F0 _V) . z by A101, FUNCT_1:12

.= (the_Source_of G2) . x by A98, FUNCT_1:49 ;

then A104: y in dom (h2 * ((F0 _V) * (h1 "))) by A92, A94, A102, FUNCT_1:11;

A105: ((h2 * (F0 _V)) * (h1 ")) . y = (h2 * ((F0 _V) * (h1 "))) . y by RELAT_1:36

.= x by A97, A103, A104, FUNCT_1:12 ;

y in dom ((h2 * (F0 _V)) * (h1 ")) by A104, RELAT_1:36;

hence x in rng ((h2 * (F0 _V)) * (h1 ")) by A105, FUNCT_1:3; :: thesis: verum

end;consider e2 being object such that

( e2 in E2 & e2 Joins (the_Source_of G2) . x,v2,G2 ) and

A96: for e9 being object st e9 Joins (the_Source_of G2) . x,v2,G2 holds

e2 = e9 by A94, A26;

( (the_Target_of G2) . x = v2 & x in the_Edges_of G2 ) by A93, A94, GLIB_000:def 15, TARSKI:def 1;

then x Joins (the_Source_of G2) . x,v2,G2 by GLIB_000:def 13;

then ( h2 . ((the_Source_of G2) . x) = e2 & x = e2 ) by A95, A96;

then A97: h2 . ((the_Source_of G2) . x) = x ;

(the_Source_of G2) . x in rng ((F0 _V) | V1) by A2, A94;

then consider z being object such that

A98: ( z in dom ((F0 _V) | V1) & ((F0 _V) | V1) . z = (the_Source_of G2) . x ) by FUNCT_1:def 3;

A99: z in V1 by A98;

then A100: h1 . z Joins z,v1,G1 by A12;

v1 in {v1} by TARSKI:def 1;

then h1 . z SJoins V1,{v1},G1 by A99, A100, GLIB_000:17;

then h1 . z in G1 .edgesBetween (V1,{v1}) by GLIB_000:def 30;

then dom h1 = V1 by FUNCT_2:def 1;

then z in rng (h1 ") by A99, FUNCT_1:33;

then consider y being object such that

A101: ( y in dom (h1 ") & (h1 ") . y = z ) by FUNCT_1:def 3;

(h1 ") . y in V1 by A99, A101;

then A102: y in dom ((F0 _V) * (h1 ")) by A3, A101, FUNCT_1:11;

then A103: ((F0 _V) * (h1 ")) . y = (F0 _V) . z by A101, FUNCT_1:12

.= (the_Source_of G2) . x by A98, FUNCT_1:49 ;

then A104: y in dom (h2 * ((F0 _V) * (h1 "))) by A92, A94, A102, FUNCT_1:11;

A105: ((h2 * (F0 _V)) * (h1 ")) . y = (h2 * ((F0 _V) * (h1 "))) . y by RELAT_1:36

.= x by A97, A103, A104, FUNCT_1:12 ;

y in dom ((h2 * (F0 _V)) * (h1 ")) by A104, RELAT_1:36;

hence x in rng ((h2 * (F0 _V)) * (h1 ")) by A105, FUNCT_1:3; :: thesis: verum

suppose A106:
( (the_Source_of G2) . x in {v2} & (the_Target_of G2) . x in V2 )
; :: thesis: b_{1} in rng ((h2 * (F0 _V)) * (h1 "))

then A107:
h2 . ((the_Target_of G2) . x) Joins (the_Target_of G2) . x,v2,G2
by A14;

consider e2 being object such that

( e2 in E2 & e2 Joins (the_Target_of G2) . x,v2,G2 ) and

A108: for e9 being object st e9 Joins (the_Target_of G2) . x,v2,G2 holds

e2 = e9 by A106, A26;

( (the_Source_of G2) . x = v2 & x in the_Edges_of G2 ) by A93, A106, GLIB_000:def 15, TARSKI:def 1;

then x Joins (the_Target_of G2) . x,v2,G2 by GLIB_000:def 13;

then ( h2 . ((the_Target_of G2) . x) = e2 & x = e2 ) by A107, A108;

then A109: h2 . ((the_Target_of G2) . x) = x ;

(the_Target_of G2) . x in rng ((F0 _V) | V1) by A2, A106;

then consider z being object such that

A110: ( z in dom ((F0 _V) | V1) & ((F0 _V) | V1) . z = (the_Target_of G2) . x ) by FUNCT_1:def 3;

A111: z in V1 by A110;

then A112: h1 . z Joins z,v1,G1 by A12;

v1 in {v1} by TARSKI:def 1;

then h1 . z SJoins V1,{v1},G1 by A111, A112, GLIB_000:17;

then h1 . z in G1 .edgesBetween (V1,{v1}) by GLIB_000:def 30;

then dom h1 = V1 by FUNCT_2:def 1;

then z in rng (h1 ") by A111, FUNCT_1:33;

then consider y being object such that

A113: ( y in dom (h1 ") & (h1 ") . y = z ) by FUNCT_1:def 3;

(h1 ") . y in V1 by A111, A113;

then A114: y in dom ((F0 _V) * (h1 ")) by A3, A113, FUNCT_1:11;

then A115: ((F0 _V) * (h1 ")) . y = (F0 _V) . z by A113, FUNCT_1:12

.= (the_Target_of G2) . x by A110, FUNCT_1:49 ;

then A116: y in dom (h2 * ((F0 _V) * (h1 "))) by A92, A106, A114, FUNCT_1:11;

A117: ((h2 * (F0 _V)) * (h1 ")) . y = (h2 * ((F0 _V) * (h1 "))) . y by RELAT_1:36

.= x by A109, A115, A116, FUNCT_1:12 ;

y in dom ((h2 * (F0 _V)) * (h1 ")) by A116, RELAT_1:36;

hence x in rng ((h2 * (F0 _V)) * (h1 ")) by A117, FUNCT_1:3; :: thesis: verum

end;consider e2 being object such that

( e2 in E2 & e2 Joins (the_Target_of G2) . x,v2,G2 ) and

A108: for e9 being object st e9 Joins (the_Target_of G2) . x,v2,G2 holds

e2 = e9 by A106, A26;

( (the_Source_of G2) . x = v2 & x in the_Edges_of G2 ) by A93, A106, GLIB_000:def 15, TARSKI:def 1;

then x Joins (the_Target_of G2) . x,v2,G2 by GLIB_000:def 13;

then ( h2 . ((the_Target_of G2) . x) = e2 & x = e2 ) by A107, A108;

then A109: h2 . ((the_Target_of G2) . x) = x ;

(the_Target_of G2) . x in rng ((F0 _V) | V1) by A2, A106;

then consider z being object such that

A110: ( z in dom ((F0 _V) | V1) & ((F0 _V) | V1) . z = (the_Target_of G2) . x ) by FUNCT_1:def 3;

A111: z in V1 by A110;

then A112: h1 . z Joins z,v1,G1 by A12;

v1 in {v1} by TARSKI:def 1;

then h1 . z SJoins V1,{v1},G1 by A111, A112, GLIB_000:17;

then h1 . z in G1 .edgesBetween (V1,{v1}) by GLIB_000:def 30;

then dom h1 = V1 by FUNCT_2:def 1;

then z in rng (h1 ") by A111, FUNCT_1:33;

then consider y being object such that

A113: ( y in dom (h1 ") & (h1 ") . y = z ) by FUNCT_1:def 3;

(h1 ") . y in V1 by A111, A113;

then A114: y in dom ((F0 _V) * (h1 ")) by A3, A113, FUNCT_1:11;

then A115: ((F0 _V) * (h1 ")) . y = (F0 _V) . z by A113, FUNCT_1:12

.= (the_Target_of G2) . x by A110, FUNCT_1:49 ;

then A116: y in dom (h2 * ((F0 _V) * (h1 "))) by A92, A106, A114, FUNCT_1:11;

A117: ((h2 * (F0 _V)) * (h1 ")) . y = (h2 * ((F0 _V) * (h1 "))) . y by RELAT_1:36

.= x by A109, A115, A116, FUNCT_1:12 ;

y in dom ((h2 * (F0 _V)) * (h1 ")) by A116, RELAT_1:36;

hence x in rng ((h2 * (F0 _V)) * (h1 ")) by A117, FUNCT_1:3; :: thesis: verum

assume F0 is onto ; :: thesis: F is onto

then A119: ( rng (F0 _V) = the_Vertices_of G4 & rng (F0 _E) = the_Edges_of G4 ) ;

A120: ( v1 is set & v2 is set ) by TARSKI:1;

A121: rng (F _V) = (rng (F0 _V)) \/ (rng (v1 .--> v2)) by A7, NECKLACE:6

.= (the_Vertices_of G4) \/ {v2} by A119, A120, FUNCOP_1:88

.= the_Vertices_of G2 by A1, GLIB_007:def 4 ;

rng (F _E) = (rng (F0 _E)) \/ (rng ((h2 * (F0 _V)) * (h1 "))) by A19, NECKLACE:6

.= the_Edges_of G2 by A1, A118, A119, GLIB_007:59 ;

hence F is onto by A121; :: thesis: verum

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A58, A122; :: thesis: ( F0 is isomorphism implies F is isomorphism )

thus ( F0 is isomorphism implies F is isomorphism ) by A58, A90, A122; :: thesis: verum