theorem :: GLIB_011:14
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is isomorphism & g is isomorphism holds
g * f is isomorphism