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, JORDAN3:8;
then A2:
(Index (p,f)) + 1 <= len f
by NAT_1:13;
len f <> 0
by A1, TOPREAL1:22;
then
len f > 0
by NAT_1:3;
then A3:
len f >= 0 + 1
by NAT_1:13;
then A4:
len f in dom f
by FINSEQ_3:25;
A5:
1 <= Index (p,f)
by A1, JORDAN3:8;
then A6:
1 < (Index (p,f)) + 1
by NAT_1:13;
then A7:
(Index (p,f)) + 1 in dom f
by A2, 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 JORDAN3:def 3;
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, JORDAN3:9;
then A10:
p in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by A5, A2, TOPREAL1:def 3;
A11:
LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
c= L~ f
by A1, A2, JORDAN3:8, SPPOL_2:16;
(mid (f,((Index (p,f)) + 1),(len f))) /. 1
= f /. ((Index (p,f)) + 1)
by A4, A7, SPRECT_2:8;
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;
len (mid (f,((Index (p,f)) + 1),(len f))) >= 0 + 1
by A4, A7, SPRECT_2:5;
then
mid (
f,
((Index (p,f)) + 1),
(len f))
<> {}
;
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 A3, A6, A2, JORDAN4:35;
hence
L~ (L_Cut (f,p)) c= L~ f
by A8, A13, A12, XBOOLE_1:8;
verum end;