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:98; :: thesis: verum