let f be FinSequence of (TOP-REAL 2); for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> q & Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) holds
q in L~ (L_Cut f,p)
let p, q be Point of (TOP-REAL 2); ( p in L~ f & q in L~ f & p <> q & Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) implies q in L~ (L_Cut f,p) )
assume that
A1:
p in L~ f
and
A2:
q in L~ f
and
A3:
p <> q
and
A4:
Index p,f = Index q,f
and
A5:
LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1)
; q in L~ (L_Cut f,p)
A6: (Index q,f) -' (Index p,f) =
(Index q,f) - (Index p,f)
by A4, XREAL_1:235
.=
0
by A4
;
Index q,f < len f
by A2, Th41;
then A7:
(Index q,f) + 1 <= len f
by NAT_1:13;
A8:
now
q in LSeg (f /. (Index p,f)),
(f /. ((Index p,f) + 1))
by A5, Def6;
then consider r being
Real such that A9:
q = ((1 - r) * (f /. (Index p,f))) + (r * (f /. ((Index p,f) + 1)))
and A10:
0 <= r
and A11:
r <= 1
;
A12:
p =
1
* p
by EUCLID:33
.=
(0. (TOP-REAL 2)) + (1 * p)
by EUCLID:31
.=
((1 - 1) * (f /. (Index p,f))) + (1 * p)
by EUCLID:33
;
assume A13:
p = f . ((Index p,f) + 1)
;
contradictionthen
p = f /. ((Index p,f) + 1)
by A4, A7, FINSEQ_4:24, NAT_1:11;
then
1
<= r
by A5, A9, A10, A12, Def6;
then
r = 1
by A11, XXREAL_0:1;
hence
contradiction
by A3, A4, A7, A13, A9, A12, FINSEQ_4:24, NAT_1:11;
verum end;
then A14:
len (L_Cut f,p) = ((len f) - (Index p,f)) + 1
by A1, Th61;
1 <= Index q,f
by A2, Th41;
then A15:
1 <= (Index q,f) + 1
by NAT_D:48;
1 < (0 + 1) + 1
;
then A16:
len <*p*> < (((Index q,f) -' (Index p,f)) + 1) + 1
by A6, FINSEQ_1:57;
A17:
Index q,f < len f
by A2, Th41;
then A18:
(Index q,f) + 1 <= len f
by NAT_1:13;
then A19:
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by XREAL_1:11;
then A20:
(((Index q,f) - (Index p,f)) + 1) + 1 <= ((len f) - (Index p,f)) + 1
by XREAL_1:8;
((Index q,f) - (Index p,f)) + 1 <= (len f) - (Index p,f)
by A19;
then A21:
((Index q,f) -' (Index p,f)) + 1 <= ((len f) - ((Index p,f) + 1)) + 1
by A4, XREAL_1:235;
A22:
1 <= (Index p,f) + 1
by NAT_1:11;
A23:
Index q,f < len f
by A2, Th41;
then
(Index q,f) - (Index p,f) <= (len f) - (Index p,f)
by XREAL_1:11;
then
((Index q,f) - (Index p,f)) + 1 <= ((len f) - (Index p,f)) + 1
by XREAL_1:8;
then A24: (L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) =
(L_Cut f,p) . (((Index q,f) -' (Index p,f)) + 1)
by A4, A6, A14, FINSEQ_4:24
.=
(<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . (((Index q,f) -' (Index p,f)) + 1)
by A8, Def4
.=
p
by A6, FINSEQ_1:58
;
set i1 = ((Index q,f) -' (Index p,f)) + 1;
A25:
(Index q,f) + 1 <= len f
by A17, NAT_1:13;
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by A18, XREAL_1:11;
then
((Index q,f) - (Index p,f)) + 1 <= (len f) - (Index p,f)
;
then
((Index q,f) -' (Index p,f)) + 1 <= (len f) - (Index p,f)
by A4, XREAL_0:def 2;
then A26:
(((Index q,f) -' (Index p,f)) + 1) + 1 <= len (L_Cut f,p)
by A14, XREAL_1:8;
1 <= Index q,f
by A2, Th41;
then
1 < len f
by A23, XXREAL_0:2;
then
len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1
by A4, A7, A22, FINSEQ_6:124;
then (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f))) =
1 + (((len f) -' ((Index p,f) + 1)) + 1)
by FINSEQ_1:57
.=
1 + (((len f) - ((Index p,f) + 1)) + 1)
by A4, A7, XREAL_1:235
.=
((len f) - (Index p,f)) + 1
;
then A27:
(((Index q,f) -' (Index p,f)) + 1) + 1 <= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f)))
by A4, A20, XREAL_1:235;
(L_Cut f,p) /. ((((Index q,f) -' (Index p,f)) + 1) + 1) =
(L_Cut f,p) . ((((Index q,f) -' (Index p,f)) + 1) + 1)
by A4, A6, A14, A20, FINSEQ_4:24
.=
(<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . ((((Index q,f) -' (Index p,f)) + 1) + 1)
by A8, Def4
.=
(mid f,((Index p,f) + 1),(len f)) . (((((Index q,f) -' (Index p,f)) + 1) + 1) - (len <*p*>))
by A16, A27, FINSEQ_6:114
.=
(mid f,((Index p,f) + 1),(len f)) . (((((Index q,f) -' (Index p,f)) + 1) + 1) - 1)
by FINSEQ_1:57
.=
f . ((((Index p,f) + 1) + (((Index q,f) - (Index p,f)) + 1)) - 1)
by A4, A7, A6, A22, A21, FINSEQ_6:128
.=
f /. ((Index q,f) + 1)
by A15, A25, FINSEQ_4:24
;
then
q in LSeg ((L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1)),((L_Cut f,p) /. ((((Index q,f) -' (Index p,f)) + 1) + 1))
by A4, A5, A24, Th65;
hence
q in L~ (L_Cut f,p)
by A6, A26, SPPOL_2:15; verum