theorem Th4: :: FIB_NUM4:4
for n being Nat
for a being Real st n is odd & a <> 0 holds
(- a) to_power n = - (a to_power n) by POWER:48;