:: deftheorem Def8 defines with_identities CAT_1:def 10 :
for C being non empty non void CatStr holds
( C is with_identities iff for a being Element of C ex i being Morphism of a,a st
for b being Element of C holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) );