let n be 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 that
A1: 1 <= n and
A2: n <= (len f) -' 1 ; :: thesis: S_Drop (n,f) = n

per cases ( n < (len f) -' 1 or n = (len f) -' 1 ) by A2, 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 Th21; :: thesis: verum

end;

end;