theorem Th8: :: POLYEQ_5:8

for n0 being non zero Nat
for r being Real st r >= 0 holds
n0 -root r = n0 -real-root r