the carrier of (Functors (C1,C2)) = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } by Def28;
hence Functors (C1,C2) is empty by Lm4; :: thesis: verum