let s be State of SCMPDS; :: thesis: for n, m being Nat ex f being FinSequence of INT st
( len f = n & f is_FinSequence_on s,m )
let n, m be Nat; :: thesis: ex f being FinSequence of INT st
( len f = n & f is_FinSequence_on s,m )
consider f being FinSequence of INT such that
A1: len f = n and
A2: for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) by Th1;
take f ; :: thesis: ( len f = n & f is_FinSequence_on s,m )
thus len f = n by A1; :: thesis: f is_FinSequence_on s,m
thus f is_FinSequence_on s,m by A2; :: thesis: verum