reconsider f = (the_Vertices_of H) |` (F _V) as PartFunc of (the_Vertices_of G1),(the_Vertices_of H) by PARTFUN1:12;

reconsider g = (the_Edges_of H) |` (F _E) as PartFunc of (the_Edges_of G1),(the_Edges_of H) by PARTFUN1:12;

reconsider g = (the_Edges_of H) |` (F _E) as PartFunc of (the_Edges_of G1),(the_Edges_of H) by PARTFUN1:12;

now :: 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,H ) )

assume A8: ( 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,H )

then A9: ( e in dom (F _E) & (F _E) . e in the_Edges_of H & v in dom (F _V) & (F _V) . v in the_Vertices_of H & w in dom (F _V) & (F _V) . w in the_Vertices_of H ) by FUNCT_1:54;

then ( e Joins v,w,G1 implies (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) by Th4;

then A10: ( e Joins v,w,G1 implies (F _E) . e Joins (F _V) . v,(F _V) . w,H ) by A9, GLIB_000:73;

( g . e = (F _E) . e & f . v = (F _V) . v & f . w = (F _V) . w ) by A8, FUNCT_1:53;

hence ( e Joins v,w,G1 implies g . e Joins f . v,f . w,H ) by A10; :: thesis: verum

end;

hence
[((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))] is PGraphMapping of G1,H
by Th8; :: thesis: verum( (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,H ) )

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,G1 holds

g . e Joins f . v,f . w,H

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,H )g . e Joins f . v,f . w,H

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) )

assume e in dom g ; :: thesis: ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f )

then A1: ( e in dom (F _E) & (F _E) . e in the_Edges_of H ) by FUNCT_1:54;

A2: (F _E) . e Joins (the_Source_of H) . ((F _E) . e),(the_Target_of H) . ((F _E) . e),H by A1, GLIB_000:def 13;

then A3: (F _E) . e Joins (the_Source_of H) . ((F _E) . e),(the_Target_of H) . ((F _E) . e),G2 by GLIB_000:72;

A4: ( (the_Source_of H) . ((F _E) . e) in the_Vertices_of H & (the_Target_of H) . ((F _E) . e) in the_Vertices_of H ) by A2, GLIB_000:13;

A5: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A1, GLIB_000:def 13;

A6: ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by A1, Th5;

then A7: (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e),G2 by A1, A5, Th4;

( (F _V) . ((the_Source_of G1) . e) in the_Vertices_of H & (F _V) . ((the_Target_of G1) . e) in the_Vertices_of H )

end;assume e in dom g ; :: thesis: ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f )

then A1: ( e in dom (F _E) & (F _E) . e in the_Edges_of H ) by FUNCT_1:54;

A2: (F _E) . e Joins (the_Source_of H) . ((F _E) . e),(the_Target_of H) . ((F _E) . e),H by A1, GLIB_000:def 13;

then A3: (F _E) . e Joins (the_Source_of H) . ((F _E) . e),(the_Target_of H) . ((F _E) . e),G2 by GLIB_000:72;

A4: ( (the_Source_of H) . ((F _E) . e) in the_Vertices_of H & (the_Target_of H) . ((F _E) . e) in the_Vertices_of H ) by A2, GLIB_000:13;

A5: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A1, GLIB_000:def 13;

A6: ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by A1, Th5;

then A7: (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e),G2 by A1, A5, Th4;

( (F _V) . ((the_Source_of G1) . e) in the_Vertices_of H & (F _V) . ((the_Target_of G1) . e) in the_Vertices_of H )

proof
end;

hence
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f )
by A6, FUNCT_1:54; :: thesis: verumper cases
( ( (F _V) . ((the_Source_of G1) . e) = (the_Source_of H) . ((F _E) . e) & (F _V) . ((the_Target_of G1) . e) = (the_Target_of H) . ((F _E) . e) ) or ( (F _V) . ((the_Source_of G1) . e) = (the_Target_of H) . ((F _E) . e) & (F _V) . ((the_Target_of G1) . e) = (the_Source_of H) . ((F _E) . e) ) )
by A3, A7, GLIB_000:15;

end;

suppose
( (F _V) . ((the_Source_of G1) . e) = (the_Source_of H) . ((F _E) . e) & (F _V) . ((the_Target_of G1) . e) = (the_Target_of H) . ((F _E) . e) )
; :: thesis: ( (F _V) . ((the_Source_of G1) . e) in the_Vertices_of H & (F _V) . ((the_Target_of G1) . e) in the_Vertices_of H )

hence
( (F _V) . ((the_Source_of G1) . e) in the_Vertices_of H & (F _V) . ((the_Target_of G1) . e) in the_Vertices_of H )
by A4; :: thesis: verum

end;suppose
( (F _V) . ((the_Source_of G1) . e) = (the_Target_of H) . ((F _E) . e) & (F _V) . ((the_Target_of G1) . e) = (the_Source_of H) . ((F _E) . e) )
; :: thesis: ( (F _V) . ((the_Source_of G1) . e) in the_Vertices_of H & (F _V) . ((the_Target_of G1) . e) in the_Vertices_of H )

hence
( (F _V) . ((the_Source_of G1) . e) in the_Vertices_of H & (F _V) . ((the_Target_of G1) . e) in the_Vertices_of H )
by A4; :: thesis: verum

end;assume A8: ( 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,H )

then A9: ( e in dom (F _E) & (F _E) . e in the_Edges_of H & v in dom (F _V) & (F _V) . v in the_Vertices_of H & w in dom (F _V) & (F _V) . w in the_Vertices_of H ) by FUNCT_1:54;

then ( e Joins v,w,G1 implies (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) by Th4;

then A10: ( e Joins v,w,G1 implies (F _E) . e Joins (F _V) . v,(F _V) . w,H ) by A9, GLIB_000:73;

( g . e = (F _E) . e & f . v = (F _V) . v & f . w = (F _V) . w ) by A8, FUNCT_1:53;

hence ( e Joins v,w,G1 implies g . e Joins f . v,f . w,H ) by A10; :: thesis: verum