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;

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 )
;

end;

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;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

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;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