set v1 = the Vertex of G1;
set v2 = the Vertex of G2;
set h = the Vertex of G1 .--> the Vertex of G2;
A1:
the Vertex of G1 .--> the Vertex of G2 = { the Vertex of G1} --> the Vertex of G2
by FUNCOP_1:def 9;
set F = [( the Vertex of G1 .--> the Vertex of G2),{}];
now ex f, g being Function st
( [( the Vertex of G1 .--> the Vertex of G2),{}] = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) )reconsider f = the
Vertex of
G1 .--> the
Vertex of
G2 as
Function ;
reconsider g =
{} as
Function ;
take f =
f;
ex g being Function st
( [( the Vertex of G1 .--> the Vertex of G2),{}] = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) )take g =
g;
( [( the Vertex of G1 .--> the Vertex of G2),{}] = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) )thus
[( the Vertex of G1 .--> the Vertex of G2),{}] = [f,g]
;
( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) )
dom f = { the Vertex of G1}
by A1;
hence
dom f c= the_Vertices_of G1
;
( rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) )A2:
rng f c= { the Vertex of G2}
by A1, FUNCOP_1:13;
thus
rng f c= the_Vertices_of G2
by A2, XBOOLE_1:1;
( dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) )
(
dom g = {} &
rng g = {} )
;
hence
(
dom g c= the_Edges_of G1 &
rng g c= the_Edges_of G2 )
by XBOOLE_1:2;
( ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) )thus
for
e being
object st
e in dom g holds
(
(the_Source_of G1) . e in dom f &
(the_Target_of G1) . e in dom f )
;
for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2let e,
v,
w be
object ;
( e in dom g & v in dom f & w in dom f & e Joins v,w,G1 implies g . e Joins f . v,f . w,G2 )assume
(
e in dom g &
v in dom f &
w in dom f )
;
( e Joins v,w,G1 implies g . e Joins f . v,f . w,G2 )hence
(
e Joins v,
w,
G1 implies
g . e Joins f . v,
f . w,
G2 )
;
verum end;
then reconsider F = [( the Vertex of G1 .--> the Vertex of G2),{}] as PGraphMapping of G1,G2 by Def8;
take
F
; ( not F is empty & F is one-to-one & F is directed & F is semi-Dcontinuous & F is semi-continuous )
thus
not F is empty
; ( F is one-to-one & F is directed & F is semi-Dcontinuous & F is semi-continuous )
thus
( F is one-to-one & F is directed & F is semi-Dcontinuous & F is semi-continuous )
; verum