theorem Th1: :: POWER:1

for a being Real
for n being Nat st n is even holds
(- a) |^ n = a |^ n