set v1 = the Vertex of G1;
set v2 = the Vertex of G2;
set f = the Vertex of G1 .--> the Vertex of G2;
the Vertex of G1 .--> the Vertex of G2 = { the Vertex of G1} --> the Vertex of G2
by FUNCOP_1:def 9;
then reconsider f = the Vertex of G1 .--> the Vertex of G2 as one-to-one PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) ;
then reconsider f = f as PVertexMapping of G1,G2 by Def1;
take
f
; ( not f is empty & f is one-to-one & f is directed & f is continuous & f is Dcontinuous )
thus
( not f is empty & f is one-to-one )
; ( f is directed & f is continuous & f is Dcontinuous )
thus
f is directed
( f is continuous & f is Dcontinuous )proof
let v,
w,
e be
object ;
GLIB_011:def 2 ( v in dom f & w in dom f & e DJoins v,w,G1 implies ex e9 being object st e9 DJoins f . v,f . w,G2 )
assume A2:
(
v in dom f &
w in dom f &
e DJoins v,
w,
G1 )
;
ex e9 being object st e9 DJoins f . v,f . w,G2
then
(
v = the
Vertex of
G1 &
w = the
Vertex of
G1 )
by FUNCOP_1:75;
then
e Joins the
Vertex of
G1, the
Vertex of
G1,
G1
by A2, GLIB_000:16;
hence
ex
e9 being
object st
e9 DJoins f . v,
f . w,
G2
by GLIB_000:18;
verum
end;
thus
f is continuous
f is Dcontinuous
thus
f is Dcontinuous
verumproof
let v,
w,
e9 be
object ;
GLIB_011:def 4 ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 implies ex e being object st e DJoins v,w,G1 )
assume A4:
(
v in dom f &
w in dom f &
e9 DJoins f . v,
f . w,
G2 )
;
ex e being object st e DJoins v,w,G1
then
(
v = the
Vertex of
G1 &
w = the
Vertex of
G1 )
by FUNCOP_1:75;
then
e9 Joins f . the
Vertex of
G1,
f . the
Vertex of
G1,
G2
by A4, GLIB_000:16;
hence
ex
e being
object st
e DJoins v,
w,
G1
by GLIB_000:18;
verum
end;