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 H1( 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 = H1(i) ) ) from
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 ; :: thesis: verum