theorem :: POWER:13

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