let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st n <= len f & 2 <= (len f) -' n & f is being_S-Seq holds

f /^ n is being_S-Seq

let n be Element of NAT ; :: thesis: ( n <= len f & 2 <= (len f) -' n & f is being_S-Seq implies f /^ n is being_S-Seq )

assume that

A1: n <= len f and

A2: 2 <= (len f) -' n and

A3: f is being_S-Seq ; :: thesis: f /^ n is being_S-Seq

reconsider f9 = f as one-to-one special unfolded s.n.c. FinSequence of (TOP-REAL 2) by A3;

len (f /^ n) = (len f) - n by A1, RFINSEQ:def 1;

then len (f9 /^ n) >= 2 by A1, A2, XREAL_1:233;

hence f /^ n is being_S-Seq by TOPREAL1:def 8; :: thesis: verum

f /^ n is being_S-Seq

let n be Element of NAT ; :: thesis: ( n <= len f & 2 <= (len f) -' n & f is being_S-Seq implies f /^ n is being_S-Seq )

assume that

A1: n <= len f and

A2: 2 <= (len f) -' n and

A3: f is being_S-Seq ; :: thesis: f /^ n is being_S-Seq

reconsider f9 = f as one-to-one special unfolded s.n.c. FinSequence of (TOP-REAL 2) by A3;

len (f /^ n) = (len f) - n by A1, RFINSEQ:def 1;

then len (f9 /^ n) >= 2 by A1, A2, XREAL_1:233;

hence f /^ n is being_S-Seq by TOPREAL1:def 8; :: thesis: verum