let A, B, C1, C2 be category; :: thesis: for E1 being Functor of (C1 [x] A),B
for E2 being Functor of (C2 [x] A),B st E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds
C1 ~= C2
let E1 be Functor of (C1 [x] A),B; :: thesis: for E2 being Functor of (C2 [x] A),B st E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds
C1 ~= C2
let E2 be Functor of (C2 [x] A),B; :: thesis: ( E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B implies C1 ~= C2 )
assume A1: E1 is covariant ; :: thesis: ( not E2 is covariant or not C1,E1 is_exponent_of A,B or not C2,E2 is_exponent_of A,B or C1 ~= C2 )
assume A2: E2 is covariant ; :: thesis: ( not C1,E1 is_exponent_of A,B or not C2,E2 is_exponent_of A,B or C1 ~= C2 )
assume A3: C1,E1 is_exponent_of A,B ; :: thesis: ( not C2,E2 is_exponent_of A,B or C1 ~= C2 )
assume A4: C2,E2 is_exponent_of A,B ; :: thesis: C1 ~= C2
ex F being Functor of C1,C2 ex G being Functor of C2,C1 st
( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 )

proof

consider F being Functor of C1,C2 such that
A5: ( F is covariant & E1 = E2 (*) (F [x] (id A)) & ( for H1 being Functor of C1,C2 st H1 is covariant & E1 = E2 (*) (H1 [x] (id A)) holds
F = H1 ) ) by A1, A2, A4, Def34;
consider G being Functor of C2,C1 such that
A6: ( G is covariant & E2 = E1 (*) (G [x] (id A)) & ( for H1 being Functor of C2,C1 st H1 is covariant & E2 = E1 (*) (H1 [x] (id A)) holds
G = H1 ) ) by A1, A2, A3, Def34;
take F ; :: thesis: ex G being Functor of C2,C1 st
( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 )
take G ; :: thesis: ( F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2 )
thus ( F is covariant & G is covariant ) by A5, A6; :: thesis: ( G (*) F = id C1 & F (*) G = id C2 )
consider H2 being Functor of C1,C1 such that
A7: ( H2 is covariant & E1 = E1 (*) (H2 [x] (id A)) & ( for H1 being Functor of C1,C1 st H1 is covariant & E1 = E1 (*) (H1 [x] (id A)) holds
H2 = H1 ) ) by A1, A3, Def34;
A8: G [x] (id A) is covariant by A6, Def22;
A9: F [x] (id A) is covariant by A5, Def22;
E1 = E1 (*) ((G [x] (id A)) (*) (F [x] (id A))) by A5, A6, A8, A9, A1, CAT_7:10
.= E1 (*) ((G (*) F) [x] ((id A) (*) (id A))) by A5, A6, Th50
.= E1 (*) ((G (*) F) [x] (id A)) by CAT_7:11 ;
then A10: G (*) F = H2 by A7, A5, A6, CAT_6:35;
E1 = E1 (*) (id (C1 [x] A)) by A1, CAT_7:11
.= E1 (*) ((id C1) [x] (id A)) by Th51 ;
hence G (*) F = id C1 by A7, A10; :: thesis: F (*) G = id C2
consider H3 being Functor of C2,C2 such that
A11: ( H3 is covariant & E2 = E2 (*) (H3 [x] (id A)) & ( for H1 being Functor of C2,C2 st H1 is covariant & E2 = E2 (*) (H1 [x] (id A)) holds
H3 = H1 ) ) by A2, A4, Def34;
E2 = E2 (*) ((F [x] (id A)) (*) (G [x] (id A))) by A2, A5, A6, A8, A9, CAT_7:10
.= E2 (*) ((F (*) G) [x] ((id A) (*) (id A))) by A5, A6, Th50
.= E2 (*) ((F (*) G) [x] (id A)) by CAT_7:11 ;
then A12: F (*) G = H3 by A11, A5, A6, CAT_6:35;
E2 = E2 (*) (id (C2 [x] A)) by A2, CAT_7:11
.= E2 (*) ((id C2) [x] (id A)) by Th51 ;
hence F (*) G = id C2 by A11, A12; :: thesis: verum

end;

hence C1,C2 are_isomorphic by CAT_6:def 28; :: thesis: verum