let n be Element of NAT ; :: thesis: ( n >= 1 implies n -root 1 = 1 )
assume A1: n >= 1 ; :: thesis: n -root 1 = 1
thus n -root 1 = n -Root 1 by A1, Def1
.= 1 by A1, PREPOWER:29 ; :: thesis: verum