1 proj 1 in PrimRec by Def17;
hence 1 proj 1 is primitive-recursive ; :: thesis: verum