theorem Th1: :: SCPISORT:1

for s being State of SCMPDS
for n, m being Nat ex f being FinSequence of INT st
( len f = n & ( for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) )