theorem Th4: :: SPRECT_5:4

for D being non empty set
for f being FinSequence of D
for p, q being Element of D st p in rng f & q in rng f & p .. f <= q .. f holds
q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1