theorem Th19: :: NUMBER04:19

for k being Nat
for r being Complex holds OddEvenPowers (r,((2 * (k + 1)) + 1)) = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> ^ (OddEvenPowers (r,((2 * k) + 1)))