set T = the categorical_product of c1,c2;
consider d being Object of C, p1 being Morphism of d,c1, p2 being Morphism of d,c2 such that
A2:
( the categorical_product of c1,c2 = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 )
by Def12;
thus
the categorical_product of c1,c2 `3_3 is Morphism of c1 [x] c2,c2
by A2; verum