let C be Cartesian_category; :: thesis: for a being Object of C holds
( dom (term a) = a & cod (term a) = [1] C )
let a be Object of C; :: thesis: ( dom (term a) = a & cod (term a) = [1] C )
( [1] C is terminal & term a = term (a,([1] C)) ) by Def8, Th14;
hence ( dom (term a) = a & cod (term a) = [1] C ) by CAT_3:35; :: thesis: verum