theorem Th37: :: JORDAN1G:37

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