:: deftheorem defines proj COMPUT_1:def 8 :
for n, i being Nat holds n proj i = proj ((n |-> NAT),i);