theorem Th4: :: CAT_7:4

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