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;