reconsider f = (F2 _V) * (F1 _V) as PartFunc of (the_Vertices_of G1),(the_Vertices_of G3) ;
reconsider g = (F2 _E) * (F1 _E) as PartFunc of (the_Edges_of G1),(the_Edges_of G3) ;

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

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,G3

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ in dom f ) )
assume e in dom g ; :: thesis: ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ in dom f )
then A1: ( e in dom (F1 _E) & (F1 _E) . e in dom (F2 _E) ) by FUNCT_1:11;
then A2: ( (the_Source_of G1) . e in dom (F1 _V) & (the_Target_of G1) . e in dom (F1 _V) ) by Th5;
A3: ( (the_Source_of G2) . ((F1 _E) . e) in dom (F2 _V) & (the_Target_of G2) . ((F1 _E) . e) in dom (F2 _V) ) by A1, Th5;
e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A1, GLIB_000:def 13;
then (F1 _E) . e Joins (F1 _V) . ((the_Source_of G1) . e),(F1 _V) . ((the_Target_of G1) . e),G2 by A1, A2, Th4;

per cases then ( ( (F1 _V) . ((the_Source_of G1) . e) = (the_Source_of G2) . ((F1 _E) . e) & (F1 _V) . ((the_Target_of G1) . e) = (the_Target_of G2) . ((F1 _E) . e) ) or ( (F1 _V) . ((the_Source_of G1) . e) = (the_Target_of G2) . ((F1 _E) . e) & (F1 _V) . ((the_Target_of G1) . e) = (the_Source_of G2) . ((F1 _E) . e) ) ) by GLIB_000:def 13;

suppose ( (F1 _V) . ((the_Source_of G1) . e) = (the_Source_of G2) . ((F1 _E) . e) & (F1 _V) . ((the_Target_of G1) . e) = (the_Target_of G2) . ((F1 _E) . e) ) ; :: thesis: ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ in dom f )

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A2, A3, FUNCT_1:11; :: thesis: verum

end;

suppose ( (F1 _V) . ((the_Source_of G1) . e) = (the_Target_of G2) . ((F1 _E) . e) & (F1 _V) . ((the_Target_of G1) . e) = (the_Source_of G2) . ((F1 _E) . e) ) ; :: thesis: ( (the_Source_of G1) . b₁ in dom f & (the_Target_of G1) . b₁ in dom f )

hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A2, A3, FUNCT_1:11; :: thesis: verum

end;

end;

end;

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,G3 )
assume A4: ( 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,G3 )
then A5: ( e in dom (F1 _E) & (F1 _E) . e in dom (F2 _E) ) by FUNCT_1:11;
A6: ( v in dom (F1 _V) & (F1 _V) . v in dom (F2 _V) & w in dom (F1 _V) & (F1 _V) . w in dom (F2 _V) ) by A4, FUNCT_1:11;
( e Joins v,w,G1 implies (F1 _E) . e Joins (F1 _V) . v,(F1 _V) . w,G2 ) by A5, A6, Th4;
then A7: ( e Joins v,w,G1 implies (F2 _E) . ((F1 _E) . e) Joins (F2 _V) . ((F1 _V) . v),(F2 _V) . ((F1 _V) . w),G3 ) by A5, A6, Th4;
( (F2 _V) . ((F1 _V) . v) = f . v & (F2 _V) . ((F1 _V) . w) = f . w ) by A4, FUNCT_1:12;
hence ( e Joins v,w,G1 implies g . e Joins f . v,f . w,G3 ) by A4, A7, FUNCT_1:12; :: thesis: verum

end;

hence [((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))] is PGraphMapping of G1,G3 by Th8; :: thesis: verum