theorem :: CAT_4:16

for C being Cartesian_category
for a being Object of C holds Hom (a,([1] C)) = {(term a)}