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