reconsider f = (F _V) | (the_Vertices_of H) as PartFunc of (the_Vertices_of H),(the_Vertices_of G2) by PARTFUN1:10;
reconsider g = (F _E) | (the_Edges_of H) as PartFunc of (the_Edges_of H),(the_Edges_of G2) by PARTFUN1:10;

now :: thesis: ( ( for e being object st e in dom g holds
( (the_Source_of H) . e in dom f & (the_Target_of H) . 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,H holds
g . e Joins f . v,f . w,G2 ) )

hereby :: thesis: for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,H holds
g . e Joins f . v,f . w,G2

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of H) . e in dom f & (the_Target_of H) . e in dom f ) )
assume e in dom g ; :: thesis: ( (the_Source_of H) . e in dom f & (the_Target_of H) . e in dom f )
then A1: ( e in dom (F _E) & e in the_Edges_of H ) by RELAT_1:57;
then ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by Th5;
then A2: ( (the_Source_of H) . e in dom (F _V) & (the_Target_of H) . e in dom (F _V) ) by A1, GLIB_000:def 32;
( (the_Source_of H) . e in the_Vertices_of H & (the_Target_of H) . e in the_Vertices_of H ) by A1, FUNCT_2:5;
hence ( (the_Source_of H) . e in dom f & (the_Target_of H) . e in dom f ) by A2, RELAT_1:57; :: thesis: verum

end;

let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e Joins v,w,H 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,H implies g . e Joins f . v,f . w,G2 )
then A3: ( e in dom (F _E) & e in the_Edges_of H & v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H ) by RELAT_1:57;
then A4: ( g . e = (F _E) . e & f . v = (F _V) . v & f . w = (F _V) . w ) by FUNCT_1:49;
assume A5: e Joins v,w,H ; :: thesis: g . e Joins f . v,f . w,G2
( v is set & w is set ) by TARSKI:1;
then e Joins v,w,G1 by A5, GLIB_000:72;
hence g . e Joins f . v,f . w,G2 by A3, A4, Th4; :: thesis: verum

end;

hence [((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))] is PGraphMapping of H,G2 by Th8; :: thesis: verum