let p be FinSequence of REAL ; :: thesis: for n, m being Nat st n + 1 < m & m <= len p holds
ex pM1 being FinSequence of REAL st
( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds
pM1 . i = p . ((i + n) + 1) ) )
let n, m be Nat; :: thesis: ( n + 1 < m & m <= len p implies ex pM1 being FinSequence of REAL st
( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds
pM1 . i = p . ((i + n) + 1) ) ) )
assume A1: ( n + 1 < m & m <= len p ) ; :: thesis: ex pM1 being FinSequence of REAL st
( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds
pM1 . i = p . ((i + n) + 1) ) )
set n1 = n + 1;
A2: (n + 1) + 1 <= m by A1, NAT_1:13;

per cases ( (n + 1) + 1 = m or (n + 1) + 1 <> m ) ;

suppose A3: (n + 1) + 1 = m ; :: thesis: ex pM1 being FinSequence of REAL st
( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds
pM1 . i = p . ((i + n) + 1) ) )

set pM1 = <*> REAL;
take <*> REAL ; :: thesis: ( len (<*> REAL) = (m - (n + 1)) - 1 & rng (<*> REAL) c= rng p & ( for i being Nat st i in dom (<*> REAL) holds
(<*> REAL) . i = p . ((i + n) + 1) ) )
thus len (<*> REAL) = (m - (n + 1)) - 1 by A3; :: thesis: ( rng (<*> REAL) c= rng p & ( for i being Nat st i in dom (<*> REAL) holds
(<*> REAL) . i = p . ((i + n) + 1) ) )
thus rng (<*> REAL) c= rng p ; :: thesis: for i being Nat st i in dom (<*> REAL) holds
(<*> REAL) . i = p . ((i + n) + 1)
thus for i being Nat st i in dom (<*> REAL) holds
(<*> REAL) . i = p . ((i + n) + 1) ; :: thesis: verum

end;

suppose (n + 1) + 1 <> m ; :: thesis: ex pM1 being FinSequence of REAL st
( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds
pM1 . i = p . ((i + n) + 1) ) )

then (n + 1) + 1 < m by A2, XXREAL_0:1;
then consider TM1 being FinSequence of REAL such that
A4: ( len TM1 = m - ((n + 1) + 1) & rng TM1 c= rng p & ( for i being Nat st i in dom TM1 holds
TM1 . i = p . (i + (n + 1)) ) ) by A1, Th15;
take TM1 ; :: thesis: ( len TM1 = (m - (n + 1)) - 1 & rng TM1 c= rng p & ( for i being Nat st i in dom TM1 holds
TM1 . i = p . ((i + n) + 1) ) )
thus len TM1 = (m - (n + 1)) - 1 by A4; :: thesis: ( rng TM1 c= rng p & ( for i being Nat st i in dom TM1 holds
TM1 . i = p . ((i + n) + 1) ) )
thus rng TM1 c= rng p by A4; :: thesis: for i being Nat st i in dom TM1 holds
TM1 . i = p . ((i + n) + 1)
let i be Nat; :: thesis: ( i in dom TM1 implies TM1 . i = p . ((i + n) + 1) )
assume i in dom TM1 ; :: thesis: TM1 . i = p . ((i + n) + 1)
hence TM1 . i = p . (i + (n + 1)) by A4
.= p . ((i + n) + 1) ;
:: thesis: verum

end;

end;