let x be Element of COMPLEX ; :: thesis: for v being CRoot of 1,x holds v = x
let v be CRoot of 1,x; :: thesis: v = x
v |^ 1 = x by Def2;
hence v = x ; :: thesis: verum