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))

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;

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))

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 :: thesis: ( ( 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)) ) )end;

hence
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))
; :: thesis: verumper cases
( 1 < j or 1 = j )
by A3, XXREAL_0:1;

end;

case A32:
1 < j
; :: thesis: 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)) ; :: thesis: verum

end;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)) ; :: thesis: verum

case A36:
1 = j
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum