let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is unfolded implies for p being Point of (TOP-REAL 2) st p in L~ f holds
R_Cut f,p is unfolded )
assume A1:
f is unfolded
; :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
R_Cut f,p is unfolded
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies R_Cut f,p is unfolded )
assume A2:
p in L~ f
; :: thesis: R_Cut f,p is unfolded
then
len f <> 0
by TOPREAL1:28;
then
len f > 0
by NAT_1:3;
then A3:
len f >= 0 + 1
by NAT_1:13;
A4:
( 1 <= Index p,f & Index p,f < len f )
by A2, JORDAN3:41;
then A5:
( 1 < (Index p,f) + 1 & ((Index p,f) + 1) + 0 <= len f )
by NAT_1:13;
A6:
((Index p,f) -' 1) + 1 = Index p,f
by A4, XREAL_1:237;
( Index p,f in Seg (len f) & 1 in Seg (len f) )
by A3, A4, FINSEQ_1:3;
then A7:
( Index p,f in dom f & 1 in dom f )
by FINSEQ_1:def 3;
then A8:
(mid f,1,(Index p,f)) /. (len (mid f,1,(Index p,f))) = f /. (Index p,f)
by SPRECT_2:13;
A9:
p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1))
by A2, JORDAN5B:32;
A10:
LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1))
by A4, A5, TOPREAL1:def 5;
per cases
( Index p,f > 0 + 1 or Index p,f = 0 + 1 )
by A4, XXREAL_0:1;
suppose
Index p,
f > 0 + 1
;
:: thesis: R_Cut f,p is unfolded then
(Index p,f) - 1
> 0
by XREAL_1:22;
then
(Index p,f) -' 1
> 0
by XREAL_0:def 2;
then A11:
(Index p,f) -' 1
>= 0 + 1
by NAT_1:13;
then A12:
LSeg f,
((Index p,f) -' 1) = LSeg (f /. ((Index p,f) -' 1)),
(f /. (Index p,f))
by A4, A6, TOPREAL1:def 5;
A13:
len (mid f,1,(Index p,f)) =
((Index p,f) -' 1) + 1
by A3, A4, JORDAN3:27
.=
Index p,
f
by A4, XREAL_1:237
;
(len (mid f,1,(Index p,f))) -' 1
<= len (mid f,1,(Index p,f))
by NAT_D:35;
then
(len (mid f,1,(Index p,f))) -' 1
in Seg (len (mid f,1,(Index p,f)))
by A11, A13, FINSEQ_1:3;
then
(len (mid f,1,(Index p,f))) -' 1
in dom (mid f,1,(Index p,f))
by FINSEQ_1:def 3;
then A14:
(mid f,1,(Index p,f)) /. ((len (mid f,1,(Index p,f))) -' 1) =
f /. ((((len (mid f,1,(Index p,f))) -' 1) + 1) -' 1)
by A4, A7, SPRECT_2:7
.=
f /. ((len (mid f,1,(Index p,f))) -' 1)
by NAT_D:34
.=
f /. ((((Index p,f) -' 1) + 1) -' 1)
by A4, JORDAN4:20
.=
f /. ((Index p,f) -' 1)
by A4, XREAL_1:237
;
((len (mid f,1,(Index p,f))) -' 1) + 1
= len (mid f,1,(Index p,f))
by A4, A13, XREAL_1:237;
then A15:
LSeg (mid f,1,(Index p,f)),
((len (mid f,1,(Index p,f))) -' 1) = LSeg (f /. ((Index p,f) -' 1)),
(f /. (Index p,f))
by A8, A11, A13, A14, TOPREAL1:def 5;
((Index p,f) -' 1) + (1 + 1) <= len f
by A5, A6;
then A16:
(LSeg (f /. ((Index p,f) -' 1)),(f /. (Index p,f))) /\ (LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1))) = {(f /. (Index p,f))}
by A1, A6, A10, A11, A12, TOPREAL1:def 8;
f /. (Index p,f) in LSeg (f /. (Index p,f)),
(f /. ((Index p,f) + 1))
by RLTOPSP1:69;
then A17:
(LSeg (f /. ((Index p,f) -' 1)),(f /. (Index p,f))) /\ (LSeg (f /. (Index p,f)),p) c= {(f /. (Index p,f))}
by A9, A16, TOPREAL1:12, XBOOLE_1:26;
(
f /. (Index p,f) in LSeg (f /. ((Index p,f) -' 1)),
(f /. (Index p,f)) &
f /. (Index p,f) in LSeg (f /. (Index p,f)),
p )
by RLTOPSP1:69;
then
f /. (Index p,f) in (LSeg (f /. ((Index p,f) -' 1)),(f /. (Index p,f))) /\ (LSeg (f /. (Index p,f)),p)
by XBOOLE_0:def 4;
then A18:
{(f /. (Index p,f))} c= (LSeg (f /. ((Index p,f) -' 1)),(f /. (Index p,f))) /\ (LSeg (f /. (Index p,f)),p)
by ZFMISC_1:37;
A19:
((len (mid f,1,(Index p,f))) -' 1) + 1
= len (mid f,1,(Index p,f))
by A4, A13, XREAL_1:237;
A20:
(LSeg (f /. ((Index p,f) -' 1)),(f /. (Index p,f))) /\ (LSeg (f /. (Index p,f)),p) = {(f /. (Index p,f))}
by A17, A18, XBOOLE_0:def 10;
now per cases
( p <> f . 1 or p = f . 1 )
;
suppose
p <> f . 1
;
:: thesis: R_Cut f,p is unfolded then
R_Cut f,
p = (mid f,1,(Index p,f)) ^ <*p*>
by JORDAN3:def 5;
hence
R_Cut f,
p is
unfolded
by A1, A8, A15, A19, A20, Th28, SPPOL_2:31;
:: thesis: verum end; hence
R_Cut f,
p is
unfolded
;
:: thesis: verum end;