let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
L~ (R_Cut f,p) c= L~ f
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies L~ (R_Cut f,p) c= L~ f )
assume A1: p in L~ f ; :: thesis: L~ (R_Cut f,p) c= L~ f
A2: 1 <= Index p,f by A1, Th41;
len f <> 0 by A1, TOPREAL1:28;
then A3: len f >= 0 + 1 by NAT_1:13;
A4: Index p,f <= len f by A1, Th41;

per cases ( p = f . 1 or p <> f . 1 ) ;

suppose p = f . 1 ; :: thesis: L~ (R_Cut f,p) c= L~ f

then R_Cut f,p = <*p*> by Def5;
then len (R_Cut f,p) = 1 by FINSEQ_1:56;
then L~ (R_Cut f,p) = {} by TOPREAL1:28;
hence L~ (R_Cut f,p) c= L~ f by XBOOLE_1:2; :: thesis: verum

end;

suppose A5: p <> f . 1 ; :: thesis: L~ (R_Cut f,p) c= L~ f

A6: f /. (Index p,f) in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by RLTOPSP1:69;
A7: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A3, A2, A4, Th27
.= Index p,f by A1, Th41, XREAL_1:237 ;
then mid f,1,(Index p,f) <> <*> the carrier of (TOP-REAL 2) by A2;
then A8: L~ ((mid f,1,(Index p,f)) ^ <*p*>) = (L~ (mid f,1,(Index p,f))) \/ (LSeg ((mid f,1,(Index p,f)) /. (Index p,f)),p) by A7, SPPOL_2:19;
mid f,1,(Index p,f) = (f /^ (1 -' 1)) | (((Index p,f) -' 1) + 1) by A2, Def1
.= (f /^ 0 ) | (((Index p,f) -' 1) + 1) by XREAL_1:234
.= f | (((Index p,f) -' 1) + 1) by FINSEQ_5:31
.= f | (Index p,f) by A1, Th41, XREAL_1:237 ;
then A9: L~ (mid f,1,(Index p,f)) c= L~ f by TOPREAL3:27;
Index p,f < len f by A1, Th41;
then A10: (Index p,f) + 1 <= len f by NAT_1:13;
then A11: LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) c= L~ f by A1, Th41, SPPOL_2:16;
p in LSeg f,(Index p,f) by A1, Th42;
then A12: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, A10, TOPREAL1:def 5;
(mid f,1,(Index p,f)) /. (Index p,f) = (mid f,1,(Index p,f)) . (Index p,f) by A2, A7, FINSEQ_4:24
.= f . (Index p,f) by A2, A4, Th32
.= f /. (Index p,f) by A1, A4, Th41, FINSEQ_4:24 ;
then LSeg ((mid f,1,(Index p,f)) /. (Index p,f)),p c= LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A12, A6, TOPREAL1:12;
then A13: LSeg ((mid f,1,(Index p,f)) /. (Index p,f)),p c= L~ f by A11, XBOOLE_1:1;
R_Cut f,p = (mid f,1,(Index p,f)) ^ <*p*> by A5, Def5;
hence L~ (R_Cut f,p) c= L~ f by A8, A13, A9, XBOOLE_1:8; :: thesis: verum

end;

end;