:: deftheorem Def6 defines homogeneous ACKERMAN:def 6 :
for f being Function-yielding ManySortedSet of NAT holds
( f is homogeneous iff for n being Nat holds f . n is homogeneous );