let x be Element of F_Complex; :: thesis: for v being CRoot of 1,x holds v = x
let v be CRoot of 1,x; :: thesis: v = x
(power F_Complex) . (v,1) = x by Def2;
hence v = x by GROUP_1:50; :: thesis: verum