theorem Th38: :: JORDAN1G:38

for f being S-Sequence_in_R2
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. (len f) in L~ (mid (f,k1,k2)) & not k1 = len f holds
k2 = len f