theorem :: NAT_1:55

for s being ManySortedSet of NAT
for k being natural Number holds rng (s ^\ k) c= rng s by Lm1;