let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st f is special holds

f /^ n is special

let n be Nat; :: thesis: ( f is special implies f /^ n is special )

assume A1: f is special ; :: thesis: f /^ n is special

f /^ n is special

let n be Nat; :: thesis: ( f is special implies f /^ n is special )

assume A1: f is special ; :: thesis: f /^ n is special

per cases
( n <= len f or n > len f )
;

end;

suppose A2:
n <= len f
; :: thesis: f /^ n is special

let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len (f /^ n) or ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 )

assume that

A3: 1 <= i and

A4: i + 1 <= len (f /^ n) ; :: thesis: ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 )

i in dom (f /^ n) by A3, A4, SEQ_4:134;

then A5: (f /^ n) /. i = f /. (n + i) by FINSEQ_5:27;

i <= n + i by NAT_1:11;

then A6: 1 <= n + i by A3, XXREAL_0:2;

i + 1 in dom (f /^ n) by A3, A4, SEQ_4:134;

then A7: (f /^ n) /. (i + 1) = f /. (n + (i + 1)) by FINSEQ_5:27

.= f /. ((n + i) + 1) ;

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

then n + (i + 1) <= len f by A4, XREAL_1:19;

hence ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 ) by A1, A5, A7, A6; :: thesis: verum

end;assume that

A3: 1 <= i and

A4: i + 1 <= len (f /^ n) ; :: thesis: ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 )

i in dom (f /^ n) by A3, A4, SEQ_4:134;

then A5: (f /^ n) /. i = f /. (n + i) by FINSEQ_5:27;

i <= n + i by NAT_1:11;

then A6: 1 <= n + i by A3, XXREAL_0:2;

i + 1 in dom (f /^ n) by A3, A4, SEQ_4:134;

then A7: (f /^ n) /. (i + 1) = f /. (n + (i + 1)) by FINSEQ_5:27

.= f /. ((n + i) + 1) ;

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

then n + (i + 1) <= len f by A4, XREAL_1:19;

hence ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 ) by A1, A5, A7, A6; :: thesis: verum