:: deftheorem defines Funct CLASSES5:def 33 :
for C, D being CategorySet holds Funct (C,D) = Funct ((SetToCat C),(SetToCat D));