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:35;
then A6: len g = 1 + (len (mid f,((Index p,f) + 1),(len f))) by FINSEQ_1:56;
then A7: (j + 1) - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1 by A4, XREAL_1:11;
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:11;
A10: j -' 1 = j - 1 by A3, XREAL_1:235;
A11: j = 1 + (j - 1)
.= (len <*p*>) + (j -' 1) by A10, FINSEQ_1:56 ;
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 A12: 1 <= ((Index p,f) + j) -' 1 by NAT_D:39;
consider i being Element of 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, Th41;
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:11;
then A17: 1 - 1 <= ((len f) - (Index p,f)) - 1 by XREAL_1:11;
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:124;
A22: 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 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:8;
then A23: j + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f) by XREAL_1:8;
then A24: (((Index p,f) + j) -' 1) + 1 <= len f by A3, NAT_1:12, XREAL_1:237;
A25: 1 <= j + 1 by A3, NAT_1:13;
then A26: g /. (j + 1) = g . (j + 1) by A4, FINSEQ_4:24;
A27: j + 1 = (len <*p*>) + ((j + 1) - 1) by FINSEQ_1:56
.= (len <*p*>) + ((j + 1) -' 1) by A25, XREAL_1:235 ;
A28: (j + 1) -' 1 = (j + 1) - 1 by A25, XREAL_1:235;
then (j + 1) -' 1 in dom (mid f,((Index p,f) + 1),(len f)) by A3, A7, FINSEQ_3:27;
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:124
.= f . (((((j + 1) -' 1) + 1) + (Index p,f)) -' 1)
.= f . (((j + 1) + (Index p,f)) -' 1) by A25, 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 ;
then A29: f /. ((((Index p,f) + j) -' 1) + 1) = g /. (j + 1) by A24, A26, FINSEQ_4:24, NAT_1:11;
(j + 1) - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1 by A4, A6, XREAL_1:11;
then j + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f) by A21, A18, XREAL_1:8;
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 5;
A31: 1 <= len g by A22, NAT_1:11;

now

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:235;
then A34: 1 <= j -' 1 by A32, SPPOL_1:6;
j - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1 by A6, A5, XREAL_1:11;
then j -' 1 in dom (mid f,((Index p,f) + 1),(len f)) by A33, A34, FINSEQ_3:27;
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:124
.= 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, A5, FINSEQ_4:24;
then LSeg f,(((Index p,f) + j) -' 1) = LSeg (g /. j),(g /. (j + 1)) by A23, A29, A12, A30, A35, 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 A36: 1 = j ; :: thesis: LSeg g,j c= LSeg f,(((Index p,f) + j) -' 1)

then j <= len <*p*> by FINSEQ_1:56;
then j in dom <*p*> by A36, FINSEQ_3:27;
then A37: g . j = <*p*> . j by A2, FINSEQ_1:def 7
.= p by A36, FINSEQ_1:57 ;
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:69;
A39: g /. j = g . j by A31, A36, FINSEQ_4:24;
A40: ((Index p,f) + j) -' 1 = Index p,f by A36, 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 A29, A30, A38, A40, TOPREAL1:12;
hence LSeg g,j c= LSeg f,(((Index p,f) + j) -' 1) by A3, A4, A37, A39, TOPREAL1:def 5; :: thesis: verum

end;

end;

end;

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