theorem Th3: :: FIB_NUM4:3

for n being Nat
for a being Real st n is even & a <> 0 holds
(- a) to_power n = a to_power n by POWER:47;