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 & 1 <= j & j + 1 <= len g & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds
LSeg (g,j) c= LSeg (f,j)
let p be Point of (TOP-REAL 2); :: thesis: for j being Nat st p in L~ f & 1 <= j & j + 1 <= len g & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds
LSeg (g,j) c= LSeg (f,j)
let j be Nat; :: thesis: ( p in L~ f & 1 <= j & j + 1 <= len g & g = (mid (f,1,(Index (p,f)))) ^ <*p*> implies LSeg (g,j) c= LSeg (f,j) )
assume that
A1: p in L~ f and
A2: 1 <= j and
A3: j + 1 <= len g and
A4: g = (mid (f,1,(Index (p,f)))) ^ <*p*> ; :: thesis: LSeg (g,j) c= LSeg (f,j)
A5: Index (p,f) < len f by A1, Th8;
A6: 1 <= j + 1 by NAT_1:11;
A7: 1 <= Index (p,f) by A1, Th8;
1 <= Index (p,f) by A1, Th8;
then A8: 1 <= len f by A5, XXREAL_0:2;
j <= j + 1 by NAT_1:11;
then A9: j <= len g by A3, XXREAL_0:2;

now :: thesis: LSeg (g,j) c= LSeg (f,j)

len g = (len (mid (f,1,(Index (p,f))))) + (len <*p*>) by A4, FINSEQ_1:22
.= (len (mid (f,1,(Index (p,f))))) + 1 by FINSEQ_1:39 ;
then len g = (((Index (p,f)) -' 1) + 1) + 1 by A5, A8, A7, FINSEQ_6:118;
then A10: len g = (Index (p,f)) + 1 by A1, Th8, XREAL_1:235;
then A11: j <= Index (p,f) by A3, XREAL_1:6;
(Index (p,f)) + 1 <= (len f) + 1 by A5, XREAL_1:6;
then j + 1 <= (len f) + 1 by A3, A10, XXREAL_0:2;
then A12: (j + 1) - 1 <= ((len f) + 1) - 1 by XREAL_1:9;
A13: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A5, A8, A7, FINSEQ_6:118
.= Index (p,f) by A1, Th8, XREAL_1:235 ;
then A14: j in dom (mid (f,1,(Index (p,f)))) by A2, A11, FINSEQ_3:25;
A15: g /. j = g . j by A2, A9, FINSEQ_4:15
.= (mid (f,1,(Index (p,f)))) . j by A4, A14, FINSEQ_1:def 7
.= f . ((j + 1) -' 1) by A2, A5, A8, A7, A11, A13, FINSEQ_6:118
.= f . j by NAT_D:34
.= f /. j by A2, A12, FINSEQ_4:15 ;

now :: thesis: ( ( j + 1 <= Index (p,f) & LSeg (g,j) c= LSeg (f,j) ) or ( j + 1 > Index (p,f) & LSeg (g,j) c= LSeg (f,j) ) )

per cases ( j + 1 <= Index (p,f) or j + 1 > Index (p,f) ) ;

case A16: j + 1 <= Index (p,f) ; :: thesis: LSeg (g,j) c= LSeg (f,j)

A17: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A5, A8, A7, FINSEQ_6:118
.= Index (p,f) by A1, Th8, XREAL_1:235 ;
then A18: j + 1 in dom (mid (f,1,(Index (p,f)))) by A6, A16, FINSEQ_3:25;
A19: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A2, A3, TOPREAL1:def 3;
A20: j + 1 <= len f by A5, A16, XXREAL_0:2;
g /. (j + 1) = g . (j + 1) by A3, FINSEQ_4:15, NAT_1:11
.= (mid (f,1,(Index (p,f)))) . (j + 1) by A4, A18, FINSEQ_1:def 7
.= f . (((j + 1) + 1) -' 1) by A5, A8, A7, A6, A16, A17, FINSEQ_6:118
.= f . (j + 1) by NAT_D:34
.= f /. (j + 1) by A20, FINSEQ_4:15, NAT_1:11 ;
hence LSeg (g,j) c= LSeg (f,j) by A2, A15, A20, A19, TOPREAL1:def 3; :: thesis: verum

end;

case j + 1 > Index (p,f) ; :: thesis: LSeg (g,j) c= LSeg (f,j)

then j >= Index (p,f) by NAT_1:13;
then A21: j = Index (p,f) by A11, XXREAL_0:1;
then A22: p in LSeg (f,j) by A1, Th9;
j + 1 <= len f by A1, A21, Th8, NAT_1:13;
then A23: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A2, TOPREAL1:def 3;
1 <= len <*p*> by FINSEQ_1:40;
then A24: 1 in dom <*p*> by FINSEQ_3:25;
A25: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A5, A8, A7, FINSEQ_6:118
.= Index (p,f) by A1, Th8, XREAL_1:235 ;
A26: f /. j in LSeg ((f /. j),(f /. (j + 1))) by RLTOPSP1:68;
g /. (j + 1) = g . (j + 1) by A3, FINSEQ_4:15, NAT_1:11
.= <*p*> . 1 by A4, A21, A24, A25, FINSEQ_1:def 7
.= p ;
then LSeg ((g /. j),(g /. (j + 1))) c= LSeg ((f /. j),(f /. (j + 1))) by A15, A26, A22, A23, TOPREAL1:6;
hence LSeg (g,j) c= LSeg (f,j) by A2, A3, A23, TOPREAL1:def 3; :: thesis: verum

end;

end;

end;

hence LSeg (g,j) c= LSeg (f,j) ; :: thesis: verum

end;

hence LSeg (g,j) c= LSeg (f,j) ; :: thesis: verum