let f, g be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: 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; :: thesis: ( 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
; :: thesis: LSeg g,j c= LSeg f,(((Index p,f) + j) -' 1)
consider i being Element of NAT such that
A5:
( 1 <= i & i + 1 <= len f & p in LSeg f,i )
by A1, SPPOL_2:13;
1 <= i + 1
by NAT_1:12;
then A6:
1 <= len f
by A5, XXREAL_0:2;
A7: len g =
(len <*p*>) + (len (mid f,((Index p,f) + 1),(len f)))
by A2, FINSEQ_1:35
.=
1 + (len (mid f,((Index p,f) + 1),(len f)))
by FINSEQ_1:56
;
then A8:
1 <= len g
by NAT_1:11;
A9:
Index p,f < len f
by A1, Th41;
then
(Index p,f) + 1 <= len f
by NAT_1:13;
then
((Index p,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by XREAL_1:11;
then A10:
1 - 1 <= ((len f) - (Index p,f)) - 1
by XREAL_1:11;
A11:
(Index p,f) + 1 <= len f
by A9, NAT_1:13;
A12:
0 + 1 <= (Index p,f) + 1
by NAT_1:13;
then A13:
len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1
by A6, A11, Th27;
A14:
( 1 <= (Index p,f) + 1 & (Index p,f) + 1 <= len f & 1 <= len f & len f <= len f )
by A9, A12, NAT_1:13;
A15: len g =
1 + (((len f) - ((Index p,f) + 1)) + 1)
by A7, A10, A13, XREAL_0:def 2
.=
1 + ((len f) - (Index p,f))
;
A16: (len f) -' ((Index p,f) + 1) =
(len f) - ((Index p,f) + 1)
by A10, XREAL_0:def 2
.=
((len f) - (Index p,f)) - 1
;
len g = (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f)))
by A2, FINSEQ_1:35;
then A17:
len g = 1 + (len (mid f,((Index p,f) + 1),(len f)))
by FINSEQ_1:56;
A18:
j <= len g
by A4, NAT_1:13;
A19:
1 <= j + 1
by A3, NAT_1:13;
A20:
j -' 1 = j - 1
by A3, XREAL_1:235;
A21:
(j + 1) -' 1 = (j + 1) - 1
by A19, XREAL_1:235;
A22: j =
1 + (j - 1)
.=
(len <*p*>) + (j -' 1)
by A20, FINSEQ_1:56
;
A23: j + 1 =
(len <*p*>) + ((j + 1) - 1)
by FINSEQ_1:56
.=
(len <*p*>) + ((j + 1) -' 1)
by A19, XREAL_1:235
;
1 <= (Index p,f) + j
by A3, NAT_1:12;
then A24:
1 - 1 <= ((Index p,f) + j) - 1
by XREAL_1:11;
(j + 1) - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1
by A4, A17, XREAL_1:11;
then
j + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f)
by A13, A16, XREAL_1:8;
then
((Index p,f) + (j - 1)) + 1 <= len f
;
then A25:
(((Index p,f) + j) -' 1) + 1 <= len f
by A24, XREAL_0:def 2;
A26:
(j + 1) - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1
by A4, A17, XREAL_1:11;
then A27:
(j + 1) -' 1 in dom (mid f,((Index p,f) + 1),(len f))
by A3, A21, FINSEQ_3:27;
j -' 1 <= j
by NAT_D:35;
then A28:
j -' 1 <= len (mid f,((Index p,f) + 1),(len f))
by A26, XXREAL_0:2;
A29: g . (j + 1) =
(mid f,((Index p,f) + 1),(len f)) . ((j + 1) -' 1)
by A2, A23, A27, FINSEQ_1:def 7
.=
f . ((((j + 1) -' 1) + ((Index p,f) + 1)) -' 1)
by A3, A14, A21, A26, Th27
.=
f . (((((j + 1) -' 1) + 1) + (Index p,f)) -' 1)
.=
f . (((j + 1) + (Index p,f)) -' 1)
by A19, XREAL_1:237
.=
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:237
;
j <= (len f) - (Index p,f)
by A4, A15, XREAL_1:8;
then A30:
j + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f)
by XREAL_1:8;
then A31:
(((Index p,f) + j) -' 1) + 1 <= len f
by A3, NAT_1:12, XREAL_1:237;
g /. (j + 1) = g . (j + 1)
by A4, A19, FINSEQ_4:24;
then A32:
f /. ((((Index p,f) + j) -' 1) + 1) = g /. (j + 1)
by A29, A31, FINSEQ_4:24, NAT_1:11;
1 <= Index p,f
by A1, Th41;
then
1 + 1 <= (Index p,f) + j
by A3, XREAL_1:9;
then
1 <= ((Index p,f) + j) - 1
by XREAL_1:21;
then A33:
1 <= ((Index p,f) + j) -' 1
by NAT_D:39;
then A34:
LSeg f,(((Index p,f) + j) -' 1) = LSeg (f /. (((Index p,f) + j) -' 1)),(f /. ((((Index p,f) + j) -' 1) + 1))
by A25, TOPREAL1:def 5;
now per cases
( 1 < j or 1 = j )
by A3, XXREAL_0:1;
case A35:
1
< j
;
:: thesis: LSeg g,j c= LSeg f,(((Index p,f) + j) -' 1)then A36:
j -' 1
= j - 1
by XREAL_1:235;
then A37:
1
<= j -' 1
by A35, SPPOL_1:6;
j - 1
<= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1
by A17, A18, XREAL_1:11;
then
j -' 1
in dom (mid f,((Index p,f) + 1),(len f))
by A36, A37, FINSEQ_3:27;
then A38:
g . j =
(mid f,((Index p,f) + 1),(len f)) . (j -' 1)
by A2, A22, FINSEQ_1:def 7
.=
f . (((j -' 1) + ((Index p,f) + 1)) -' 1)
by A14, A28, A37, Th27
.=
f . ((((j -' 1) + 1) + (Index p,f)) -' 1)
.=
f . (((Index p,f) + j) -' 1)
by A3, XREAL_1:237
;
g /. j = g . j
by A3, A18, FINSEQ_4:24;
then LSeg f,
(((Index p,f) + j) -' 1) =
LSeg (g /. j),
(g /. (j + 1))
by A30, A32, A33, A34, A38, FINSEQ_4:24, NAT_D:50
.=
LSeg g,
j
by A3, A4, TOPREAL1:def 5
;
hence
LSeg g,
j c= LSeg f,
(((Index p,f) + j) -' 1)
;
:: thesis: verum end; case A39:
1
= j
;
:: thesis: LSeg g,j c= LSeg f,(((Index p,f) + j) -' 1)then
( 1
<= j &
j <= len <*p*> )
by FINSEQ_1:56;
then
j in dom <*p*>
by FINSEQ_3:27;
then A40:
g . j =
<*p*> . j
by A2, FINSEQ_1:def 7
.=
p
by A39, FINSEQ_1:57
;
A41:
g /. j = g . j
by A8, A39, FINSEQ_4:24;
A42:
f /. ((((Index p,f) + j) -' 1) + 1) in LSeg (f /. (((Index p,f) + j) -' 1)),
(f /. ((((Index p,f) + j) -' 1) + 1))
by RLTOPSP1:69;
A43:
((Index p,f) + j) -' 1
= Index p,
f
by A39, NAT_D:34;
p in LSeg f,
(Index p,f)
by A1, Th42;
then
LSeg p,
(g /. (j + 1)) c= LSeg f,
(((Index p,f) + j) -' 1)
by A32, A34, A42, A43, TOPREAL1:12;
hence
LSeg g,
j c= LSeg f,
(((Index p,f) + j) -' 1)
by A3, A4, A40, A41, TOPREAL1:def 5;
:: thesis: verum end;
hence
LSeg g,j c= LSeg f,(((Index p,f) + j) -' 1)
; :: thesis: verum