for n being non zero Element of NAT
for x being Element of F_Complex
for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex