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

reconsider f = the Vertex of G1 .--> the Vertex of G2 as Function ;
reconsider g = {} as Function ;
take f = f; :: thesis:
take g = g; :: thesis:
thus [( the Vertex of G1 .--> the Vertex of G2),{}] = [f,g] ; :: thesis:
dom f = { the Vertex of G1} by A1;
hence dom f c= the_Vertices_of G1 ; :: thesis:
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 = {} & rng g = {} ) ;
hence ( dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 ) by XBOOLE_1:2; :: thesis:
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:
let e, v, w be object ; :: thesis:
assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis:
hence ( e Joins v,w,G1 implies g . e Joins f . v,f . w,G2 ) ; :: thesis:

end;