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
A1: ( 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 `1_3 is Object of C by A1; :: thesis: verum