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

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