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 :: thesis: 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
( () . e in dom f & () . 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; :: thesis: 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
( () . e in dom f & () . 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; :: thesis: ( [( 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
( () . e in dom f & () . 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] ; :: thesis: ( 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
( () . e in dom f & () . 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 ; :: thesis: ( 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
( () . e in dom f & () . 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 ;
thus rng f c= the_Vertices_of G2 by ; :: thesis: ( dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( () . e in dom f & () . 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; :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom f & () . 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
( () . e in dom f & () . e in dom f ) ; :: thesis: 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

let e, v, w be object ; :: thesis: ( 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 ) ; :: thesis: ( 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 ) ; :: thesis: verum
end;
then reconsider F = [( the Vertex of G1 .--> the Vertex of G2),{}] as PGraphMapping of G1,G2 by Def8;
take F ; :: thesis: ( 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 ; :: thesis: ( 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 ) ; :: thesis: verum