let n be Nat; :: thesis: 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) )
let f be FinSequence; :: thesis: ( S_Drop (n,f) = S_Drop ((n + ((len f) -' 1)),f) & S_Drop (n,f) = S_Drop ((((len f) -' 1) + n),f) )
A1: (n + ((len f) -' 1)) mod ((len f) -' 1) = (n + (((len f) -' 1) * 1)) mod ((len f) -' 1)
.= n mod ((len f) -' 1) by NAT_D:21 ;

per cases ( n mod ((len f) -' 1) <> 0 or n mod ((len f) -' 1) = 0 ) ;

suppose A2: n mod ((len f) -' 1) <> 0 ; :: thesis: ( S_Drop (n,f) = S_Drop ((n + ((len f) -' 1)),f) & S_Drop (n,f) = S_Drop ((((len f) -' 1) + n),f) )

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

end;

suppose A3: n mod ((len f) -' 1) = 0 ; :: thesis: ( S_Drop (n,f) = S_Drop ((n + ((len f) -' 1)),f) & S_Drop (n,f) = S_Drop ((((len f) -' 1) + n),f) )

then S_Drop (n,f) = (len f) -' 1 by Def1;
hence ( S_Drop (n,f) = S_Drop ((n + ((len f) -' 1)),f) & S_Drop (n,f) = S_Drop ((((len f) -' 1) + n),f) ) by A1, A3, Def1; :: thesis: verum

end;

end;