for n being Nat
for f being FinSequence st 1 <= n & n <= (len f) -' 1 holds
S_Drop (n,f) = n