theorem :: CLASSES5:90

for C, D being CategorySet holds
( Obj (Functors (C,D)) = Funct ((SetToCat C),(SetToCat D)) & Mor (Functors (C,D)) = NatTrans ((SetToCat C),(SetToCat D)) ) by NATTRA_1:def 17;