let g be PVertexMapping of G2,G1; :: thesis: ( g = f " implies ( g is one-to-one & g is continuous & g is invertible ) )
assume A1: g = f " ; :: thesis: ( g is one-to-one & g is continuous & g is invertible )
hence A2: g is one-to-one ; :: thesis: ( g is continuous & g is invertible )

now :: thesis: for v, w, e9 being object st v in dom g & w in dom g & e9 Joins g . v,g . w,G1 holds
ex e being object st e Joins v,w,G2

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

end;

hence ( g is continuous & g is invertible ) by A2, Th2; :: thesis: verum