let f be FinSequence of (); :: thesis: for p being Point of () st p in L~ f holds
L~ (R_Cut (f,p)) c= L~ f

let p be Point of (); :: 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 ;
len f <> 0 by ;
then A3: len f >= 0 + 1 by NAT_1:13;
A4: Index (p,f) <= len f by ;
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 Def4;
then len (R_Cut (f,p)) = 1 by FINSEQ_1:39;
then L~ (R_Cut (f,p)) = {} by TOPREAL1:22;
hence L~ (R_Cut (f,p)) c= L~ f ; :: 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:68;
A7: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by
.= Index (p,f) by ;
then mid (f,1,(Index (p,f))) <> <*> the carrier of () 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 ;
mid (f,1,(Index (p,f))) = (f /^ (1 -' 1)) | (((Index (p,f)) -' 1) + 1) by
.= (f /^ 0) | (((Index (p,f)) -' 1) + 1) by XREAL_1:232
.= f | (((Index (p,f)) -' 1) + 1)
.= f | (Index (p,f)) by ;
then A9: L~ (mid (f,1,(Index (p,f)))) c= L~ f by TOPREAL3:20;
Index (p,f) < len f by ;
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 ;
p in LSeg (f,(Index (p,f))) by ;
then A12: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by ;
(mid (f,1,(Index (p,f)))) /. (Index (p,f)) = (mid (f,1,(Index (p,f)))) . (Index (p,f)) by
.= f . (Index (p,f)) by
.= f /. (Index (p,f)) by ;
then LSeg (((mid (f,1,(Index (p,f)))) /. (Index (p,f))),p) c= LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by ;
then A13: LSeg (((mid (f,1,(Index (p,f)))) /. (Index (p,f))),p) c= L~ f by A11;
R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by ;
hence L~ (R_Cut (f,p)) c= L~ f by ; :: thesis: verum
end;
end;