theorem Th47: :: POWER:47

for a being Real
for k being Integer st k is even holds
(- a) to_power k = a to_power k