let C be with_binary_products category; :: thesis: for a, b, c, d being Object of C st Hom (a,b) <> {} & Hom (c,d) <> {} holds
Hom ((a [x] c),(b [x] d)) <> {}
let a, b, c, d be Object of C; :: thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} implies Hom ((a [x] c),(b [x] d)) <> {} )
assume A1: Hom (a,b) <> {} ; :: thesis: ( not Hom (c,d) <> {} or Hom ((a [x] c),(b [x] d)) <> {} )
assume A2: Hom (c,d) <> {} ; :: thesis: Hom ((a [x] c),(b [x] d)) <> {}
A3: ( a [x] c, pr1 (a,c), pr2 (a,c) is_product_of a,c & Hom ((a [x] c),a) <> {} & Hom ((a [x] c),c) <> {} ) by Th42;
A4: ( b [x] d, pr1 (b,d), pr2 (b,d) is_product_of b,d & Hom ((b [x] d),b) <> {} & Hom ((b [x] d),d) <> {} ) by Th42;
( Hom ((a [x] c),b) <> {} & Hom ((a [x] c),d) <> {} ) by A3, A1, A2, CAT_7:22;
hence Hom ((a [x] c),(b [x] d)) <> {} by A4, Def10; :: thesis: verum