let G3, G4 be _Graph; :: thesis: for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let v1, v3 be Vertex of G3; :: thesis: for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let v2, v4 be Vertex of G4; :: thesis: for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let e1, e2 be object ; :: thesis: for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let G1 be addEdge of G3,v1,e1,v3; :: thesis: for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let G2 be addEdge of G4,v2,e2,v4; :: thesis: for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) implies ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) ) )

A1: ( e1 is set & e2 is set ) by TARSKI:1;

assume that

A2: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 ) and

A3: ( v1 in dom (F0 _V) & v3 in dom (F0 _V) ) and

A4: ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

( the_Vertices_of G1 = the_Vertices_of G3 & the_Vertices_of G2 = the_Vertices_of G4 ) by GLIB_006:102;

then reconsider f = F0 _V as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) ;

set g = (F0 _E) +* (e1 .--> e2);

A5: dom ((F0 _E) +* (e1 .--> e2)) = (dom (F0 _E)) \/ (dom (e1 .--> e2)) by FUNCT_4:def 1

.= (dom (F0 _E)) \/ (dom ({e1} --> e2)) by FUNCOP_1:def 9

.= (dom (F0 _E)) \/ {e1} ;

not e1 in dom (F0 _E) by A2;

then dom (F0 _E) misses {e1} by ZFMISC_1:50;

then dom (F0 _E) misses dom ({e1} --> e2) ;

then A6: dom (F0 _E) misses dom (e1 .--> e2) by FUNCOP_1:def 9;

dom ((F0 _E) +* (e1 .--> e2)) c= (the_Edges_of G3) \/ {e1} by A5, XBOOLE_1:9;

then A7: dom ((F0 _E) +* (e1 .--> e2)) c= the_Edges_of G1 by A2, GLIB_006:def 11;

not e2 in rng (F0 _E) by A2;

then rng (F0 _E) misses {e2} by ZFMISC_1:50;

then A8: rng (F0 _E) misses rng (e1 .--> e2) by A1, FUNCOP_1:88;

A9: rng ((F0 _E) +* (e1 .--> e2)) = (rng (F0 _E)) \/ (rng (e1 .--> e2)) by A6, NECKLACE:6

.= (rng (F0 _E)) \/ {e2} by A1, FUNCOP_1:88 ;

rng ((F0 _E) +* (e1 .--> e2)) c= (the_Edges_of G4) \/ {e2} by A9, XBOOLE_1:9;

then rng ((F0 _E) +* (e1 .--> e2)) c= the_Edges_of G2 by A2, GLIB_006:def 11;

then reconsider g = (F0 _E) +* (e1 .--> e2) as PartFunc of (the_Edges_of G1),(the_Edges_of G2) by A7, RELSET_1:4;

A10: (dom g) /\ (the_Edges_of G3) = ((dom (F0 _E)) /\ (the_Edges_of G3)) \/ ({e1} /\ (the_Edges_of G3)) by A5, XBOOLE_1:23

.= (dom (F0 _E)) \/ ({e1} /\ (the_Edges_of G3)) by XBOOLE_1:28

.= (dom (F0 _E)) \/ {} by A2, ZFMISC_1:50, XBOOLE_0:def 7 ;

take F ; :: thesis: ( F = [(F0 _V),((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 ) )

thus F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] ; :: 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 ) )

thus ( F0 is total implies F is total ) by A2, A5, GLIB_006:def 11; :: thesis: ( ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) )

thus ( F0 is onto implies F is onto ) by A2, A9, GLIB_006:def 11; :: thesis: ( F0 is one-to-one implies F is one-to-one )

thus ( F0 is one-to-one implies F is one-to-one ) by A8, FUNCT_4:92; :: thesis: verum

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let v1, v3 be Vertex of G3; :: thesis: for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let v2, v4 be Vertex of G4; :: thesis: for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let e1, e2 be object ; :: thesis: for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let G1 be addEdge of G3,v1,e1,v3; :: thesis: for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let G2 be addEdge of G4,v2,e2,v4; :: thesis: for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) implies ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) ) )

A1: ( e1 is set & e2 is set ) by TARSKI:1;

assume that

A2: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 ) and

A3: ( v1 in dom (F0 _V) & v3 in dom (F0 _V) ) and

A4: ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((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 ) )

( the_Vertices_of G1 = the_Vertices_of G3 & the_Vertices_of G2 = the_Vertices_of G4 ) by GLIB_006:102;

then reconsider f = F0 _V as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) ;

set g = (F0 _E) +* (e1 .--> e2);

A5: dom ((F0 _E) +* (e1 .--> e2)) = (dom (F0 _E)) \/ (dom (e1 .--> e2)) by FUNCT_4:def 1

.= (dom (F0 _E)) \/ (dom ({e1} --> e2)) by FUNCOP_1:def 9

.= (dom (F0 _E)) \/ {e1} ;

not e1 in dom (F0 _E) by A2;

then dom (F0 _E) misses {e1} by ZFMISC_1:50;

then dom (F0 _E) misses dom ({e1} --> e2) ;

then A6: dom (F0 _E) misses dom (e1 .--> e2) by FUNCOP_1:def 9;

dom ((F0 _E) +* (e1 .--> e2)) c= (the_Edges_of G3) \/ {e1} by A5, XBOOLE_1:9;

then A7: dom ((F0 _E) +* (e1 .--> e2)) c= the_Edges_of G1 by A2, GLIB_006:def 11;

not e2 in rng (F0 _E) by A2;

then rng (F0 _E) misses {e2} by ZFMISC_1:50;

then A8: rng (F0 _E) misses rng (e1 .--> e2) by A1, FUNCOP_1:88;

A9: rng ((F0 _E) +* (e1 .--> e2)) = (rng (F0 _E)) \/ (rng (e1 .--> e2)) by A6, NECKLACE:6

.= (rng (F0 _E)) \/ {e2} by A1, FUNCOP_1:88 ;

rng ((F0 _E) +* (e1 .--> e2)) c= (the_Edges_of G4) \/ {e2} by A9, XBOOLE_1:9;

then rng ((F0 _E) +* (e1 .--> e2)) c= the_Edges_of G2 by A2, GLIB_006:def 11;

then reconsider g = (F0 _E) +* (e1 .--> e2) as PartFunc of (the_Edges_of G1),(the_Edges_of G2) by A7, RELSET_1:4;

A10: (dom g) /\ (the_Edges_of G3) = ((dom (F0 _E)) /\ (the_Edges_of G3)) \/ ({e1} /\ (the_Edges_of G3)) by A5, XBOOLE_1:23

.= (dom (F0 _E)) \/ ({e1} /\ (the_Edges_of G3)) by XBOOLE_1:28

.= (dom (F0 _E)) \/ {} by A2, ZFMISC_1:50, XBOOLE_0:def 7 ;

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 A17: ( 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 A18: 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 A11: e in dom g ; :: thesis: ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} in dom f )

then A12: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;

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

then A12: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;

per cases then
( e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G3 or not e in the_Edges_of G3 )
by GLIB_006:72;

end;

suppose A13:
e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G3
; :: thesis: ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} in dom f )

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

then e in dom (F0 _E) by A10, A11, XBOOLE_0:def 4;

then A15: ( (the_Source_of G3) . e in dom (F0 _V) & (the_Target_of G3) . e in dom (F0 _V) ) by Th5;

e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by A14, GLIB_000:def 13;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A13, A15, GLIB_000:15; :: thesis: verum

end;then e in dom (F0 _E) by A10, A11, XBOOLE_0:def 4;

then A15: ( (the_Source_of G3) . e in dom (F0 _V) & (the_Target_of G3) . e in dom (F0 _V) ) by Th5;

e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by A14, GLIB_000:def 13;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A13, A15, GLIB_000:15; :: thesis: verum

suppose A16:
not e in the_Edges_of G3
; :: thesis: ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} in dom f )

then
e = e1
by A2, A12, GLIB_006:106;

then e DJoins v1,v3,G1 by A16, GLIB_006:105;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A3, GLIB_000:def 14; :: thesis: verum

end;then e DJoins v1,v3,G1 by A16, GLIB_006:105;

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A3, GLIB_000:def 14; :: thesis: verum

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

assume A18: 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 A19:
e Joins v,w,G3
; :: thesis: g . b_{1} Joins f . b_{2},f . b_{3},G2

then
e in the_Edges_of G3
by GLIB_000:def 13;

then A20: e in dom (F0 _E) by A10, A17, XBOOLE_0:def 4;

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

then g . e Joins f . v,f . w,G4 by A17, A19, A20, Th4;

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

end;then A20: e in dom (F0 _E) by A10, A17, XBOOLE_0:def 4;

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

proof

then
g . e = (F0 _E) . e
by FUNCT_4:11;
assume
e in dom (e1 .--> e2)
; :: thesis: contradiction

then e in (dom (F0 _E)) /\ (dom (e1 .--> e2)) by A20, XBOOLE_0:def 4;

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

end;then e in (dom (F0 _E)) /\ (dom (e1 .--> e2)) by A20, XBOOLE_0:def 4;

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

then g . e Joins f . v,f . w,G4 by A17, A19, A20, Th4;

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

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

then A22:
e = e1
by A2, A18, GLIB_006:106;

then e in {e1} by TARSKI:def 1;

then e in dom ({e1} --> e2) ;

then A23: e in dom (e1 .--> e2) by FUNCOP_1:def 9;

A24: e2 = (e1 .--> e2) . e by A22, FUNCOP_1:72

.= g . e by A23, FUNCT_4:13 ;

e2 DJoins v2,v4,G2 by A2, GLIB_006:105;

then g . e Joins v2,v4,G2 by A24, GLIB_000:16;

then A25: g . e Joins (F0 _V) . v1,(F0 _V) . v3,G2 by A4, GLIB_000:14;

( ( v = v1 & w = v3 ) or ( v = v3 & w = v1 ) ) by A2, A18, A21, GLIB_006:107;

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

end;then e in {e1} by TARSKI:def 1;

then e in dom ({e1} --> e2) ;

then A23: e in dom (e1 .--> e2) by FUNCOP_1:def 9;

A24: e2 = (e1 .--> e2) . e by A22, FUNCOP_1:72

.= g . e by A23, FUNCT_4:13 ;

e2 DJoins v2,v4,G2 by A2, GLIB_006:105;

then g . e Joins v2,v4,G2 by A24, GLIB_000:16;

then A25: g . e Joins (F0 _V) . v1,(F0 _V) . v3,G2 by A4, GLIB_000:14;

( ( v = v1 & w = v3 ) or ( v = v3 & w = v1 ) ) by A2, A18, A21, GLIB_006:107;

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

take F ; :: thesis: ( F = [(F0 _V),((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 ) )

thus F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] ; :: 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 ) )

thus ( F0 is total implies F is total ) by A2, A5, GLIB_006:def 11; :: thesis: ( ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) )

thus ( F0 is onto implies F is onto ) by A2, A9, GLIB_006:def 11; :: thesis: ( F0 is one-to-one implies F is one-to-one )

thus ( F0 is one-to-one implies F is one-to-one ) by A8, FUNCT_4:92; :: thesis: verum