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

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