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; :: thesis: verum