reconsider f = (F _V) " as PartFunc of (the_Vertices_of G2),(the_Vertices_of G1) ;
reconsider g = (F _E) " as PartFunc of (the_Edges_of G2),(the_Edges_of G1) ;

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

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,G2 holds
g . e Joins f . v,f . w,G1

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f ) )
assume e in dom g ; :: thesis: ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f )
then e in rng (F _E) by FUNCT_1:33;
then ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) ) by Th6;
hence ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f ) by FUNCT_1:33; :: 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,G2 implies g . e Joins f . v,f . w,G1 )
assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G2 implies g . e Joins f . v,f . w,G1 )
then A1: ( e in rng (F _E) & v in rng (F _V) & w in rng (F _V) ) by FUNCT_1:33;
then consider e0 being object such that
A2: ( e0 in dom (F _E) & (F _E) . e0 = e ) by FUNCT_1:def 3;
consider v0 being object such that
A3: ( v0 in dom (F _V) & (F _V) . v0 = v ) by A1, FUNCT_1:def 3;
consider w0 being object such that
A4: ( w0 in dom (F _V) & (F _V) . w0 = w ) by A1, FUNCT_1:def 3;
A5: ( g . e = e0 & f . v = v0 & f . w = w0 ) by A2, A3, A4, FUNCT_1:34;
A6: F is semi-continuous ;
assume e Joins v,w,G2 ; :: thesis: g . e Joins f . v,f . w,G1
then (F _E) . e0 Joins (F _V) . v0,(F _V) . w0,G2 by A2, A3, A4;
hence g . e Joins f . v,f . w,G1 by A2, A3, A4, A5, A6; :: thesis: verum

end;

hence [((F _V) "),((F _E) ")] is PGraphMapping of G2,G1 by Th8; :: thesis: verum