let C be with_binary_products category; :: thesis: for a, b being Object of C holds
( a [x] b, pr1 (a,b), pr2 (a,b) is_product_of a,b & Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )
let a, b be Object of C; :: thesis: ( a [x] b, pr1 (a,b), pr2 (a,b) is_product_of a,b & Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )
set T = the categorical_product of a,b;
consider c being Object of C, p1 being Morphism of c,a, p2 being Morphism of c,b such that
A1: ( the categorical_product of a,b = [c,p1,p2] & Hom (c,a) <> {} & Hom (c,b) <> {} & c,p1,p2 is_product_of a,b ) by Def12;
thus ( a [x] b, pr1 (a,b), pr2 (a,b) is_product_of a,b & Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by A1; :: thesis: verum