let G1, G2, G3 be _Graph; :: thesis: for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is continuous & g is continuous holds
g * f is continuous
let f be PVertexMapping of G1,G2; :: thesis: for g being PVertexMapping of G2,G3 st f is continuous & g is continuous holds
g * f is continuous
let g be PVertexMapping of G2,G3; :: thesis: ( f is continuous & g is continuous implies g * f is continuous )
assume A1: ( f is continuous & g is continuous ) ; :: thesis: g * f is continuous

now :: thesis: for v, w, e9 being object st v in dom (g * f) & w in dom (g * f) & e9 Joins (g * f) . v,(g * f) . w,G3 holds
ex e being object st e Joins v,w,G1

let v, w, e9 be object ; :: thesis: ( v in dom (g * f) & w in dom (g * f) & e9 Joins (g * f) . v,(g * f) . w,G3 implies ex e being object st e Joins v,w,G1 )
assume A2: ( v in dom (g * f) & w in dom (g * f) & e9 Joins (g * f) . v,(g * f) . w,G3 ) ; :: thesis: ex e being object st e Joins v,w,G1
then e9 Joins g . (f . v),(g * f) . w,G3 by FUNCT_1:12;
then A3: e9 Joins g . (f . v),g . (f . w),G3 by A2, FUNCT_1:12;
( f . v in dom g & f . w in dom g ) by A2, FUNCT_1:11;
then consider e8 being object such that
A4: e8 Joins f . v,f . w,G2 by A1, A3, Th2;
( v in dom f & w in dom f ) by A2, FUNCT_1:11;
then consider e being object such that
A5: e Joins v,w,G1 by A1, A4, Th2;
take e = e; :: thesis: e Joins v,w,G1
thus e Joins v,w,G1 by A5; :: thesis: verum

end;

hence g * f is continuous by Th2; :: thesis: verum