theorem Th6: :: SETLIM_1:6

for k being Nat
for Y being non empty set
for f being sequence of Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }