theorem Th1: :: SETLIM_1:1

for n, m being Nat
for Y being set
for f being sequence of Y holds f . (n + m) in { (f . k) where k is Nat : n <= k }