let n0 be non zero natural number ; :: thesis: for r being real number st r >= 0 holds
n0 -root r = n0 -real-root r
let r be real number ; :: thesis: ( r >= 0 implies n0 -root r = n0 -real-root r )
reconsider r9 = r as Real by XREAL_0:def 1;
assume A1: r >= 0 ; :: thesis: n0 -root r = n0 -real-root r
then Arg r9 = 0 by COMPTRIG:53;
hence n0 -root r = n0 -real-root r by A1, COMPLEX1:129, SIN_COS:34; :: thesis: verum