let f be FinSequence of (TOP-REAL 2); ( f is special implies for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) is special )
assume A1:
f is special
; for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) is special
let p be Point of (TOP-REAL 2); ( p in L~ f implies L_Cut (f,p) is special )
A2:
mid (f,((Index (p,f)) + 1),(len f)) is special
by A1, Th27;
A3:
<*p*> /. 1 = p
by FINSEQ_4:16;
assume A4:
p in L~ f
; L_Cut (f,p) is special
then
Index (p,f) < len f
by JORDAN3:8;
then A5:
(Index (p,f)) + 1 <= len f
by NAT_1:13;
1 <= Index (p,f)
by A4, JORDAN3:8;
then A6:
LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))
by A5, TOPREAL1:def 3;
A8:
len <*p*> = 1
by FINSEQ_1:39;
len f <> 0
by A4, TOPREAL1:22;
then
len f > 0
by NAT_1:3;
then
len f >= 0 + 1
by NAT_1:13;
then A9:
len f in dom f
by FINSEQ_3:25;
(Index (p,f)) + 1 >= 1
by NAT_1:11;
then
(Index (p,f)) + 1 in dom f
by A5, FINSEQ_3:25;
then A10:
(mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. ((Index (p,f)) + 1)
by A9, SPRECT_2:8;
per cases
( p <> f . ((Index (p,f)) + 1) or p = f . ((Index (p,f)) + 1) )
;
suppose
p <> f . ((Index (p,f)) + 1)
;
L_Cut (f,p) is special then
L_Cut (
f,
p)
= <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))
by JORDAN3:def 3;
hence
L_Cut (
f,
p) is
special
by A2, A8, A3, A10, A7, GOBOARD2:8;
verum end; end;