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