let a be Real; :: thesis: for n being Nat st a >= 0 & n >= 1 holds
n -root a >= 0
let n be Nat; :: thesis: ( a >= 0 & n >= 1 implies n -root a >= 0 )
assume that
A1: a >= 0 and
A2: n >= 1 ; :: thesis: n -root a >= 0

now :: thesis: n -root a >= 0

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

suppose A3: a > 0 ; :: thesis: n -root a >= 0

n -root a = n -Root a by A1, A2, Def1;
hence n -root a >= 0 by A2, A3, PREPOWER:def 2; :: thesis: verum

end;

suppose A4: a = 0 ; :: thesis: n -root a >= 0

n -root a = n -Root a by A1, A2, Def1
.= 0 by A2, A4, PREPOWER:def 2 ;
hence n -root a >= 0 ; :: thesis: verum

end;

end;

end;

hence n -root a >= 0 ; :: thesis: verum