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, Th8;
then A5:
(Index (q,f)) - (Index (p,f)) <= (len f) - (Index (p,f))
by XREAL_1:9;
then A6:
((Index (q,f)) - (Index (p,f))) + 1 <= ((len f) - (Index (p,f))) + 1
by XREAL_1:6;
(Index (q,f)) - (Index (p,f)) <= (((len f) - (Index (p,f))) - 1) + 1
by A4, XREAL_1:9;
then A7:
(Index (q,f)) -' (Index (p,f)) <= ((len f) - ((Index (p,f)) + 1)) + 1
by A3, XREAL_1:233;
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:9;
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:6;
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:40;
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, Th8;
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, FINSEQ_6:118;
then A18: (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) =
1 + (((len f) -' ((Index (p,f)) + 1)) + 1)
by FINSEQ_1:40
.=
1 + (((len f) - ((Index (p,f)) + 1)) + 1)
by A4, A9, XREAL_1:233, 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:233;
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, Th26;
then
len (L_Cut (f,p)) >= (Index (q,f)) -' (Index (p,f))
by A3, A5, XREAL_1:233;
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:15
.=
(mid (f,((Index (p,f)) + 1),(len f))) . ((Index (q,f)) -' (Index (p,f)))
by A20, Def3
.=
f . ((((Index (p,f)) + 1) + ((Index (q,f)) -' (Index (p,f)))) - 1)
by A11, A8, A16, A7, FINSEQ_6:122
.=
f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1)
by A3, XREAL_1:233
.=
f . (Index (q,f))
;
then A22:
(L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f))) = f /. (Index (q,f))
by A2, A4, Th8, FINSEQ_4:15;
1
<= Index (
q,
f)
by A2, Th8;
then A23:
1
<= (Index (q,f)) + 1
by NAT_D:48;
A24:
q in LSeg (
f,
(Index (q,f)))
by A2, Th9;
A25:
Index (
q,
f)
< len f
by A2, Th8;
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:9;
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:233;
((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f))
by A26, XREAL_1:9;
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:233;
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:15
.=
(mid (f,((Index (p,f)) + 1),(len f))) . (((Index (q,f)) -' (Index (p,f))) + 1)
by A20, Def3
.=
f . ((((Index (p,f)) + 1) + (((Index (q,f)) -' (Index (p,f))) + 1)) - 1)
by A12, A8, A16, A28, FINSEQ_6:122
.=
f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1)
by A3, XREAL_1:233
.=
f /. ((Index (q,f)) + 1)
by A23, A30, FINSEQ_4:15
;
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 3;
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, Th26;
then
len (L_Cut (f,p)) >= ((Index (q,f)) -' (Index (p,f))) + 1
by A3, A6, XREAL_1:233;
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:15, NAT_1:11
.=
(<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . (((Index (q,f)) -' (Index (p,f))) + 1)
by A31, Def3
.=
(mid (f,((Index (p,f)) + 1),(len f))) . ((((Index (q,f)) -' (Index (p,f))) + 1) - (len <*p*>))
by A14, A19, FINSEQ_6:108
.=
(mid (f,((Index (p,f)) + 1),(len f))) . ((((Index (q,f)) -' (Index (p,f))) + 1) - 1)
by FINSEQ_1:40
.=
f . ((((Index (p,f)) + 1) + ((Index (q,f)) -' (Index (p,f)))) - 1)
by A11, A8, A16, A7, FINSEQ_6:122
.=
f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1)
by A3, XREAL_1:233
.=
f . (Index (q,f))
;
then A33:
(L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = f /. (Index (q,f))
by A2, A4, Th8, FINSEQ_4:15;
A34:
Index (
q,
f)
< len f
by A2, Th8;
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:9;
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:233;
((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f))
by A35, XREAL_1:9;
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:6;
1
<= Index (
q,
f)
by A2, Th8;
then A39:
1
<= (Index (q,f)) + 1
by NAT_D:48;
A40:
q in LSeg (
f,
(Index (q,f)))
by A2, Th9;
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:6;
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:233;
len (L_Cut (f,p)) >= (((Index (q,f)) -' (Index (p,f))) + 1) + 1
by A3, A32, A42, XREAL_1:233;
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:15, NAT_1:11
.=
(<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . ((((Index (q,f)) -' (Index (p,f))) + 1) + 1)
by A31, Def3
.=
(mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - (len <*p*>))
by A15, A43, FINSEQ_6:108
.=
(mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - 1)
by FINSEQ_1:40
.=
f . ((((Index (p,f)) + 1) + (((Index (q,f)) -' (Index (p,f))) + 1)) - 1)
by A12, A8, A16, A37, FINSEQ_6:122
.=
f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1)
by A3, XREAL_1:233
.=
f /. ((Index (q,f)) + 1)
by A39, A41, FINSEQ_4:15
;
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 3;
hence
q in L~ (L_Cut (f,p))
by A38, NAT_1:11, SPPOL_2:15;
verum end;