:: deftheorem Def3 defines OddEvenPowers NUMBER04:def 3 :
for r being Complex
for n being Nat
for b₃ being complex-valued FinSequence holds
( b₃ = OddEvenPowers (r,n) iff ( len b₃ = n & ( for i being Nat st 1 <= i & i <= n holds
for m being Nat st m = n - i holds
( ( i is odd implies b₃ . i = r |^ m ) & ( i is even implies b₃ . i = - (r |^ m) ) ) ) ) );