let C be Cartesian_category; :: thesis: for a, b, c being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds
Hom (c,(a [x] b)) <> {}
let a, b, c be Object of C; :: thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} implies Hom (c,(a [x] b)) <> {} )
A1: a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) by Def8;
( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19;
hence ( Hom (c,a) <> {} & Hom (c,b) <> {} implies Hom (c,(a [x] b)) <> {} ) by A1, CAT_3:55; :: thesis: verum