let n be non zero Element of NAT ; :: thesis: for x being Element of F_Complex
for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex
let x be Element of F_Complex; :: thesis: for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex
let v be CRoot of n,x; :: thesis: ( v = 0. F_Complex implies x = 0. F_Complex )
assume v = 0. F_Complex ; :: thesis: x = 0. F_Complex
then (power F_Complex) . ((0. F_Complex),n) = x by Def2;
hence x = 0. F_Complex by NAT_1:3, VECTSP_1:36; :: thesis: verum