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