let n be non empty Element of NAT ; :: thesis: BRoots (unital_poly F_Complex ,n) = (n -roots_of_1 ),1 -bag
set p = unital_poly F_Complex ,n;
A1: Roots (unital_poly F_Complex ,n) = n -roots_of_1 by Th46;
A2: support (BRoots (unital_poly F_Complex ,n)) = Roots (unital_poly F_Complex ,n) by UPROOTS:def 9;
A3: degree (BRoots (unital_poly F_Complex ,n)) = (len (unital_poly F_Complex ,n)) -' 1 by UPROOTS:61
.= (n + 1) -' 1 by Th44
.= n by NAT_D:34 ;
card (n -roots_of_1 ) = n by Th30;
hence BRoots (unital_poly F_Complex ,n) = (n -roots_of_1 ),1 -bag by A1, A2, A3, UPROOTS:15; :: thesis: verum