:: deftheorem defines Functors CLASSES5:def 34 :
for C, D being CategorySet holds Functors (C,D) = CatToSet (Functors ((SetToCat C),(SetToCat D)));