let n be Nat; :: thesis: ( n >= 1 implies n -root 0 = 0 )
assume A1: n >= 1 ; :: thesis: n -root 0 = 0
hence n -root 0 = n -Root 0 by Def1
.= 0 by A1, PREPOWER:def 2 ;
:: thesis: verum