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