theorem Th8: :: CAT_7:8

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