let f be FinSequence; :: thesis: S_Drop (((len f) -' 1),f) = (len f) -' 1
((len f) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
hence S_Drop (((len f) -' 1),f) = (len f) -' 1 by Def1; :: thesis: verum