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;

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

per cases ( 1 < j or 1 = j ) by A3, XXREAL_0:1;

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;

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

end;

end;

hence LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) ; :: thesis: verum