let f be FinSequence of (); :: thesis: ( f is unfolded implies Rev f is unfolded )
assume A1: f is unfolded ; :: thesis: Rev f is unfolded
A2: dom f = Seg (len f) by FINSEQ_1:def 3;
let i be Nat; :: according to TOPREAL1:def 6 :: 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
A3: 1 <= i and
A4: i + 2 <= len (Rev f) ; :: thesis: (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = {((Rev f) /. (i + 1))}
A5: len (Rev f) = len f by FINSEQ_5:def 3;
then A6: i + 1 in dom f by ;
i + 1 <= (i + 1) + 1 by NAT_1:11;
then reconsider j9 = (len f) - (i + 1) as Element of NAT by ;
i <= i + 2 by NAT_1:11;
then reconsider j = (len f) - i as Element of NAT by ;
A7: j9 + (i + 1) = len f ;
i in dom f by ;
then j + 1 in dom f by ;
then A8: j9 + 2 <= len f by FINSEQ_3:25;
A9: j + (i + 1) = (len f) + 1 ;
i + (1 + 1) = (i + 1) + 1 ;
then A10: 1 <= j9 by ;
j + i = len f ;
hence (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = (LSeg (f,j)) /\ (LSeg ((Rev f),(i + 1))) by Th2
.= (LSeg (f,(j9 + 1))) /\ (LSeg (f,j9)) by
.= {(f /. (j9 + 1))} by A1, A10, A8
.= {((Rev f) /. (i + 1))} by ;
:: thesis: verum