let f be FinSequence of (); :: 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 ;
j <= (len f) - 1 by ;
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 ;
then j in dom f by ;
then A8: (Rev f) /. (i + 1) = f /. j by ;
A9: i + (j + 1) = (len f) + 1 ;
j + 1 in dom f by ;
then (Rev f) /. i = f /. (j + 1) by ;
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