for k being Nat
for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Nat : k <= n }