let f be FinSequence of (TOP-REAL 2); 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); ( p in L~ f implies L~ (L_Cut (f,p)) c= L~ f )
assume A1:
p in L~ f
; L~ (L_Cut (f,p)) c= L~ f
Index (p,f) < len f
by A1, Th8;
then A2:
(Index (p,f)) + 1 <= len f
by NAT_1:13;
A3:
1 <= Index (p,f)
by A1, Th8;
then A4:
1 < (Index (p,f)) + 1
by NAT_1:13;
then A5:
(Index (p,f)) + 1 in dom f
by A2, FINSEQ_3:25;
len f <> 0
by A1, TOPREAL1:22;
then A6:
len f >= 0 + 1
by NAT_1:13;
then A7:
len f in dom f
by FINSEQ_3:25;
per cases
( p = f . ((Index (p,f)) + 1) or p <> f . ((Index (p,f)) + 1) )
;
suppose
p <> f . ((Index (p,f)) + 1)
;
L~ (L_Cut (f,p)) c= L~ fthen A8:
L_Cut (
f,
p)
= <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))
by Def3;
A9:
f /. ((Index (p,f)) + 1) in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by RLTOPSP1:68;
p in LSeg (
f,
(Index (p,f)))
by A1, Th9;
then A10:
p in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by A3, A2, TOPREAL1:def 3;
A11:
LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
c= L~ f
by A1, A2, Th8, 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:6;
then A12:
LSeg (
p,
((mid (f,((Index (p,f)) + 1),(len f))) /. 1))
c= L~ f
by A11;
mid (
f,
((Index (p,f)) + 1),
(len f))
<> {}
by A7, A5, Lm8, CARD_1:27;
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;
verum end;