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;

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

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

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