let n0 be non zero Nat; :: thesis: for r being Real st r >= 0 holds
n0 -root r = n0 -real-root r
let r be Real; :: thesis: ( r >= 0 implies n0 -root r = n0 -real-root r )
reconsider r9 = r as Real ;
assume A1: r >= 0 ; :: thesis: n0 -root r = n0 -real-root r
then Arg r9 = 0 by COMPTRIG:35;
hence n0 -root r = n0 -real-root r by A1, COMPLEX1:43, SIN_COS:31; :: thesis: verum