theorem :: POWER:15

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