theorem Th23: :: PREPOWER:23
for a being Real
for n being Nat st a > 0 & n >= 1 holds
n -Root (1 / a) = 1 / (n -Root a)