theorem Th19: :: PREPOWER:19

for a being Real
for n being Nat st a >= 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )