theorem Th3: :: WSIERP_1:3

for x, y being Real
for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds
x = y