set D = (C1 ->OrdC1) [|x|] (C2 ->OrdC1);
reconsider P1 = pr1 ((C1 ->OrdC1),(C2 ->OrdC1)) as Functor of ((C1 ->OrdC1) [|x|] (C2 ->OrdC1)),C1 ;
reconsider P2 = pr2 ((C1 ->OrdC1),(C2 ->OrdC1)) as Functor of ((C1 ->OrdC1) [|x|] (C2 ->OrdC1)),C2 ;
take [((C1 ->OrdC1) [|x|] (C2 ->OrdC1)),P1,P2] ; :: thesis: ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( [((C1 ->OrdC1) [|x|] (C2 ->OrdC1)),P1,P2] = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 )
( P1 is covariant & P2 is covariant ) by CAT_7:52;
hence ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( [((C1 ->OrdC1) [|x|] (C2 ->OrdC1)),P1,P2] = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 ) by Th47; :: thesis: verum