theorem Th9: :: CAT_7:9

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