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 the categorical_exponent of C1,C2 `1 is category by A1; :: thesis: verum