let G3, G4 be _Graph; :: thesis:
let v1, v3 be Vertex of G3; :: thesis:
let v2, v4 be Vertex of G4; :: thesis:
let e1, e2 be object ; :: thesis:
let G1 be addEdge of G3,v1,e1,v3; :: thesis:
let G2 be addEdge of G4,v2,e2,v4; :: thesis:
let F0 be PGraphMapping of G3,G4; :: thesis:
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:
( 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:

hereby :: thesis:

let e be object ; :: thesis:
assume A11: e in dom g ; :: thesis:
then A12: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;

per cases by GLIB_006:72;

suppose A13: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G3 ; :: thesis:

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:

end;

suppose A16: not e in the_Edges_of G3 ; :: thesis:

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:

end;

let e, v, w be object ; :: thesis:
assume A17: ( e in dom g & v in dom f & w in dom f ) ; :: thesis:
assume A18: e Joins v,w,G1 ; :: thesis:

per cases by GLIB_006:72;

suppose A19: e Joins v,w,G3 ; :: thesis:

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)

proof

assume e in dom (e1 .--> e2) ; :: thesis:
then e in (dom (F0 _E)) /\ (dom (e1 .--> e2)) by A20, XBOOLE_0:def 4;
hence contradiction by A6, XBOOLE_0:def 7; :: thesis:

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:

end;

suppose A21: not e in the_Edges_of G3 ; :: thesis:

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:

end;

then reconsider F = [f,g] as PGraphMapping of G1,G2 by Th8;
take F ; :: thesis:
thus F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] ; :: thesis:
thus ( F0 is total implies F is total ) by A2, A5, GLIB_006:def 11; :: thesis:
thus ( F0 is onto implies F is onto ) by A2, A9, GLIB_006:def 11; :: thesis:
thus ( F0 is one-to-one implies F is one-to-one ) by A8, FUNCT_4:92; :: thesis: