let C be Cartesian_category; :: thesis: for a being Object of C holds term a = term a,([1] C)
let a be Object of C; :: thesis: term a = term a,([1] C)
[1] C is terminal by Def9;
hence term a = term a,([1] C) by CAT_3:41; :: thesis: verum