let C be Cartesian_category; :: thesis: for a, c, b, d being Object of C st Hom a,c <> {} & Hom b,d <> {} holds
Hom (a [x] b),(c [x] d) <> {}
let a, c, b, d be Object of C; :: thesis: ( Hom a,c <> {} & Hom b,d <> {} implies Hom (a [x] b),(c [x] d) <> {} )
assume A1: ( Hom a,c <> {} & Hom b,d <> {} ) ; :: thesis: Hom (a [x] b),(c [x] d) <> {}
( Hom (a [x] b),a <> {} & Hom (a [x] b),b <> {} ) by Th21;
then ( Hom (a [x] b),c <> {} & Hom (a [x] b),d <> {} ) by A1, CAT_1:52;
hence Hom (a [x] b),(c [x] d) <> {} by Th25; :: thesis: verum