:: deftheorem Def21 defines . CAT_6:def 21 :
for C, D being with_identities CategoryStr
for F being Functor of C,D
for f being morphism of C holds
( ( not C is empty implies F . f = F . f ) & ( C is empty implies F . f = the Object of D ) );