let z be complex number ; :: thesis: for v being CRoot of 1,z holds v = z
let v be CRoot of 1,z; :: thesis: v = z
v |^ 1 = z by COMPTRIG:def 2;
hence v = z by NEWTON:10; :: thesis: verum