now for v, w, e being object st v in dom (g * f) & w in dom (g * f) & e Joins v,w,G1 holds
ex e9 being object st e9 Joins (g * f) . v,(g * f) . w,G3let v,
w,
e be
object ;
( v in dom (g * f) & w in dom (g * f) & e Joins v,w,G1 implies ex e9 being object st e9 Joins (g * f) . v,(g * f) . w,G3 )assume A1:
(
v in dom (g * f) &
w in dom (g * f) &
e Joins v,
w,
G1 )
;
ex e9 being object st e9 Joins (g * f) . v,(g * f) . w,G3then A2:
(
v in dom f &
w in dom f &
f . v in dom g &
f . w in dom g )
by FUNCT_1:11;
then consider e8 being
object such that A3:
e8 Joins f . v,
f . w,
G2
by A1, Th1;
consider e9 being
object such that A4:
e9 Joins g . (f . v),
g . (f . w),
G3
by A2, A3, Th1;
take e9 =
e9;
e9 Joins (g * f) . v,(g * f) . w,G3
(
(g * f) . v = g . (f . v) &
(g * f) . w = g . (f . w) )
by A1, FUNCT_1:12;
hence
e9 Joins (g * f) . v,
(g * f) . w,
G3
by A4;
verum end;
hence
f * g is PVertexMapping of G1,G3
by Th1; verum