theorem Th26: :: PREPOWER:26

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