for a being Real
for n being Nat st ( ( n >= 1 & a >= 0 ) or n is odd ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )