let C be Cartesian_category; :: thesis: C is with_finite_product
A1: [1] C is terminal by Def9;
for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st
( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 )

proof

let a, b be Object of C; :: thesis: ex c being Object of C ex p1, p2 being Morphism of C st
( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 )
take a [x] b ; :: thesis: ex p1, p2 being Morphism of C st
( dom p1 = a [x] b & dom p2 = a [x] b & cod p1 = a & cod p2 = b & a [x] b is_a_product_wrt p1,p2 )
take pr1 a,b ; :: thesis: ex p2 being Morphism of C st
( dom (pr1 a,b) = a [x] b & dom p2 = a [x] b & cod (pr1 a,b) = a & cod p2 = b & a [x] b is_a_product_wrt pr1 a,b,p2 )
take pr2 a,b ; :: thesis: ( dom (pr1 a,b) = a [x] b & dom (pr2 a,b) = a [x] b & cod (pr1 a,b) = a & cod (pr2 a,b) = b & a [x] b is_a_product_wrt pr1 a,b, pr2 a,b )
thus ( dom (pr1 a,b) = a [x] b & dom (pr2 a,b) = a [x] b & cod (pr1 a,b) = a & cod (pr2 a,b) = b & a [x] b is_a_product_wrt pr1 a,b, pr2 a,b ) by Def9, Th19, Th20; :: thesis: verum

end;

hence C is with_finite_product by A1, Th1; :: thesis: verum