:: deftheorem Def32 defines IdMap CAT_6:def 32 :
for C being with_identities CategoryStr
for b₂ being Function of (Ob C),(Mor C) holds
( ( not C is empty implies ( b₂ = IdMap C iff for o being Element of Ob C holds b₂ . o = id- o ) ) & ( C is empty implies ( b₂ = IdMap C iff b₂ = {} ) ) );