1 <= n by NAT_1:14;
then n proj 1 in PrimRec by Def17;
hence n proj 1 is primitive-recursive ; :: thesis: verum