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 ( ( 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 ) )let e,
v,
w be
object ;
( 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 )
;
( 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;
verum end;
hence
[((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))] is PGraphMapping of G1,G3
by Th8; verum