let C be Cartesian_category; :: thesis: for a, b, c, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a [x] b),(c [x] d)) <> {}
let a, b, c, d be Object of C; :: thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} implies Hom ((a [x] b),(c [x] d)) <> {} )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,d) <> {} ; :: thesis: Hom ((a [x] b),(c [x] d)) <> {}
Hom ((a [x] b),b) <> {} by Th19;
then A3: Hom ((a [x] b),d) <> {} by A2, CAT_1:24;
Hom ((a [x] b),a) <> {} by Th19;
then Hom ((a [x] b),c) <> {} by A1, CAT_1:24;
hence Hom ((a [x] b),(c [x] d)) <> {} by A3, Th23; :: thesis: verum