set G1 = F1 (*) (pr1 (C1,C2));
set G2 = F2 (*) (pr2 (C1,C2));
A2: D1 [x] D2, pr1 (D1,D2), pr2 (D1,D2) is_product_of D1,D2 by Th48;
( F1 (*) (pr1 (C1,C2)) is covariant & F2 (*) (pr2 (C1,C2)) is covariant ) by A1, CAT_6:35;
then consider H2 being Functor of (C1 [x] C2),(D1 [x] D2) such that
A3: ( H2 is covariant & (pr1 (D1,D2)) (*) H2 = F1 (*) (pr1 (C1,C2)) & (pr2 (D1,D2)) (*) H2 = F2 (*) (pr2 (C1,C2)) & ( for H1 being Functor of (C1 [x] C2),(D1 [x] D2) st H1 is covariant & (pr1 (D1,D2)) (*) H1 = F1 (*) (pr1 (C1,C2)) & (pr2 (D1,D2)) (*) H1 = F2 (*) (pr2 (C1,C2)) holds
H2 = H1 ) ) by A2, Def17;
thus ex H being Functor of (C1 [x] C2),(D1 [x] D2) st
( H is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) H & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) H ) by A3; :: thesis: for b₁, b₂ being Functor of (C1 [x] C2),(D1 [x] D2) st b₁ is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b₁ & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b₁ & b₂ is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b₂ & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b₂ holds
b₁ = b₂
let H3, H4 be Functor of (C1 [x] C2),(D1 [x] D2); :: thesis: ( H3 is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) H3 & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) H3 & H4 is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) H4 & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) H4 implies H3 = H4 )
assume A4: ( H3 is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) H3 & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) H3 ) ; :: thesis: ( not H4 is covariant or not F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) H4 or not F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) H4 or H3 = H4 )
assume A5: ( H4 is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) H4 & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) H4 ) ; :: thesis: H3 = H4
thus H3 = H2 by A4, A3
.= H4 by A5, A3 ; :: thesis: verum