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