theorem Th2: :: WSIERP_1:2

for x being Real
for a being Nat holds
( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )