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:41;
then A2:
(Index p,f) + 1 <= len f
by NAT_1:13;
len f <> 0
by A1, TOPREAL1:28;
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:27;
A5:
1 <= Index p,f
by A1, JORDAN3:41;
then A6:
1 < (Index p,f) + 1
by NAT_1:13;
then A7:
(Index p,f) + 1 in dom f
by A2, 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)
;
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 4;
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, JORDAN3:42;
then A10:
p in LSeg (f /. (Index p,f)),
(f /. ((Index p,f) + 1))
by A5, A2, TOPREAL1:def 5;
A11:
LSeg (f /. (Index p,f)),
(f /. ((Index p,f) + 1)) c= L~ f
by A1, A2, JORDAN3:41, SPPOL_2:16;
(mid f,((Index p,f) + 1),(len f)) /. 1
= f /. ((Index p,f) + 1)
by A4, A7, SPRECT_2:12;
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;
len (mid f,((Index p,f) + 1),(len f)) >= 0 + 1
by A4, A7, SPRECT_2:9;
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:47;
hence
L~ (L_Cut f,p) c= L~ f
by A8, A13, A12, XBOOLE_1:8;
verum end;