( n >= 1 & a >= 0 ) by NAT_1:14;
hence n -root (a |^ n) = a by POWER:4; :: thesis: verum