let n be non zero Nat; :: thesis: for x being Element of COMPLEX
for v being CRoot of n,x st v = 0 holds
x = 0
let x be Element of COMPLEX ; :: thesis: for v being CRoot of n,x st v = 0 holds
x = 0
let v be CRoot of n,x; :: thesis: ( v = 0 implies x = 0 )
assume v = 0 ; :: thesis: x = 0
then ( n >= 0 + 1 & 0 |^ n = x ) by Def2, NAT_1:13;
hence x = 0 by NEWTON:11; :: thesis: verum