let C1, C2, A, B be category; :: thesis: for P1 being Functor of A,C1
for P2 being Functor of A,C2
for Q1 being Functor of B,C1
for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let P1 be Functor of A,C1; :: thesis: for P2 being Functor of A,C2
for Q1 being Functor of B,C1
for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let P2 be Functor of A,C2; :: thesis: for Q1 being Functor of B,C1
for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let Q1 be Functor of B,C1; :: thesis: for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B
let Q2 be Functor of B,C2; :: thesis: ( P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 implies A ~= B )
assume A1: ( P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant ) ; :: thesis: ( not A,P1,P2 is_product_of C1,C2 or not B,Q1,Q2 is_product_of C1,C2 or A ~= B )
assume A2: A,P1,P2 is_product_of C1,C2 ; :: thesis: ( not B,Q1,Q2 is_product_of C1,C2 or A ~= B )
assume A3: B,Q1,Q2 is_product_of C1,C2 ; :: thesis: A ~= B
ex FF being Functor of A,B ex GG being Functor of B,A st
( FF is covariant & GG is covariant & GG (*) FF = id A & FF (*) GG = id B )

proof

consider FF being Functor of A,B such that
A4: ( FF is covariant & Q1 (*) FF = P1 & Q2 (*) FF = P2 & ( for H1 being Functor of A,B st H1 is covariant & Q1 (*) H1 = P1 & Q2 (*) H1 = P2 holds
FF = H1 ) ) by A1, A3, Def17;
consider GG being Functor of B,A such that
A5: ( GG is covariant & P1 (*) GG = Q1 & P2 (*) GG = Q2 & ( for H1 being Functor of B,A st H1 is covariant & P1 (*) H1 = Q1 & P2 (*) H1 = Q2 holds
GG = H1 ) ) by A1, A2, Def17;
take FF ; :: thesis: ex GG being Functor of B,A st
( FF is covariant & GG is covariant & GG (*) FF = id A & FF (*) GG = id B )
take GG ; :: thesis: ( FF is covariant & GG is covariant & GG (*) FF = id A & FF (*) GG = id B )
thus ( FF is covariant & GG is covariant ) by A4, A5; :: thesis: ( GG (*) FF = id A & FF (*) GG = id B )
set G11 = Q1 (*) FF;
set G12 = Q2 (*) FF;
consider H1 being Functor of A,A such that
A6: ( H1 is covariant & P1 (*) H1 = Q1 (*) FF & P2 (*) H1 = Q2 (*) FF & ( for H being Functor of A,A st H is covariant & P1 (*) H = Q1 (*) FF & P2 (*) H = Q2 (*) FF holds
H1 = H ) ) by A1, A4, A2, Def17;
A7: P1 (*) (GG (*) FF) = Q1 (*) FF by A1, A4, A5, CAT_7:10;
A8: P2 (*) (GG (*) FF) = Q2 (*) FF by A1, A4, A5, CAT_7:10;
A9: P1 (*) (id A) = Q1 (*) FF by A1, A4, CAT_7:11;
A10: P2 (*) (id A) = Q2 (*) FF by A1, A4, CAT_7:11;
thus GG (*) FF = H1 by A6, A7, A8, A4, A5, CAT_6:35
.= id A by A6, A9, A10 ; :: thesis: FF (*) GG = id B
set G21 = P1 (*) GG;
set G22 = P2 (*) GG;
consider H2 being Functor of B,B such that
A11: ( H2 is covariant & Q1 (*) H2 = P1 (*) GG & Q2 (*) H2 = P2 (*) GG & ( for H being Functor of B,B st H is covariant & Q1 (*) H = P1 (*) GG & Q2 (*) H = P2 (*) GG holds
H2 = H ) ) by A1, A5, A3, Def17;
A12: Q1 (*) (FF (*) GG) = P1 (*) GG by A1, A4, A5, CAT_7:10;
A13: Q2 (*) (FF (*) GG) = P2 (*) GG by A1, A4, A5, CAT_7:10;
A14: Q1 (*) (id B) = P1 (*) GG by A1, A5, CAT_7:11;
A15: Q2 (*) (id B) = P2 (*) GG by A1, A5, CAT_7:11;
thus FF (*) GG = H2 by A11, A12, A13, A4, A5, CAT_6:35
.= id B by A11, A14, A15 ; :: thesis: verum

end;

hence A ~= B by CAT_6:def 28; :: thesis: verum