theorem Th5: :: CAT_7:5

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