let n be non empty 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 A1: v = 0 ; :: thesis: x = 0
A2: n >= 0 + 1 by NAT_1:13;
0 |^ n = x by A1, Def2;
hence x = 0 by A2, NEWTON:16; :: thesis: verum