theorem :: GLIB_011:13
for G1, G2, G3 being _Graph
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