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 Def9, Th16;
hence ( dom (term a) = a & cod (term a) = [1] C ) by CAT_3:39; :: thesis: verum