theorem Th2: :: CAT_8:2

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