:: deftheorem defines ?- CAT_2:def 8 :
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C holds S ?- c = (curry S) . (id c);