reconsider X2 = [[{},{}],{}] as set by TARSKI:1;
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;
then
( the carrier of (Functors (C1,C2)) = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of (Functors (C1,C2)) : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {[[X2,X2],X2]} )
by Lm5;
hence
( not Functors (C1,C2) is empty & Functors (C1,C2) is trivial )
; verum