consider d being Object of C, p1 being Morphism of d,c1, p2 being Morphism of d,c2 such that
A1: ( Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 ) by Def11;
take [d,p1,p2] ; :: thesis: ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st
( [d,p1,p2] = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 )
thus ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st
( [d,p1,p2] = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 ) by A1; :: thesis: verum