theorem Th23: :: CAT_4:23

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