let n be Element of NAT ; :: thesis: for f being FinSequence st 1 <= n & n <= (len f) -' 1 holds
S_Drop n,f = n
let f be FinSequence; :: thesis: ( 1 <= n & n <= (len f) -' 1 implies S_Drop n,f = n )
assume A1: ( 1 <= n & n <= (len f) -' 1 ) ; :: thesis: S_Drop n,f = n

per cases ( n < (len f) -' 1 or n = (len f) -' 1 ) by A1, XXREAL_0:1;

suppose n < (len f) -' 1 ; :: thesis: S_Drop n,f = n

then n mod ((len f) -' 1) = n by NAT_D:24;
hence S_Drop n,f = n by A1, Def1; :: thesis: verum

end;

suppose n = (len f) -' 1 ; :: thesis: S_Drop n,f = n

hence S_Drop n,f = n by Th33; :: thesis: verum

end;

end;