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)

proof

V1 = (dom (F0 _V)) /\ V1 by A2, RELAT_1:61;
hence V1 c= dom (F0 _V) by XBOOLE_1:17; :: thesis: verum

end;

set f = (F0 _V) +* (v1 .--> v2);
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

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;

A22: rng (F0 _E) misses rng ((h2 * (F0 _V)) * (h1 "))

proof

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;

consider E1 being set such that
( 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 ) )

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₄ Joins f . b₅,f . b₆,G2

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ in dom f ) )
assume e in dom g ; :: thesis: ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ in dom f )
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;

suppose A27: e in dom (F0 _E) ; :: thesis: ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ 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;

suppose e in dom ((h2 * (F0 _V)) * (h1 ")) ; :: thesis: ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ 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;

end;

end;

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 . b₁ Joins f . b₂,f . b₃,G2 )
assume A29: ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G1 implies g . b₁ Joins f . b₂,f . b₃,G2 )
assume A30: e Joins v,w,G1 ; :: thesis: g . b₁ Joins f . b₂,f . b₃,G2

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

suppose A31: e Joins v,w,G3 ; :: thesis: g . b₁ Joins f . b₂,f . b₃,G2

then A32: e in the_Edges_of G3 by GLIB_000:def 13;
A33: not e in dom ((h2 * (F0 _V)) * (h1 "))

proof

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;

e in (dom (F0 _E)) \/ (dom ((h2 * (F0 _V)) * (h1 "))) by A29, FUNCT_4:def 1;
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;

suppose A37: not e in the_Edges_of G3 ; :: thesis: g . b₁ Joins f . b₂,f . b₃,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}) <> {} ;

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

suppose A44: ( v = v1 & w in V1 ) ; :: thesis: g . b₁ Joins f . b₂,f . b₃,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;

suppose A51: ( v in V1 & w = v1 ) ; :: thesis: g . b₁ Joins f . b₂,f . b₃,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;

end;

end;

end;

end;

then reconsider F = [f,g] as PGraphMapping of G1,G2 by Th8;
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

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 ")) ) )

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₁ in dom ((h2 * (F0 _V)) * (h1 ")) ) )

hereby :: thesis: ( x in G1 .edgesBetween (V1,{v1}) implies b₁ in dom ((h2 * (F0 _V)) * (h1 ")) )

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;

set w1 = (the_Source_of G1) . x;
set w2 = (the_Target_of G1) . x;
assume A64: x in G1 .edgesBetween (V1,{v1}) ; :: thesis: b₁ 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;

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;

suppose A67: ( (the_Source_of G1) . x in V1 & (the_Target_of G1) . x in {v1} ) ; :: thesis: b₁ 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;

suppose A77: ( (the_Source_of G1) . x in {v1} & (the_Target_of G1) . x in V1 ) ; :: thesis: b₁ 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;

end;

end;

then A87: dom ((h2 * (F0 _V)) * (h1 ")) = G1 .edgesBetween (V1,{v1}) by TARSKI:2;
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 ) )

proof

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 ")) ) )

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

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;

suppose A94: ( (the_Source_of G2) . x in V2 & (the_Target_of G2) . x in {v2} ) ; :: thesis: b₁ 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;

suppose A106: ( (the_Source_of G2) . x in {v2} & (the_Target_of G2) . x in V2 ) ; :: thesis: b₁ 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;

end;

end;

then A118: rng ((h2 * (F0 _V)) * (h1 ")) = G2 .edgesBetween (V2,{v2}) by TARSKI:2;
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 ) )
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