theorem Th25: :: PREPOWER:25

for a being Real
for m, n being Nat st a >= 0 & n >= 1 & m >= 1 holds
n -Root (m -Root a) = (n * m) -Root a