let s be State of SCMPDS; :: thesis: 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)) ) )
let n, m be Nat; :: thesis: 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)) ) )
deffunc H₁( Nat) -> set = s . (intpos (m + $1));
consider f being FinSequence such that
A1: ( len f = n & ( for i being Nat st i in dom f holds
f . i = H₁(i) ) ) from FINSEQ_1:sch 2();

now :: thesis: for i being Nat st i in dom f holds
f . i in INT

let i be Nat; :: thesis: ( i in dom f implies f . i in INT )
reconsider a = i as Nat ;
assume i in dom f ; :: thesis: f . i in INT
then f . i = s . (intpos (m + a)) by A1;
hence f . i in INT by INT_1:def 2; :: thesis: verum

end;

then reconsider f = f as FinSequence of INT by FINSEQ_2:12;
take f ; :: thesis: ( len f = n & ( for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) )
thus len f = n by A1; :: thesis: for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i))
thus for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) by A1, FINSEQ_3:25; :: thesis: verum