let j be Element of 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 & j <= len f ) and
A2: p in L~ (mid f,1,j) ; :: thesis: LE p,f /. j, L~ f,f /. 1,f /. (len f)
consider i being Element of NAT such that
A3: ( 1 <= i & i + 1 <= len (mid f,1,j) ) and
A4: p in LSeg (mid f,1,j),i by A2, SPPOL_2:13;
A5: (j -' 1) + 1 = j by A1, XREAL_1:237;
then A6: i + 1 <= j by A1, A3, JORDAN4:20;
A7: i = (i + 1) -' 1 by NAT_D:34;
i < (j -' 1) + 1 by A5, A6, NAT_1:13;
then A8: LSeg (mid f,1,j),i = LSeg f,((i + 1) -' 1) by A1, A3, JORDAN4:31;
i + 1 <= len f by A1, A6, XXREAL_0:2;
then A9: LE p,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A3, A4, A7, A8, JORDAN5C:26;
1 <= i + 1 by NAT_1:11;
then LE f /. (i + 1),f /. j, L~ f,f /. 1,f /. (len f) by A1, A6, JORDAN5C:24;
hence LE p,f /. j, L~ f,f /. 1,f /. (len f) by A9, JORDAN5C:13; :: thesis: verum