let s be State of SCMPDS; :: thesis: for n, m being Element of NAT ex f being FinSequence of INT st
( len f = n & ( for i being Element of NAT st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) )
let n, m be Element of NAT ; :: thesis: ex f being FinSequence of INT st
( len f = n & ( for i being Element of 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

let i be Nat; :: thesis: ( i in dom f implies f . i in INT )
reconsider a = i as Element of NAT by ORDINAL1:def 12;
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 Element of NAT st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) )
thus len f = n by A1; :: thesis: for i being Element of NAT st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i))

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f implies f . i = s . (intpos (m + i)) )
assume ( 1 <= i & i <= len f ) ; :: thesis: f . i = s . (intpos (m + i))
then i in dom f by FINSEQ_3:25;
hence f . i = s . (intpos (m + i)) by A1; :: thesis: verum

end;