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

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

suppose p = f . ((Index p,f) + 1) ; :: thesis: L~ (L_Cut f,p) c= L~ f

then L_Cut f,p = mid f,((Index p,f) + 1),(len f) by Def4;
hence L~ (L_Cut f,p) c= L~ f by A6, A4, A2, Lm7; :: thesis: verum

end;

suppose p <> f . ((Index p,f) + 1) ; :: thesis: L~ (L_Cut f,p) c= L~ f

then A8: L_Cut f,p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) by Def4;
A9: f /. ((Index p,f) + 1) in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by RLTOPSP1:69;
p in LSeg f,(Index p,f) by A1, Th42;
then A10: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A3, A2, TOPREAL1:def 5;
A11: LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) c= L~ f by A1, A2, Th41, SPPOL_2:16;
(mid f,((Index p,f) + 1),(len f)) /. 1 = f /. ((Index p,f) + 1) by A7, A5, Lm10;
then LSeg p,((mid f,((Index p,f) + 1),(len f)) /. 1) c= LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A10, A9, TOPREAL1:12;
then A12: LSeg p,((mid f,((Index p,f) + 1),(len f)) /. 1) c= L~ f by A11, XBOOLE_1:1;
mid f,((Index p,f) + 1),(len f) <> {} by A7, A5, Lm8, CARD_1:47;
then A13: L~ (<*p*> ^ (mid f,((Index p,f) + 1),(len f))) = (LSeg p,((mid f,((Index p,f) + 1),(len f)) /. 1)) \/ (L~ (mid f,((Index p,f) + 1),(len f))) by SPPOL_2:20;
L~ (mid f,((Index p,f) + 1),(len f)) c= L~ f by A6, A4, A2, Lm7;
hence L~ (L_Cut f,p) c= L~ f by A8, A13, A12, XBOOLE_1:8; :: thesis: verum

end;

end;