theorem :: CAT_4:39

for C being Cartesian_category
for a, b, c, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a [x] b),(c [x] d)) <> {}