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 & Index p,f < Index q,f 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 & Index p,f < Index q,f implies q in L~ (L_Cut f,p) )
assume that
A1:
p in L~ f
and
A2:
q in L~ f
and
A3:
Index p,f < Index q,f
; q in L~ (L_Cut f,p)
A4:
Index q,f < len f
by A2, Th41;
then A5:
(Index q,f) - (Index p,f) <= (len f) - (Index p,f)
by XREAL_1:11;
then A6:
((Index q,f) - (Index p,f)) + 1 <= ((len f) - (Index p,f)) + 1
by XREAL_1:8;
(Index q,f) - (Index p,f) <= (((len f) - (Index p,f)) - 1) + 1
by A4, XREAL_1:11;
then A7:
(Index q,f) -' (Index p,f) <= ((len f) - ((Index p,f) + 1)) + 1
by A3, XREAL_1:235;
set i1 = ((Index q,f) -' (Index p,f)) + 1;
A8:
1 <= (Index p,f) + 1
by NAT_1:11;
A9:
(Index p,f) + 1 <= Index q,f
by A3, NAT_1:13;
then A10:
((Index p,f) + 1) - (Index p,f) <= (Index q,f) - (Index p,f)
by XREAL_1:11;
then A11:
1 <= (Index q,f) -' (Index p,f)
by XREAL_0:def 2;
then A12:
1 <= ((Index q,f) -' (Index p,f)) + 1
by NAT_D:48;
1 + 1 <= ((Index q,f) -' (Index p,f)) + 1
by A11, XREAL_1:8;
then A13:
1 < ((Index q,f) -' (Index p,f)) + 1
by XXREAL_0:2;
then A14:
len <*p*> < ((Index q,f) -' (Index p,f)) + 1
by FINSEQ_1:57;
then A15:
len <*p*> < (((Index q,f) -' (Index p,f)) + 1) + 1
by NAT_1:13;
A16:
(Index p,f) + 1 <= len f
by A4, A9, XXREAL_0:2;
A17:
1 <= Index q,f
by A2, Th41;
then
1 < len f
by A4, XXREAL_0:2;
then
len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1
by A8, A16, Th27;
then A18: (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, A9, XREAL_1:235, XXREAL_0:2
.=
((len f) - (Index p,f)) + 1
;
then A19:
((Index q,f) -' (Index p,f)) + 1 <= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f)))
by A3, A6, XREAL_1:235;
per cases
( p = f . ((Index p,f) + 1) or p <> f . ((Index p,f) + 1) )
;
suppose A20:
p = f . ((Index p,f) + 1)
;
q in L~ (L_Cut f,p)then A21:
len (L_Cut f,p) = (len f) - (Index p,f)
by A1, Th61;
then
len (L_Cut f,p) >= (Index q,f) -' (Index p,f)
by A3, A5, XREAL_1:235;
then (L_Cut f,p) /. ((Index q,f) -' (Index p,f)) =
(L_Cut f,p) . ((Index q,f) -' (Index p,f))
by A11, FINSEQ_4:24
.=
(mid f,((Index p,f) + 1),(len f)) . ((Index q,f) -' (Index p,f))
by A20, Def4
.=
f . ((((Index p,f) + 1) + ((Index q,f) -' (Index p,f))) - 1)
by A11, A8, A16, A7, Th31
.=
f . ((((Index p,f) + 1) + ((Index q,f) - (Index p,f))) - 1)
by A3, XREAL_1:235
.=
f . (Index q,f)
;
then A22:
(L_Cut f,p) /. ((Index q,f) -' (Index p,f)) = f /. (Index q,f)
by A2, A4, Th41, FINSEQ_4:24;
1
<= Index q,
f
by A2, Th41;
then A23:
1
<= (Index q,f) + 1
by NAT_D:48;
A24:
q in LSeg f,
(Index q,f)
by A2, Th42;
A25:
Index q,
f < len f
by A2, Th41;
then A26:
(Index q,f) + 1
<= len f
by NAT_1:13;
then A27:
((Index q,f) + 1) - (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)
;
then A28:
((Index q,f) -' (Index p,f)) + 1
<= ((len f) - ((Index p,f) + 1)) + 1
by A3, XREAL_1:235;
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by A26, XREAL_1:11;
then
((Index q,f) - (Index p,f)) + 1
<= (len f) - (Index p,f)
;
then A29:
((Index q,f) -' (Index p,f)) + 1
<= len (L_Cut f,p)
by A10, A21, XREAL_0:def 2;
A30:
(Index q,f) + 1
<= len f
by A25, NAT_1:13;
((Index q,f) - (Index p,f)) + 1
<= (len f) - (Index p,f)
by A27;
then
len (L_Cut f,p) >= ((Index q,f) -' (Index p,f)) + 1
by A3, A21, XREAL_1:235;
then (L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) =
(L_Cut f,p) . (((Index q,f) -' (Index p,f)) + 1)
by A13, FINSEQ_4:24
.=
(mid f,((Index p,f) + 1),(len f)) . (((Index q,f) -' (Index p,f)) + 1)
by A20, Def4
.=
f . ((((Index p,f) + 1) + (((Index q,f) -' (Index p,f)) + 1)) - 1)
by A12, A8, A16, A28, Th31
.=
f . ((((Index p,f) + 1) + (((Index q,f) - (Index p,f)) + 1)) - 1)
by A3, XREAL_1:235
.=
f /. ((Index q,f) + 1)
by A23, A30, FINSEQ_4:24
;
then
q in LSeg ((L_Cut f,p) /. ((Index q,f) -' (Index p,f))),
((L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1))
by A17, A22, A26, A24, TOPREAL1:def 5;
hence
q in L~ (L_Cut f,p)
by A11, A29, SPPOL_2:15;
verum end; suppose A31:
p <> f . ((Index p,f) + 1)
;
q in L~ (L_Cut f,p)A32:
len (L_Cut f,p) = ((len f) - (Index p,f)) + 1
by A1, A31, Th61;
then
len (L_Cut f,p) >= ((Index q,f) -' (Index p,f)) + 1
by A3, A6, XREAL_1:235;
then (L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) =
(L_Cut f,p) . (((Index q,f) -' (Index p,f)) + 1)
by FINSEQ_4:24, NAT_1:11
.=
(<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . (((Index q,f) -' (Index p,f)) + 1)
by A31, Def4
.=
(mid f,((Index p,f) + 1),(len f)) . ((((Index q,f) -' (Index p,f)) + 1) - (len <*p*>))
by A14, A19, Th15
.=
(mid f,((Index p,f) + 1),(len f)) . ((((Index q,f) -' (Index p,f)) + 1) - 1)
by FINSEQ_1:57
.=
f . ((((Index p,f) + 1) + ((Index q,f) -' (Index p,f))) - 1)
by A11, A8, A16, A7, Th31
.=
f . ((((Index p,f) + 1) + ((Index q,f) - (Index p,f))) - 1)
by A3, XREAL_1:235
.=
f . (Index q,f)
;
then A33:
(L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) = f /. (Index q,f)
by A2, A4, Th41, FINSEQ_4:24;
A34:
Index q,
f < len f
by A2, Th41;
then A35:
(Index q,f) + 1
<= len f
by NAT_1:13;
then A36:
((Index q,f) + 1) - (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)
;
then A37:
((Index q,f) -' (Index p,f)) + 1
<= ((len f) - ((Index p,f) + 1)) + 1
by A3, XREAL_1:235;
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by A35, 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 A10, XREAL_0:def 2;
then A38:
(((Index q,f) -' (Index p,f)) + 1) + 1
<= len (L_Cut f,p)
by A32, XREAL_1:8;
1
<= Index q,
f
by A2, Th41;
then A39:
1
<= (Index q,f) + 1
by NAT_D:48;
A40:
q in LSeg f,
(Index q,f)
by A2, Th42;
A41:
(Index q,f) + 1
<= len f
by A34, NAT_1:13;
A42:
(((Index q,f) - (Index p,f)) + 1) + 1
<= ((len f) - (Index p,f)) + 1
by A36, XREAL_1:8;
then A43:
(((Index q,f) -' (Index p,f)) + 1) + 1
<= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f)))
by A3, A18, XREAL_1:235;
len (L_Cut f,p) >= (((Index q,f) -' (Index p,f)) + 1) + 1
by A3, A32, A42, XREAL_1:235;
then (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 FINSEQ_4:24, NAT_1:11
.=
(<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . ((((Index q,f) -' (Index p,f)) + 1) + 1)
by A31, Def4
.=
(mid f,((Index p,f) + 1),(len f)) . (((((Index q,f) -' (Index p,f)) + 1) + 1) - (len <*p*>))
by A15, A43, Th15
.=
(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 A12, A8, A16, A37, Th31
.=
f . ((((Index p,f) + 1) + (((Index q,f) - (Index p,f)) + 1)) - 1)
by A3, XREAL_1:235
.=
f /. ((Index q,f) + 1)
by A39, A41, 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 A17, A33, A35, A40, TOPREAL1:def 5;
hence
q in L~ (L_Cut f,p)
by A38, NAT_1:11, SPPOL_2:15;
verum end;