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
let i be Nat; :: according to TOPREAL1:def 7 :: 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
A2: 1 <= i and
A3: 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 )
A4: len (Rev f) = len f by FINSEQ_5:def 3;
i <= i + 1 by NAT_1:11;
then reconsider j = (len f) - i as Element of NAT by A3, A4, INT_1:18, XXREAL_0:2;
j <= (len f) - 1 by A2, XREAL_1:12;
then A5: j + 1 <= ((len f) - 1) + 1 by XREAL_1:8;
A6: (i + 1) - i <= j by A3, A4, XREAL_1:11;
A7: i + (j + 1) = (len f) + 1 ;
j + 1 in dom f by A5, A6, GOBOARD2:3;
then A9: (Rev f) /. i = f /. (j + 1) by A7, FINSEQ_5:69;
A10: (1 + i) + j = (len f) + 1 ;
j in dom f by A5, A6, GOBOARD2:3;
then (Rev f) /. (i + 1) = f /. j by A10, FINSEQ_5:69;
hence ( ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 ) by A1, A5, A6, A9, TOPREAL1:def 7; :: thesis: verum