let C1, C2, D be category; :: thesis: for P1 being Functor of D,C1
for P2 being Functor of D,C2 st P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 holds
D,P2,P1 is_product_of C2,C1
let P1 be Functor of D,C1; :: thesis: for P2 being Functor of D,C2 st P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 holds
D,P2,P1 is_product_of C2,C1
let P2 be Functor of D,C2; :: thesis: ( P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 implies D,P2,P1 is_product_of C2,C1 )
assume A1: ( P1 is covariant & P2 is covariant ) ; :: thesis: ( not D,P1,P2 is_product_of C1,C2 or D,P2,P1 is_product_of C2,C1 )
assume A2: D,P1,P2 is_product_of C1,C2 ; :: thesis: D,P2,P1 is_product_of C2,C1
for D1 being category
for G1 being Functor of D1,C2
for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant holds
ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )

proof

let D1 be category; :: thesis: for G1 being Functor of D1,C2
for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant holds
ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
let G1 be Functor of D1,C2; :: thesis: for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant holds
ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
let G2 be Functor of D1,C1; :: thesis: ( G1 is covariant & G2 is covariant implies ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) ) )
assume A3: ( G1 is covariant & G2 is covariant ) ; :: thesis: ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
consider H being Functor of D1,D such that
A4: ( H is covariant & P1 (*) H = G2 & P2 (*) H = G1 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G2 & P2 (*) H1 = G1 holds
H = H1 ) ) by A3, A2, A1, Def17;
take H ; :: thesis: ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
thus ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 ) by A4; :: thesis: for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1
let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 implies H = H1 )
assume ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 ) ; :: thesis: H = H1
hence H = H1 by A4; :: thesis: verum

end;

hence D,P2,P1 is_product_of C2,C1 by A1, Def17; :: thesis: verum