let C be with_binary_products 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)) <> {} )
assume A1: ( Hom (c,a) <> {} & Hom (c,b) <> {} ) ; :: thesis: Hom (c,(a [x] b)) <> {}
( 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 Th42;
hence Hom (c,(a [x] b)) <> {} by Def10, A1; :: thesis: verum