theorem Th21: :: JORDAN4:21

for f being FinSequence holds S_Drop (((len f) -' 1),f) = (len f) -' 1