theorem :: CAT_1:18
for C being Category
for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f by Def6;