theorem Th1: :: CAT_8:1

for C being associative composable CategoryStr
for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 holds
(f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3)