let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is unfolded implies Rev f is unfolded )
assume A1: f is unfolded ; :: thesis: Rev f is unfolded
let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( not 1 <= i or not i + 2 <= len (Rev f) or (LSeg (Rev f),i) /\ (LSeg (Rev f),(i + 1)) = {((Rev f) /. (i + 1))} )
assume that
A2: 1 <= i and
A3: i + 2 <= len (Rev f) ; :: thesis: (LSeg (Rev f),i) /\ (LSeg (Rev f),(i + 1)) = {((Rev f) /. (i + 1))}
A4: len (Rev f) = len f by FINSEQ_5:def 3;
i <= i + 2 by NAT_1:11;
then reconsider j = (len f) - i as Element of NAT by A3, A4, INT_1:18, XXREAL_0:2;
A5: j + i = len f ;
i + 1 <= (i + 1) + 1 by NAT_1:11;
then reconsider j' = (len f) - (i + 1) as Element of NAT by A3, A4, INT_1:18, XXREAL_0:2;
A6: j' + (i + 1) = len f ;
A7: j + (i + 1) = (len f) + 1 ;
A8: dom f = Seg (len f) by FINSEQ_1:def 3;
i + (1 + 1) = (i + 1) + 1 ;
then A9: 1 <= j' by A3, A4, XREAL_1:21;
i in dom f by A2, A3, A4, GOBOARD2:4;
then j + 1 in dom f by A8, FINSEQ_5:2;
then A10: j' + 2 <= len f by FINSEQ_3:27;
A11: i + 1 in dom f by A2, A3, A4, GOBOARD2:4;
thus (LSeg (Rev f),i) /\ (LSeg (Rev f),(i + 1)) = (LSeg f,j) /\ (LSeg (Rev f),(i + 1)) by A5, Th2
.= (LSeg f,(j' + 1)) /\ (LSeg f,j') by A6, Th2
.= {(f /. (j' + 1))} by A1, A9, A10, TOPREAL1:def 8
.= {((Rev f) /. (i + 1))} by A7, A8, A11, FINSEQ_5:2, FINSEQ_5:69 ; :: thesis: verum