theorem Th45: :: POWER:45

for a being Real
for n being Nat st a >= 0 & n >= 1 holds
a to_power (1 / n) = n -root a