theorem Th44: :: SEQM_3:45

for v being FinSequence of REAL
for n, m, i being Nat st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Nat st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds
r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Nat st k in dom v & v . k = i holds
k <= m ) holds
( m + 1 in dom v & v . (m + 1) = i + 1 )