:: deftheorem Def17 defines idm ALTCAT_1:def 17 :
for C being non empty with_units AltCatStr
for o being Object of C
for b₃ being Morphism of o,o holds
( b₃ = idm o iff for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * b₃ = a );