:: deftheorem Def1 defines -root POWER:def 1 :
for n being natural Number
for a being Real holds
( ( a >= 0 & n >= 1 implies n -root a = n -Root a ) & ( a < 0 & n is odd implies n -root a = - (n -Root (- a)) ) );