let f be FinSequence of (TOP-REAL 2); for n being Nat st f is special holds
f /^ n is special
let n be Nat; ( f is special implies f /^ n is special )
assume A1:
f is special
; f /^ n is special
per cases
( n <= len f or n > len f )
;
suppose A2:
n <= len f
;
f /^ n is special let i be
Nat;
TOPREAL1:def 5 ( 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)
;
( ((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;
verum end; end;