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

end;

end;