let C be Cartesian_category; :: thesis: for c, a, b being Object of C st Hom c,a <> {} & Hom c,b <> {} holds
Hom c,(a [x] b) <> {}
let c, a, b 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 Def9;
( Hom (a [x] b),a <> {} & Hom (a [x] b),b <> {} ) by Th21;
hence ( Hom c,a <> {} & Hom c,b <> {} implies Hom c,(a [x] b) <> {} ) by A1, CAT_3:60; :: thesis: verum