let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is being_S-Seq implies R_Cut f,(f /. (len f)) = f )
assume A1: f is being_S-Seq ; :: thesis: R_Cut f,(f /. (len f)) = f
then A2: 2 <= len f by TOPREAL1:def 10;
then A3: f /. (len f) in L~ f by JORDAN3:34;
A4: f /. (len f) = (Rev f) /. 1 by A2, CARD_1:47, FINSEQ_5:68;
thus R_Cut f,(f /. (len f)) = Rev (Rev (R_Cut f,(f /. (len f)))) by FINSEQ_6:29
.= Rev (L_Cut (Rev f),(f /. (len f))) by A1, A3, JORDAN3:57
.= Rev (Rev f) by A1, A4, Th30, SPPOL_2:47
.= f by FINSEQ_6:29 ; :: thesis: verum