:: deftheorem Def7 defines to-naturals ACKERMAN:def 7 :
for f being Function-yielding ManySortedSet of NAT holds
( f is to-naturals iff for n being Nat holds f . n is to-naturals );