:: deftheorem Def8 defines primitive-recursive ACKERMAN:def 8 :
for f being Function-yielding ManySortedSet of NAT holds
( f is primitive-recursive iff for n being Nat holds f . n is primitive-recursive );