theorem :: SPRECT_3:17

for j being Nat
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)