let g be PVertexMapping of G2,G1; ( g = f " implies ( g is one-to-one & g is continuous & g is invertible ) )
assume A1:
g = f "
; ( g is one-to-one & g is continuous & g is invertible )
hence A2:
g is one-to-one
; ( g is continuous & g is invertible )
now 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,G2let v,
w,
e9 be
object ;
( 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
;
( 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
;
( 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
;
ex e being object st e Joins v,w,G2then
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;
e Joins v,w,G2thus
e Joins v,
w,
G2
by A3, A4, A5;
verum end;
hence
( g is continuous & g is invertible )
by A2, Th2; verum