theorem Th21: :: CAT_1:25

for C being Category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)