theorem Th11: :: POWER:11

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