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
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
A2: 1 <= i and
A3: 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 A2, A3, SEQ_4:134;
then A4: (f | n) /. i = f /. i by FINSEQ_4:70;
i + 1 in dom (f | n) by A2, A3, SEQ_4:134;
then A5: (f | n) /. (i + 1) = f /. (i + 1) by FINSEQ_4:70;
len (f | n) <= len f by FINSEQ_5:16;
then i + 1 <= len f by A3, XXREAL_0:2;
hence ( ((f | n) /. i) `1 = ((f | n) /. (i + 1)) `1 or ((f | n) /. i) `2 = ((f | n) /. (i + 1)) `2 ) by A1, A2, A4, A5; :: thesis: verum