let n be Element of 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;