theorem Th2: :: SETLIM_1:2

for n being Nat
for Y being set
for f being sequence of Y holds { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}