let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is being_S-Seq implies for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut f,p) holds
f . 1 = p )
assume A1: f is being_S-Seq ; :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut f,p) holds
f . 1 = p
then A2: ( f is one-to-one & f is unfolded & f is s.n.c. & len f >= 2 ) by TOPREAL1:def 10;
then A3: f <> 0 ;
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & f . 1 in L~ (L_Cut f,p) implies f . 1 = p )
assume that
A4: p in L~ f and
A5: f . 1 in L~ (L_Cut f,p) and
A6: f . 1 <> p ; :: thesis: contradiction
set g = mid f,((Index p,f) + 1),(len f);
A7: len f in dom f by A3, FINSEQ_5:6;
1 in dom f by A3, FINSEQ_5:6;
then A8: f /. 1 = f . 1 by PARTFUN1:def 8;
A9: not f . 1 in L~ (mid f,((Index p,f) + 1),(len f)) by A1, A4, Th9;
then p <> f . ((Index p,f) + 1) by A5, JORDAN3:def 4;
then A10: L_Cut f,p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) by JORDAN3:def 4;

per cases ( mid f,((Index p,f) + 1),(len f) is empty or not mid f,((Index p,f) + 1),(len f) is empty ) ;

suppose mid f,((Index p,f) + 1),(len f) is empty ; :: thesis: contradiction

then L_Cut f,p = <*p*> by A10, FINSEQ_1:47;
then len (L_Cut f,p) = 1 by FINSEQ_1:56;
hence contradiction by A5, TOPREAL1:28; :: thesis: verum

end;

suppose not mid f,((Index p,f) + 1),(len f) is empty ; :: thesis: contradiction

then L~ (L_Cut f,p) = (LSeg p,((mid f,((Index p,f) + 1),(len f)) /. 1)) \/ (L~ (mid f,((Index p,f) + 1),(len f))) by A10, SPPOL_2:20;
then A11: f . 1 in LSeg p,((mid f,((Index p,f) + 1),(len f)) /. 1) by A5, A9, XBOOLE_0:def 3;
consider i being Element of NAT such that
A12: ( 1 <= i & i + 1 <= len (<*p*> ^ (mid f,((Index p,f) + 1),(len f))) ) and
A13: f /. 1 in LSeg (<*p*> ^ (mid f,((Index p,f) + 1),(len f))),i by A5, A8, A10, SPPOL_2:13;
A14: 1 <= Index p,f by A4, JORDAN3:41;
LSeg (<*p*> ^ (mid f,((Index p,f) + 1),(len f))),i c= LSeg f,(((Index p,f) + i) -' 1) by A4, A12, JORDAN3:49;
then A15: ((Index p,f) + i) -' 1 = 1 by A2, A13, JORDAN5B:33;
1 + 1 <= (Index p,f) + i by A12, A14, XREAL_1:9;
then A16: (Index p,f) + i = 1 + 1 by A15, XREAL_1:237, XXREAL_0:2;
then Index p,f = 1 by A12, A14, Th10;
then A17: p in LSeg f,1 by A4, JORDAN3:42;
A18: i = 1 by A12, A14, A16, Th10;
A19: 1 + 1 <= len f by A1, TOPREAL1:def 10;
then A20: p in LSeg (f /. 1),(f /. (1 + 1)) by A17, TOPREAL1:def 5;
2 in dom f by A19, FINSEQ_3:27;
then (mid f,((Index p,f) + 1),(len f)) /. 1 = f /. (1 + 1) by A7, A16, A18, SPRECT_2:12;
hence contradiction by A6, A8, A11, A20, SPRECT_3:16; :: thesis: verum

end;

end;