theorem Th5: :: CAT_8:5

for C being non empty with_identities CategoryStr
for f being morphism of C ex f1, f2 being morphism of C st
( f1 is identity & f2 is identity & f1 |> f & f |> f2 )