let a be real number ; :: thesis: for n being Element of NAT st a >= 0 & n >= 1 holds
a to_power (1 / n) = n -root a
let n be Element of NAT ; :: thesis: ( a >= 0 & n >= 1 implies a to_power (1 / n) = n -root a )
assume A1: ( a >= 0 & n >= 1 ) ; :: thesis: a to_power (1 / n) = n -root a
reconsider p = n " as Rational ;
A3: 1 / n > 0 by A1;

now

per cases ( a > 0 or a = 0 ) by A1;

suppose A4: a > 0 ; :: thesis: a to_power (1 / n) = n -Root a

hence a to_power (1 / n) = a #Q p by Th51
.= n -Root a by A1, A4, PREPOWER:61 ;
:: thesis: verum

end;

suppose A5: a = 0 ; :: thesis: a to_power (1 / n) = n -Root a

hence a to_power (1 / n) = 0 by A3, Def2
.= n -Root a by A1, A5, PREPOWER:def 3 ;
:: thesis: verum

end;

end;

end;

hence a to_power (1 / n) = n -root a by A1, Def1; :: thesis: verum