:: deftheorem defines is_FinSequence_on SCPISORT:def 1 :
for f being FinSequence of INT
for s being State of SCMPDS
for m being Nat holds
( f is_FinSequence_on s,m iff for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) );