theorem Th22: :: PREPOWER:22

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)