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_{1}( 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_{1}(i) ) )
from FINSEQ_1:sch 2();

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

( 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

consider f being FinSequence such that

A1: ( len f = n & ( for i being Nat st i in dom f holds

f . i = H

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

f . i in INT

then reconsider f = f as FinSequence of INT by FINSEQ_2:12;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;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

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