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 13;
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:35
.= (len (mid f,1,(Index p,f))) + 1 by FINSEQ_1:56 ;
then len g = (((Index p,f) -' 1) + 1) + 1 by A5, A9, A8, FINSEQ_6:124;
then A11: len g = (Index p,f) + 1 by A1, Th41, XREAL_1:237;
then A12: j <= Index p,f by A3, XREAL_1:8;
(Index p,f) + 1 <= (len f) + 1 by A5, XREAL_1:8;
then j + 1 <= (len f) + 1 by A3, A11, XXREAL_0:2;
then A13: (j + 1) - 1 <= ((len f) + 1) - 1 by XREAL_1:11;
A14: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A5, A9, A8, FINSEQ_6:124
.= Index p,f by A1, Th41, XREAL_1:237 ;
then A15: j in dom (mid f,1,(Index p,f)) by A2, A12, FINSEQ_3:27;
A16: g /. j = g . j by A2, A10, FINSEQ_4:24
.= (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:124
.= f . j by NAT_D:34
.= f /. j by A2, A13, 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

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