let z be Complex; :: 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 ; :: thesis: verum