theorem Th4: :: CAT_8:4

for C being composable with_identities CategoryStr
for f1, f2 being morphism of C st f1 |> f2 holds
( ( f1 is identity implies f1 (*) f2 = f2 ) & ( f2 is identity implies f1 (*) f2 = f1 ) )