:: deftheorem Def31 defines TargetMap CAT_6:def 31 :
for C being composable with_identities CategoryStr
for b₂ being Function of (Mor C),(Ob C) holds
( ( not C is empty implies ( b₂ = TargetMap C iff for f being Element of Mor C holds b₂ . f = cod f ) ) & ( C is empty implies ( b₂ = TargetMap C iff b₂ = {} ) ) );