:: deftheorem defines rho' CAT_4:def 14 :
for C being Cartesian_category
for a being Object of C holds rho' a = <:(id a),(term a):>;