let n be non zero Element of NAT ; :: thesis: for z being Complex
for v being CRoot of n,z st v = 0 holds
z = 0
let z be Complex; :: thesis: for v being CRoot of n,z st v = 0 holds
z = 0
let v be CRoot of n,z; :: thesis: ( v = 0 implies z = 0 )
assume v = 0 ; :: thesis: z = 0
then 0 |^ n = z by COMPTRIG:def 2;
hence z = 0 by Lm2; :: thesis: verum