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