:: deftheorem defines . CAT_1:def 23 :
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . c = (Obj T) . c;