:: deftheorem Def10 defines id CAT_1:def 12 :
for C being non empty non void reflexive with_identities CatStr
for a being Object of C
for b₃ being Morphism of a,a holds
( b₃ = id a iff for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b₃ = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b₃ (*) f = f ) ) );