assume n -root a is heavy ; :: thesis: contradiction
then (n -root a) |^ n is heavy ;
hence contradiction by POLYEQ_5:7; :: thesis: verum