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, Th8;
len f <> 0 by A1, TOPREAL1:22;
then A3: len f >= 0 + 1 by NAT_1:13;
A4: Index (p,f) <= len f by A1, Th8;
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 A3, A2, A4, FINSEQ_6:118
.= Index (p,f) by A1, Th8, XREAL_1:235 ;
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, FINSEQ_6:def 3
.= (f /^ 0) | (((Index (p,f)) -' 1) + 1) by XREAL_1:232
.= f | (((Index (p,f)) -' 1) + 1)
.= f | (Index (p,f)) by A1, Th8, XREAL_1:235 ;
then A9: L~ (mid (f,1,(Index (p,f)))) c= L~ f by TOPREAL3:20;
Index (p,f) < len f by A1, Th8;
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, Th8, SPPOL_2:16;
p in LSeg (f,(Index (p,f))) by A1, Th9;
then A12: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, A10, TOPREAL1:def 3;
(mid (f,1,(Index (p,f)))) /. (Index (p,f)) = (mid (f,1,(Index (p,f)))) . (Index (p,f)) by A2, A7, FINSEQ_4:15
.= f . (Index (p,f)) by A2, A4, FINSEQ_6:123
.= f /. (Index (p,f)) by A1, A4, Th8, FINSEQ_4:15 ;
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:6;
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 A5, Def4;
hence L~ (R_Cut (f,p)) c= L~ f by A8, A13, A9, XBOOLE_1:8; :: thesis: verum
end;
end;