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),{}];

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

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

( (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 ) )

then reconsider F = [( the Vertex of G1 .--> the Vertex of G2),{}] as PGraphMapping of G1,G2 by Def8;( [( 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; :: 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

( (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; :: 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

( (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] ; :: 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

( (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 ; :: 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

( (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; :: 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

( (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; :: thesis: ( ( 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 ) ; :: 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;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

( (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; :: 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

( (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] ; :: 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

( (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 ; :: 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

( (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; :: 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

( (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; :: thesis: ( ( 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 ) ; :: 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

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