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 (),() ;
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= () \/ {e1} by ;
then A7: dom ((F0 _E) +* (e1 .--> e2)) c= the_Edges_of G1 by ;
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 ;
A9: rng ((F0 _E) +* (e1 .--> e2)) = (rng (F0 _E)) \/ (rng (e1 .--> e2)) by
.= (rng (F0 _E)) \/ {e2} by ;
rng ((F0 _E) +* (e1 .--> e2)) c= () \/ {e2} by ;
then rng ((F0 _E) +* (e1 .--> e2)) c= the_Edges_of G2 by ;
then reconsider g = (F0 _E) +* (e1 .--> e2) as PartFunc of (),() by ;
A10: (dom g) /\ () = ((dom (F0 _E)) /\ ()) \/ ({e1} /\ ()) by
.= (dom (F0 _E)) \/ ({e1} /\ ()) by XBOOLE_1:28
.= (dom (F0 _E)) \/ {} by ;
now :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom f & () . 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 . b4 Joins f . b5,f . b6,G2
let e be object ; :: thesis: ( e in dom g implies ( () . b1 in dom f & () . b1 in dom f ) )
assume A11: e in dom g ; :: thesis: ( () . b1 in dom f & () . b1 in dom f )
then A12: e Joins () . e,() . e,G1 by GLIB_000:def 13;
per cases then ( e Joins () . e,() . e,G3 or not e in the_Edges_of G3 ) by GLIB_006:72;
suppose A13: e Joins () . e,() . e,G3 ; :: thesis: ( () . b1 in dom f & () . b1 in dom f )
then A14: e in the_Edges_of G3 by GLIB_000:def 13;
then e in dom (F0 _E) by ;
then A15: ( (the_Source_of G3) . e in dom (F0 _V) & () . e in dom (F0 _V) ) by Th5;
e Joins () . e,() . e,G3 by ;
hence ( (the_Source_of G1) . e in dom f & () . e in dom f ) by ; :: thesis: verum
end;
suppose A16: not e in the_Edges_of G3 ; :: thesis: ( () . b1 in dom f & () . b1 in dom f )
then e = e1 by ;
then e DJoins v1,v3,G1 by ;
hence ( (the_Source_of G1) . e in dom f & () . e in dom f ) by ; :: 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 . b1 Joins f . b2,f . b3,G2 )
assume A17: ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G1 implies g . b1 Joins f . b2,f . b3,G2 )
assume A18: e Joins v,w,G1 ; :: thesis: g . b1 Joins f . b2,f . b3,G2
per cases then ( e Joins v,w,G3 or not e in the_Edges_of G3 ) by GLIB_006:72;
suppose A19: e Joins v,w,G3 ; :: thesis: g . b1 Joins f . b2,f . b3,G2
then e in the_Edges_of G3 by GLIB_000:def 13;
then A20: e in dom (F0 _E) by ;
not e in dom (e1 .--> e2)
proof
assume e in dom (e1 .--> e2) ; :: thesis: contradiction
then e in (dom (F0 _E)) /\ (dom (e1 .--> e2)) by ;
hence contradiction by A6, XBOOLE_0:def 7; :: thesis: verum
end;
then g . e = (F0 _E) . e by FUNCT_4:11;
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;
suppose A21: not e in the_Edges_of G3 ; :: thesis: g . b1 Joins f . b2,f . b3,G2
then A22: e = e1 by ;
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
.= g . e by ;
e2 DJoins v2,v4,G2 by ;
then g . e Joins v2,v4,G2 by ;
then A25: g . e Joins (F0 _V) . v1,(F0 _V) . v3,G2 by ;
( ( v = v1 & w = v3 ) or ( v = v3 & w = v1 ) ) by ;
hence g . e Joins f . v,f . w,G2 by ; :: thesis: verum
end;
end;
end;
then reconsider F = [f,g] as PGraphMapping of G1,G2 by Th8;
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 ; :: 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 ; :: 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 ; :: thesis: verum