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