let G1, G2 be _Graph; :: thesis:
let f be PVertexMapping of G1,G2; :: thesis:
let E1 be RepEdgeSelection of G1; :: thesis:
let E2 be RepEdgeSelection of G2; :: thesis:
defpred S₁[ object , object ] means ex v, w being object st
( v in dom f & w in dom f & $1 in E1 & $2 in E2 & $1 Joins v,w,G1 & $2 Joins f . v,f . w,G2 );
A1: for e1, e2, e3 being object st e1 in E1 /\ (G1 .edgesBetween (dom f)) & S₁[e1,e2] & S₁[e1,e3] holds
e2 = e3

let e1, e2, e3 be object ; :: thesis:
assume A2: ( e1 in E1 /\ (G1 .edgesBetween (dom f)) & S₁[e1,e2] & S₁[e1,e3] ) ; :: thesis:
then consider v2, w2 being object such that
A3: ( v2 in dom f & w2 in dom f & e1 in E1 & e2 in E2 & e1 Joins v2,w2,G1 & e2 Joins f . v2,f . w2,G2 ) ;
consider v3, w3 being object such that
A4: ( v3 in dom f & w3 in dom f & e1 in E1 & e3 in E2 & e1 Joins v3,w3,G1 & e3 Joins f . v3,f . w3,G2 ) by A2;
( ( v2 = v3 & w2 = w3 ) or ( v2 = w3 & w2 = v3 ) ) by A3, A4, GLIB_000:15;
then ( ( f . v2 = f . v3 & f . w2 = f . w3 ) or ( f . v2 = f . w3 & f . w2 = f . v3 ) ) ;
then A5: e3 Joins f . v2,f . w2,G2 by A4, GLIB_000:14;
then consider e0 being object such that
( e0 Joins f . v2,f . w2,G2 & e0 in E2 ) and
A6: for e9 being object st e9 Joins f . v2,f . w2,G2 & e9 in E2 holds
e9 = e0 by GLIB_009:def 5;
( e2 = e0 & e3 = e0 ) by A3, A4, A5, A6;
hence e2 = e3 ; :: thesis:

end;

A7: for e1 being object st e1 in E1 /\ (G1 .edgesBetween (dom f)) holds
ex e2 being object st S₁[e1,e2]

end;

consider g being Function such that
A13: dom g = E1 /\ (G1 .edgesBetween (dom f)) and
A14: for e1 being object st e1 in E1 /\ (G1 .edgesBetween (dom f)) holds
S₁[e1,g . e1] from FUNCT_1:sch 2(A1, A7);
for y being object st y in rng g holds
y in E2 /\ (G2 .edgesBetween (rng f))

let y be object ; :: thesis:
assume y in rng g ; :: thesis:
then consider x being object such that
A15: ( x in dom g & g . x = y ) by FUNCT_1:def 3;
consider v, w being object such that
A16: ( v in dom f & w in dom f & x in E1 & g . x in E2 ) and
A17: ( x Joins v,w,G1 & g . x Joins f . v,f . w,G2 ) by A13, A14, A15;
( f . v in rng f & f . w in rng f ) by A16, FUNCT_1:3;
then ( (the_Source_of G2) . y in rng f & (the_Target_of G2) . y in rng f & y in the_Edges_of G2 ) by A15, A17, GLIB_000:def 13;
then y in G2 .edgesBetween (rng f) by GLIB_000:31;
hence y in E2 /\ (G2 .edgesBetween (rng f)) by A15, A16, XBOOLE_0:def 4; :: thesis:

end;

let e be object ; :: thesis:
assume e in dom g ; :: thesis:
then consider v, w being object such that
A19: ( v in dom f & w in dom f & e in E1 & g . e in E2 & e Joins v,w,G1 & g . e Joins f . v,f . w,G2 ) by A13, A14;
thus ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A19, GLIB_000:def 13; :: thesis:

end;

let e, v, w be object ; :: thesis:
assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis:
then consider v0, w0 being object such that
A20: ( v0 in dom f & w0 in dom f & e in E1 & g . e in E2 & e Joins v0,w0,G1 & g . e Joins f . v0,f . w0,G2 ) by A13, A14;
assume e Joins v,w,G1 ; :: thesis:
then ( ( v = v0 & w = w0 ) or ( v = w0 & w = v0 ) ) by A20, GLIB_000:15;
hence g . e Joins f . v,f . w,G2 by A20, GLIB_000:14; :: thesis:

end;

then reconsider F = [f,g] as PGraphMapping of G1,G2 by GLIB_010:8;
take F ; :: thesis:
thus ( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) ) by A13, A18; :: thesis: