theorem Th17: :: BASEL_2:17

for n being Nat
for im being imaginary Element of F_Complex
for r being real Element of F_Complex st n is odd holds
( even_part (<%im,r%> `^ n) is imaginary & odd_part (<%im,r%> `^ n) is real )