let f, g be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2)
for j being Nat st p in L~ f & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) & 1 <= j & j + 1 <= len g holds
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))
let p be Point of (TOP-REAL 2); for j being Nat st p in L~ f & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) & 1 <= j & j + 1 <= len g holds
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))
let j be Nat; ( p in L~ f & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) & 1 <= j & j + 1 <= len g implies LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) )
assume that
A1:
p in L~ f
and
A2:
g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))
and
A3:
1 <= j
and
A4:
j + 1 <= len g
; LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))
A5:
j <= len g
by A4, NAT_1:13;
len g = (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f))))
by A2, FINSEQ_1:22;
then A6:
len g = 1 + (len (mid (f,((Index (p,f)) + 1),(len f))))
by FINSEQ_1:39;
then A7:
(j + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1
by A4, XREAL_1:9;
j -' 1 <= j
by NAT_D:35;
then A8:
j -' 1 <= len (mid (f,((Index (p,f)) + 1),(len f)))
by A7, XXREAL_0:2;
1 <= (Index (p,f)) + j
by A3, NAT_1:12;
then A9:
1 - 1 <= ((Index (p,f)) + j) - 1
by XREAL_1:9;
A10:
j -' 1 = j - 1
by A3, XREAL_1:233;
A11: j =
1 + (j - 1)
.=
(len <*p*>) + (j -' 1)
by A10, FINSEQ_1:39
;
1 <= Index (p,f)
by A1, Th8;
then
1 + 1 <= (Index (p,f)) + j
by A3, XREAL_1:7;
then
1 <= ((Index (p,f)) + j) - 1
by XREAL_1:19;
then A12:
1 <= ((Index (p,f)) + j) -' 1
by NAT_D:39;
consider i being Nat such that
1 <= i
and
A13:
i + 1 <= len f
and
p in LSeg (f,i)
by A1, SPPOL_2:13;
1 <= i + 1
by NAT_1:12;
then A14:
1 <= len f
by A13, XXREAL_0:2;
A15:
Index (p,f) < len f
by A1, Th8;
then A16:
(Index (p,f)) + 1 <= len f
by NAT_1:13;
(Index (p,f)) + 1 <= len f
by A15, NAT_1:13;
then
((Index (p,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f))
by XREAL_1:9;
then A17:
1 - 1 <= ((len f) - (Index (p,f))) - 1
by XREAL_1:9;
then A18: (len f) -' ((Index (p,f)) + 1) =
(len f) - ((Index (p,f)) + 1)
by XREAL_0:def 2
.=
((len f) - (Index (p,f))) - 1
;
A19:
0 + 1 <= (Index (p,f)) + 1
by NAT_1:13;
then A20:
1 <= len f
by A15, NAT_1:13;
(Index (p,f)) + 1 <= len f
by A15, NAT_1:13;
then A21:
len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1
by A14, A19, FINSEQ_6:118;
A22: len g =
(len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f))))
by A2, FINSEQ_1:22
.=
1 + (len (mid (f,((Index (p,f)) + 1),(len f))))
by FINSEQ_1:39
;
then len g =
1 + (((len f) - ((Index (p,f)) + 1)) + 1)
by A17, A21, XREAL_0:def 2
.=
1 + ((len f) - (Index (p,f)))
;
then
j <= (len f) - (Index (p,f))
by A4, XREAL_1:6;
then A23:
j + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f))
by XREAL_1:6;
then A24:
(((Index (p,f)) + j) -' 1) + 1 <= len f
by A3, NAT_1:12, XREAL_1:235;
A25:
1 <= j + 1
by A3, NAT_1:13;
then A26:
g /. (j + 1) = g . (j + 1)
by A4, FINSEQ_4:15;
A27: j + 1 =
(len <*p*>) + ((j + 1) - 1)
by FINSEQ_1:39
.=
(len <*p*>) + ((j + 1) -' 1)
by A25, XREAL_1:233
;
A28:
(j + 1) -' 1 = (j + 1) - 1
by A25, XREAL_1:233;
then
(j + 1) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f)))
by A3, A7, FINSEQ_3:25;
then g . (j + 1) =
(mid (f,((Index (p,f)) + 1),(len f))) . ((j + 1) -' 1)
by A2, A27, FINSEQ_1:def 7
.=
f . ((((j + 1) -' 1) + ((Index (p,f)) + 1)) -' 1)
by A3, A19, A16, A20, A28, A7, FINSEQ_6:118
.=
f . (((((j + 1) -' 1) + 1) + (Index (p,f))) -' 1)
.=
f . (((j + 1) + (Index (p,f))) -' 1)
by A25, XREAL_1:235
.=
f . ((((Index (p,f)) + j) + 1) -' 1)
.=
f . ((Index (p,f)) + j)
by NAT_D:34
.=
f . ((((Index (p,f)) + j) -' 1) + 1)
by A3, NAT_1:12, XREAL_1:235
;
then A29:
f /. ((((Index (p,f)) + j) -' 1) + 1) = g /. (j + 1)
by A24, A26, FINSEQ_4:15, NAT_1:11;
(j + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1
by A4, A6, XREAL_1:9;
then
j + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f))
by A21, A18, XREAL_1:6;
then
((Index (p,f)) + (j - 1)) + 1 <= len f
;
then
(((Index (p,f)) + j) -' 1) + 1 <= len f
by A9, XREAL_0:def 2;
then A30:
LSeg (f,(((Index (p,f)) + j) -' 1)) = LSeg ((f /. (((Index (p,f)) + j) -' 1)),(f /. ((((Index (p,f)) + j) -' 1) + 1)))
by A12, TOPREAL1:def 3;
A31:
1 <= len g
by A22, NAT_1:11;
now ( ( 1 < j & LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) ) or ( 1 = j & LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) ) )per cases
( 1 < j or 1 = j )
by A3, XXREAL_0:1;
case A32:
1
< j
;
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))then A33:
j -' 1
= j - 1
by XREAL_1:233;
then A34:
1
<= j -' 1
by A32, SPPOL_1:1;
j - 1
<= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1
by A6, A5, XREAL_1:9;
then
j -' 1
in dom (mid (f,((Index (p,f)) + 1),(len f)))
by A33, A34, FINSEQ_3:25;
then A35:
g . j =
(mid (f,((Index (p,f)) + 1),(len f))) . (j -' 1)
by A2, A11, FINSEQ_1:def 7
.=
f . (((j -' 1) + ((Index (p,f)) + 1)) -' 1)
by A19, A16, A20, A8, A34, FINSEQ_6:118
.=
f . ((((j -' 1) + 1) + (Index (p,f))) -' 1)
.=
f . (((Index (p,f)) + j) -' 1)
by A3, XREAL_1:235
;
g /. j = g . j
by A3, A5, FINSEQ_4:15;
then LSeg (
f,
(((Index (p,f)) + j) -' 1)) =
LSeg (
(g /. j),
(g /. (j + 1)))
by A23, A29, A12, A30, A35, FINSEQ_4:15, NAT_D:50
.=
LSeg (
g,
j)
by A3, A4, TOPREAL1:def 3
;
hence
LSeg (
g,
j)
c= LSeg (
f,
(((Index (p,f)) + j) -' 1))
;
verum end; case A36:
1
= j
;
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))then
j <= len <*p*>
by FINSEQ_1:39;
then
j in dom <*p*>
by A36, FINSEQ_3:25;
then A37:
g . j =
<*p*> . j
by A2, FINSEQ_1:def 7
.=
p
by A36, FINSEQ_1:40
;
A38:
f /. ((((Index (p,f)) + j) -' 1) + 1) in LSeg (
(f /. (((Index (p,f)) + j) -' 1)),
(f /. ((((Index (p,f)) + j) -' 1) + 1)))
by RLTOPSP1:68;
A39:
g /. j = g . j
by A31, A36, FINSEQ_4:15;
A40:
((Index (p,f)) + j) -' 1
= Index (
p,
f)
by A36, NAT_D:34;
p in LSeg (
f,
(Index (p,f)))
by A1, Th9;
then
LSeg (
p,
(g /. (j + 1)))
c= LSeg (
f,
(((Index (p,f)) + j) -' 1))
by A29, A30, A38, A40, TOPREAL1:6;
hence
LSeg (
g,
j)
c= LSeg (
f,
(((Index (p,f)) + j) -' 1))
by A3, A4, A37, A39, TOPREAL1:def 3;
verum end;
hence
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))
; verum