:: deftheorem Def2 defines -Root PREPOWER:def 2 :
for n being natural Number
for a being Real st 1 <= n holds
for b₃ being Real holds
( ( a > 0 implies ( b₃ = n -Root a iff ( b₃ |^ n = a & b₃ > 0 ) ) ) & ( a = 0 implies ( b₃ = n -Root a iff b₃ = 0 ) ) );