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

( 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