now :: thesis: 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,G3

let v, w, e be object ; :: thesis: ( 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 ) ; :: thesis: ex e9 being object st e9 Joins (g * f) . v,(g * f) . w,G3
then 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; :: thesis: 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; :: thesis: verum

end;

hence f * g is PVertexMapping of G1,G3 by Th1; :: thesis: verum