set C = Functors (C1,C2);
consider E being Functor of ((Functors (C1,C2)) [x] C1),C2 such that
A1:
E is covariant
and
A2:
for D being category
for F being Functor of (D [x] C1),C2 st F is covariant holds
ex H being Functor of D,(Functors (C1,C2)) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(Functors (C1,C2)) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
by Lm6;
A3:
Functors (C1,C2),E is_exponent_of C1,C2
by A1, A2, Def34;
C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2
by Th72;
hence
not C2 |^ C1 is empty
by CAT_7:15, A1, A3, Th73; verum