A1: 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;
set F = the covariant Functor of C1,C2;
A2: the covariant Functor of C1,C2 is_natural_transformation_of the covariant Functor of C1,C2, the covariant Functor of C1,C2 by Th61;
the covariant Functor of C1,C2 is_naturally_transformable_to the covariant Functor of C1,C2 by Th61;
then reconsider t = the covariant Functor of C1,C2 as natural_transformation of the covariant Functor of C1,C2, the covariant Functor of C1,C2 by A2, Def26;
the covariant Functor of C1,C2 is_naturally_transformable_to the covariant Functor of C1,C2 by Th61;
then [[ the covariant Functor of C1,C2, the covariant Functor of C1,C2],t] in the carrier of (Functors (C1,C2)) by A1;
hence not Functors (C1,C2) is empty ; :: thesis: verum