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

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

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

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

assume e in dom g ; :: thesis: ( (the_Source_of G1) . b_{1} in dom f & (the_Target_of G1) . b_{1} 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;

end;assume e in dom g ; :: thesis: ( (the_Source_of G1) . b

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;

end;

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_{1} in dom f & (the_Target_of G1) . b_{1} 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_{1} in dom f & (the_Target_of G1) . b_{1} 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;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