let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is being_S-Seq implies L_Cut (f,(f /. 1)) = f )
assume A1: f is being_S-Seq ; :: thesis: L_Cut (f,(f /. 1)) = f
then A2: 1 + 1 <= len f by TOPREAL1:def 8;
then 1 <= len f by XXREAL_0:2;
then A3: 1 in dom f by FINSEQ_3:25;
A4: 1 + 1 in dom f by A2, FINSEQ_3:25;
A5: 1 < len f by A2, NAT_1:13;
A6: f is one-to-one by A1;
A7: f /. 1 = f . 1 by A3, PARTFUN1:def 6;
A8: Index ((f /. 1),f) = 1 by A2, JORDAN3:11;
f /. 1 <> f /. (1 + 1) by A3, A4, A6, PARTFUN2:10;
then f /. 1 <> f . (1 + 1) by A4, PARTFUN1:def 6;
hence L_Cut (f,(f /. 1)) = <*(f /. 1)*> ^ (mid (f,((Index ((f /. 1),f)) + 1),(len f))) by A8, JORDAN3:def 3
.= mid (f,1,(len f)) by A3, A5, A7, A8, FINSEQ_6:126
.= f by A2, FINSEQ_6:120, XXREAL_0:2 ;
:: thesis: verum