let f be S-Sequence_in_R2; :: thesis: for p being Point of (TOP-REAL 2)
for j being Nat st 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) holds
LE f /. j,p, L~ f,f /. 1,f /. (len f)
let p be Point of (TOP-REAL 2); :: thesis: for j being Nat st 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) holds
LE f /. j,p, L~ f,f /. 1,f /. (len f)
let j be Nat; :: thesis: ( 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) implies LE f /. j,p, L~ f,f /. 1,f /. (len f) )
assume that
A1: 1 <= j and
A2: j < len f and
A3: p in L~ (mid (f,j,(len f))) ; :: thesis: LE f /. j,p, L~ f,f /. 1,f /. (len f)
consider i being Nat such that
A4: 1 <= i and
A5: i + 1 <= len (mid (f,j,(len f))) and
A6: p in LSeg ((mid (f,j,(len f))),i) by A3, SPPOL_2:13;
A7: len (mid (f,j,(len f))) = ((len f) -' j) + 1 by A1, A2, FINSEQ_6:186;
then i <= (len f) -' j by A5, XREAL_1:6;
then A8: i + j <= len f by A2, NAT_D:54;
j + i >= i by NAT_1:11;
then A9: ((j + i) -' 1) + 1 <= len f by A4, A8, XREAL_1:235, XXREAL_0:2;
1 + 1 <= j + i by A1, A4, XREAL_1:7;
then A10: 1 <= (j + i) -' 1 by NAT_D:49;
j + 1 <= j + i by A4, XREAL_1:6;
then A11: j <= (j + i) -' 1 by NAT_D:49;
((j + i) -' 1) + 1 >= (j + i) -' 1 by NAT_1:11;
then len f >= (j + i) -' 1 by A9, XXREAL_0:2;
then A12: LE f /. j,f /. ((j + i) -' 1), L~ f,f /. 1,f /. (len f) by A1, A11, JORDAN5C:24;
i < ((len f) -' j) + 1 by A5, A7, NAT_1:13;
then p in LSeg (f,((j + i) -' 1)) by A1, A2, A4, A6, JORDAN4:19;
then LE f /. ((j + i) -' 1),p, L~ f,f /. 1,f /. (len f) by A10, A9, JORDAN5C:25;
hence LE f /. j,p, L~ f,f /. 1,f /. (len f) by A12, JORDAN5C:13; :: thesis: verum