let f be FinSequence of (TOP-REAL 2); ( f is unfolded implies for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) is unfolded )
assume A1:
f is unfolded
; for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) is unfolded
let p be Point of (TOP-REAL 2); ( p in L~ f implies L_Cut (f,p) is unfolded )
A2:
mid (f,((Index (p,f)) + 1),(len f)) is unfolded
by A1, Th28;
assume A3:
p in L~ f
; L_Cut (f,p) is unfolded
then A4:
p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))
by JORDAN5B:29;
Index (p,f) < len f
by A3, JORDAN3:8;
then A5:
((Index (p,f)) + 1) + 0 <= len f
by NAT_1:13;
len f <> 0
by A3, TOPREAL1:22;
then
len f > 0
by NAT_1:3;
then A6:
len f >= 0 + 1
by NAT_1:13;
then A7:
len f in dom f
by FINSEQ_3:25;
A8:
1 <= Index (p,f)
by A3, JORDAN3:8;
then A9:
LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))
by A5, TOPREAL1:def 3;
A10:
1 < (Index (p,f)) + 1
by A8, NAT_1:13;
then A11:
(Index (p,f)) + 1 in dom f
by A5, FINSEQ_3:25;
then A12:
(mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. ((Index (p,f)) + 1)
by A7, SPRECT_2:8;
per cases
( ((Index (p,f)) + 1) + 1 <= len f or ((Index (p,f)) + 1) + 1 > len f )
;
suppose A13:
((Index (p,f)) + 1) + 1
<= len f
;
L_Cut (f,p) is unfolded then
LSeg (
f,
((Index (p,f)) + 1))
= LSeg (
(f /. ((Index (p,f)) + 1)),
(f /. ((Index (p,f)) + (1 + 1))))
by A10, TOPREAL1:def 3;
then A14:
(LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) = {(f /. ((Index (p,f)) + 1))}
by A1, A8, A9, A13, TOPREAL1:def 6;
A15:
(len f) - ((Index (p,f)) + 1) >= 0
by A5, XREAL_1:19;
(Index (p,f)) + (1 + 1) <= len f
by A13;
then A16:
2
<= (len f) - (Index (p,f))
by XREAL_1:19;
A17:
f /. ((Index (p,f)) + 1) in LSeg (
(f /. ((Index (p,f)) + 1)),
(f /. ((Index (p,f)) + (1 + 1))))
by RLTOPSP1:68;
f /. ((Index (p,f)) + 1) in LSeg (
p,
(f /. ((Index (p,f)) + 1)))
by RLTOPSP1:68;
then
f /. ((Index (p,f)) + 1) in (LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1)))))
by A17, XBOOLE_0:def 4;
then A18:
{(f /. ((Index (p,f)) + 1))} c= (LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1)))))
by ZFMISC_1:31;
(2 + ((Index (p,f)) + 1)) - 1
= ((Index (p,f)) + 1) + 1
;
then A19:
(2 + ((Index (p,f)) + 1)) - 1
>= 0
by NAT_1:2;
A20:
len (mid (f,((Index (p,f)) + 1),(len f))) =
((len f) -' ((Index (p,f)) + 1)) + 1
by A6, A10, A5, FINSEQ_6:118
.=
((len f) - ((Index (p,f)) + 1)) + 1
by A15, XREAL_0:def 2
.=
(len f) - (Index (p,f))
;
then
2
in dom (mid (f,((Index (p,f)) + 1),(len f)))
by A16, FINSEQ_3:25;
then (mid (f,((Index (p,f)) + 1),(len f))) /. 2 =
f /. ((2 + ((Index (p,f)) + 1)) -' 1)
by A5, A11, A7, SPRECT_2:3
.=
f /. ((Index (p,f)) + (1 + 1))
by A19, XREAL_0:def 2
;
then A21:
LSeg (
(mid (f,((Index (p,f)) + 1),(len f))),1)
= LSeg (
(f /. ((Index (p,f)) + 1)),
(f /. ((Index (p,f)) + (1 + 1))))
by A12, A20, A16, TOPREAL1:def 3;
f /. ((Index (p,f)) + 1) in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by RLTOPSP1:68;
then
(LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) c= {(f /. ((Index (p,f)) + 1))}
by A4, A14, TOPREAL1:6, XBOOLE_1:26;
then A22:
(LSeg (p,(f /. ((Index (p,f)) + 1)))) /\ (LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1))))) = {(f /. ((Index (p,f)) + 1))}
by A18;
now L_Cut (f,p) is unfolded 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 unfolded then
L_Cut (
f,
p)
= <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))
by JORDAN3:def 3;
hence
L_Cut (
f,
p) is
unfolded
by A1, A12, A21, A22, Th28, SPPOL_2:29;
verum end; end; end; hence
L_Cut (
f,
p) is
unfolded
;
verum end; suppose A23:
((Index (p,f)) + 1) + 1
> len f
;
L_Cut (f,p) is unfolded A24:
(
(Index (p,f)) + 1
< len f or
(Index (p,f)) + 1
= len f )
by A5, XXREAL_0:1;
now L_Cut (f,p) is unfolded 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 unfolded then L_Cut (
f,
p) =
<*p*> ^ (mid (f,(len f),(len f)))
by A23, A24, JORDAN3:def 3, NAT_1:13
.=
<*p*> ^ <*(f . (len f))*>
by A7, JORDAN4:15
.=
<*p*> ^ <*(f /. (len f))*>
by A7, PARTFUN1:def 6
.=
<*p,(f /. (len f))*>
by FINSEQ_1:def 9
;
then
len (L_Cut (f,p)) = 2
by FINSEQ_1:44;
hence
L_Cut (
f,
p) is
unfolded
by SPPOL_2:26;
verum end; end; end; hence
L_Cut (
f,
p) is
unfolded
;
verum end; end;