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, Th41;
A6: j in NAT by ORDINAL1:def 12;
A7: 1 <= j + 1 by NAT_1:11;
A8: 1 <= Index (p,f) by A1, Th41;
1 <= Index (p,f) by A1, Th41;
then A9: 1 <= len f by A5, XXREAL_0:2;
j <= j + 1 by NAT_1:11;
then A10: j <= len g by A3, XXREAL_0:2;

now

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, A9, A8, FINSEQ_6:118;
then A11: len g = (Index (p,f)) + 1 by A1, Th41, XREAL_1:235;
then A12: 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, A11, XXREAL_0:2;
then A13: (j + 1) - 1 <= ((len f) + 1) - 1 by XREAL_1:9;
A14: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A5, A9, A8, FINSEQ_6:118
.= Index (p,f) by A1, Th41, XREAL_1:235 ;
then A15: j in dom (mid (f,1,(Index (p,f)))) by A2, A12, FINSEQ_3:25;
A16: g /. j = g . j by A2, A10, FINSEQ_4:15
.= (mid (f,1,(Index (p,f)))) . j by A4, A15, FINSEQ_1:def 7
.= f . ((j + 1) -' 1) by A2, A6, A5, A9, A8, A12, A14, FINSEQ_6:118
.= f . j by NAT_D:34
.= f /. j by A2, A13, FINSEQ_4:15 ;

now

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

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

A18: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A5, A9, A8, FINSEQ_6:118
.= Index (p,f) by A1, Th41, XREAL_1:235 ;
then A19: j + 1 in dom (mid (f,1,(Index (p,f)))) by A7, A17, FINSEQ_3:25;
A20: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A2, A3, TOPREAL1:def 3;
A21: j + 1 <= len f by A5, A17, 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, A19, FINSEQ_1:def 7
.= f . (((j + 1) + 1) -' 1) by A5, A9, A8, A7, A17, A18, FINSEQ_6:118
.= f . (j + 1) by NAT_D:34
.= f /. (j + 1) by A21, FINSEQ_4:15, NAT_1:11 ;
hence LSeg (g,j) c= LSeg (f,j) by A2, A16, A21, A20, 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 A22: j = Index (p,f) by A12, XXREAL_0:1;
then A23: p in LSeg (f,j) by A1, Th42;

now

assume j + 1 > len f ; :: thesis: contradiction
then j >= len f by NAT_1:13;
hence contradiction by A1, A22, Th41; :: thesis: verum

end;

then A24: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A2, TOPREAL1:def 3;
1 <= len <*p*> by FINSEQ_1:40;
then A25: 1 in dom <*p*> by FINSEQ_3:25;
A26: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A5, A9, A8, FINSEQ_6:118
.= Index (p,f) by A1, Th41, XREAL_1:235 ;
A27: 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, A22, A25, A26, FINSEQ_1:def 7
.= p by FINSEQ_1:def 8 ;
then LSeg ((g /. j),(g /. (j + 1))) c= LSeg ((f /. j),(f /. (j + 1))) by A16, A27, A23, A24, TOPREAL1:6;
hence LSeg (g,j) c= LSeg (f,j) by A2, A3, A24, 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