let C be Cartesian_category; :: thesis: C is with_finite_product
A1: 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 Def8, Th17, Th18; :: thesis: verum
end;
[1] C is terminal by Def8;
hence C is with_finite_product by A1, Th1; :: thesis: verum