theorem Th23: :: JORDAN4:23

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