theorem Th23: :: CAT_7:23

for C being category
for a, b, c, d being Object of C
for f1 being Morphism of a,b
for f2 being Morphism of b,c
for f3 being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
f3 * (f2 * f1) = (f3 * f2) * f1