theorem Th9: :: POLYEQ_5:9

for z being Complex
for n0 being non zero Nat
for r being Real st r > 0 holds
n0 -root (z / r) = (n0 -root z) / (n0 -root r)