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

now

len g = (len (mid f,1,(Index p,f))) + (len <*p*>) by A4, FINSEQ_1:35
.= (len (mid f,1,(Index p,f))) + 1 by FINSEQ_1:56 ;
then len g = (((Index p,f) -' 1) + 1) + 1 by A8, Th27;
then A11: len g = (Index p,f) + 1 by A6, XREAL_1:237;
(Index p,f) + 1 <= (len f) + 1 by A7, XREAL_1:8;
then j + 1 <= (len f) + 1 by A3, A11, XXREAL_0:2;
then A12: (j + 1) - 1 <= ((len f) + 1) - 1 by XREAL_1:11;
A13: j <= Index p,f by A3, A11, XREAL_1:8;
A14: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A8, Th27
.= Index p,f by A6, XREAL_1:237 ;
then A15: j in dom (mid f,1,(Index p,f)) by A2, A13, FINSEQ_3:27;
A16: g /. j = g . j by A2, A9, FINSEQ_4:24
.= (mid f,1,(Index p,f)) . j by A4, A15, FINSEQ_1:def 7
.= f . ((j + 1) -' 1) by A2, A5, A8, A13, A14, Th27
.= f . j by NAT_D:34
.= f /. j by A2, A12, FINSEQ_4:24 ;

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

then A18: j + 1 <= len f by A7, XXREAL_0:2;
A19: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A8, Th27
.= Index p,f by A6, XREAL_1:237 ;
then A20: j + 1 in dom (mid f,1,(Index p,f)) by A10, A17, FINSEQ_3:27;
A21: g /. (j + 1) = g . (j + 1) by A3, FINSEQ_4:24, NAT_1:11
.= (mid f,1,(Index p,f)) . (j + 1) by A4, A20, FINSEQ_1:def 7
.= f . (((j + 1) + 1) -' 1) by A8, A10, A17, A19, Th27
.= f . (j + 1) by NAT_D:34
.= f /. (j + 1) by A18, FINSEQ_4:24, NAT_1:11 ;
LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A2, A3, TOPREAL1:def 5;
hence LSeg g,j c= LSeg f,j by A2, A16, A18, A21, TOPREAL1:def 5; :: 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 A13, XXREAL_0:1;
( 1 <= 1 & 1 <= len <*p*> ) by FINSEQ_1:57;
then A23: 1 in dom <*p*> by FINSEQ_3:27;
A24: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A8, Th27
.= Index p,f by A6, XREAL_1:237 ;
A25: g /. (j + 1) = g . (j + 1) by A3, FINSEQ_4:24, NAT_1:11
.= <*p*> . 1 by A4, A22, A23, A24, FINSEQ_1:def 7
.= p by FINSEQ_1:def 8 ;
A26: f /. j in LSeg (f /. j),(f /. (j + 1)) by RLTOPSP1:69;
A27: p in LSeg f,j by A1, A22, 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 A28: LSeg f,j = LSeg (f /. j),(f /. (j + 1)) by A2, TOPREAL1:def 5;
then LSeg (g /. j),(g /. (j + 1)) c= LSeg (f /. j),(f /. (j + 1)) by A16, A25, A26, A27, TOPREAL1:12;
hence LSeg g,j c= LSeg f,j by A2, A3, A28, TOPREAL1:def 5; :: 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