let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is special implies Rev f is special )
assume A1: f is special ; :: thesis: Rev f is special
A2: len (Rev f) = len f by FINSEQ_5:def 3;
let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len (Rev f) or ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 )
assume that
A3: 1 <= i and
A4: i + 1 <= len (Rev f) ; :: thesis: ( ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 )
i <= i + 1 by NAT_1:11;
then reconsider j = (len f) - i as Element of NAT by A4, A2, INT_1:5, XXREAL_0:2;
j <= (len f) - 1 by A3, XREAL_1:10;
then A5: j + 1 <= ((len f) - 1) + 1 by XREAL_1:6;
A6: (1 + i) + j = (len f) + 1 ;
A7: (i + 1) - i <= j by A4, A2, XREAL_1:9;
then j in dom f by A5, SEQ_4:134;
then A8: (Rev f) /. (i + 1) = f /. j by A6, FINSEQ_5:66;
A9: i + (j + 1) = (len f) + 1 ;
j + 1 in dom f by A5, A7, SEQ_4:134;
then (Rev f) /. i = f /. (j + 1) by A9, FINSEQ_5:66;
hence ( ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 ) by A1, A5, A7, A8; :: thesis: verum