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