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

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

let v, w, e9 be object ; :: thesis: ( v in dom (g * f) & w in dom (g * f) & e9 DJoins (g * f) . v,(g * f) . w,G3 implies ex e being object st e DJoins v,w,G1 )
assume A2: ( v in dom (g * f) & w in dom (g * f) & e9 DJoins (g * f) . v,(g * f) . w,G3 ) ; :: thesis: ex e being object st e DJoins v,w,G1
then e9 DJoins g . (f . v),(g * f) . w,G3 by FUNCT_1:12;
then A3: e9 DJoins 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 DJoins f . v,f . w,G2 by A1, A3;
( v in dom f & w in dom f ) by A2, FUNCT_1:11;
then consider e being object such that
A5: e DJoins v,w,G1 by A1, A4;
take e = e; :: thesis: e DJoins v,w,G1
thus e DJoins v,w,G1 by A5; :: thesis: verum

end;

hence g * f is Dcontinuous ; :: thesis: verum