for s being State of SCMPDS
for n, m being Nat ex f being FinSequence of INT st
( len f = n & f is_FinSequence_on s,m )