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 8;
then A3: f /. (len f) in L~ f by JORDAN3:1;
A4: f /. (len f) = (Rev f) /. 1 by A2, CARD_1:27, FINSEQ_5:65;
thus R_Cut (f,(f /. (len f))) = Rev (Rev (R_Cut (f,(f /. (len f)))))
.= Rev (L_Cut ((Rev f),(f /. (len f)))) by A1, A3, JORDAN3:22
.= Rev (Rev f) by A1, A4, Th27
.= f ; :: thesis: verum