let C be Cartesian_category; :: thesis: for a being Object of C holds Hom (a,([1] C)) = {(term a)}
let a be Object of C; :: thesis: Hom (a,([1] C)) = {(term a)}
for f2 being Morphism of a, [1] C holds term a = f2 by Th12;
hence Hom (a,([1] C)) = {(term a)} by Th13, CAT_1:8; :: thesis: verum