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