:: deftheorem Def1 defines S_Drop JORDAN4:def 1 :
for n being Nat
for f being FinSequence holds
( ( n mod ((len f) -' 1) <> 0 implies S_Drop (n,f) = n mod ((len f) -' 1) ) & ( not n mod ((len f) -' 1) <> 0 implies S_Drop (n,f) = (len f) -' 1 ) );