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