take f = n const n; :: thesis: ( f is n -ary & f is primitive-recursive & not f is empty )
thus f is n -ary ; :: thesis: ( f is primitive-recursive & not f is empty )
thus f in PrimRec by Def16; :: according to COMPUT_1:def 16 :: thesis: not f is empty
thus not f is empty ; :: thesis: verum