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, JORDAN4:8;

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

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, JORDAN4:8;

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