set T = the categorical_product of C1,C2;
consider D being strict category, P1 being Functor of D,C1, P2 being Functor of D,C2 such that
A2: ( the categorical_product of C1,C2 = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 ) by Def18;
thus the categorical_product of C1,C2 `3_3 is Functor of (C1 [x] C2),C2 by A2; :: thesis: verum