theorem Th4: :: COMPTRIG:4

for x being Real
for n being Nat st x >= 0 & n <> 0 holds
(n -root x) |^ n = x