theorem :: CLASSES5:65

for C, D being Category
for F being Functor of C,D holds F c= [: the carrier' of C, the carrier' of D:] ;