theorem Th12: :: POWER:12

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