:: deftheorem Def9 defines -defined ACKERMAN:def 9 :
for D being set
for f being Function-yielding ManySortedSet of NAT holds
( f is D -defined iff for n being Nat holds f . n is D -defined );