take f = 3 proj 1; :: thesis: ( f is ternary & f is primitive-recursive )
thus f is ternary ; :: thesis: f is primitive-recursive
thus f in PrimRec by Def17; :: according to COMPUT_1:def 19 :: thesis: verum