theorem Th5: :: SETLIM_1:5

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