now :: thesis: for v, w, e being object st v in dom (f ") & w in dom (f ") & e Joins v,w,G2 holds
ex e0 being object st e0 Joins (f ") . v,(f ") . w,G1

let v, w, e be object ; :: thesis: ( v in dom (f ") & w in dom (f ") & e Joins v,w,G2 implies ex e0 being object st e0 Joins (f ") . v,(f ") . w,G1 )
assume A1: ( v in dom (f ") & w in dom (f ") & e Joins v,w,G2 ) ; :: thesis: ex e0 being object st e0 Joins (f ") . v,(f ") . w,G1
then A2: ( v in rng f & w in rng f ) by FUNCT_1:33;
then consider v0 being object such that
A3: ( v0 in dom f & f . v0 = v ) by FUNCT_1:def 3;
consider w0 being object such that
A4: ( w0 in dom f & f . w0 = w ) by A2, FUNCT_1:def 3;
consider e0 being object such that
A5: e0 Joins v0,w0,G1 by A1, A3, A4, Th2;
take e0 = e0; :: thesis: e0 Joins (f ") . v,(f ") . w,G1
( (f ") . v = v0 & (f ") . w = w0 ) by A3, A4, FUNCT_1:34;
hence e0 Joins (f ") . v,(f ") . w,G1 by A5; :: thesis: verum

end;

hence f " is PVertexMapping of G2,G1 by Th1; :: thesis: verum