theorem Th23: :: CAT_6:23

for C being non empty with_identities CategoryStr
for f, f1 being morphism of C
for o being Object of C st f = o holds
( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f )