let C1, C2 be category; :: thesis: Functors (C1,C2) ~= C2 |^ C1

per cases ( C1 is empty or ( C2 is empty & not C1 is empty ) or ( not C1 is empty & not C2 is empty ) ) ;

suppose C1 is empty ; :: thesis: Functors (C1,C2) ~= C2 |^ C1

hence Functors (C1,C2) ~= C2 |^ C1 by Th28; :: thesis: verum

end;

suppose ( C2 is empty & not C1 is empty ) ; :: thesis: Functors (C1,C2) ~= C2 |^ C1

hence Functors (C1,C2) ~= C2 |^ C1 by CAT_7:13; :: thesis: verum

end;

suppose A1: ( not C1 is empty & not C2 is empty ) ; :: thesis: Functors (C1,C2) ~= C2 |^ C1

set C = Functors (C1,C2);
consider E being Functor of ((Functors (C1,C2)) [x] C1),C2 such that
A2: E is covariant and
A3: 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 A1, Lm6;
A4: Functors (C1,C2),E is_exponent_of C1,C2 by A2, A3, Def34;
C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2 by Th72;
hence Functors (C1,C2) ~= C2 |^ C1 by A2, A4, Th73; :: thesis: verum

end;

end;