:: deftheorem defines satisfying_primrec_conditions ACKERMAN:def 10 :
for f being Function-yielding ManySortedSet of NAT holds
( f is satisfying_primrec_conditions iff ( f is homogeneous & f is to-naturals & f is NAT * -defined ) );