theorem POW1: :: NEWTON03:12

for a, b being non negative Real
for n being positive Nat holds
( a |^ n = b |^ n iff a = b )