let C1, C2 be category; :: thesis: C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2
set T = the categorical_exponent of C1,C2;
consider C being category, E being Functor of (C [x] C1),C2 such that
A1: ( the categorical_exponent of C1,C2 = [C,E] & E is covariant & C,E is_exponent_of C1,C2 ) by Def35;
thus C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2 by A1; :: thesis: verum