0 + 1 <= n by NAT_1:13;
hence n proj n in PrimRec by Def14; :: according to COMPUT_1:def 16 :: thesis: verum