let n be non empty Element of NAT ; :: thesis: unital_poly F_Complex ,n = poly_with_roots ((n -roots_of_1 ),1 -bag )
set p = unital_poly F_Complex ,n;
len (unital_poly F_Complex ,n) = n + 1 by Th44;
then (unital_poly F_Complex ,n) . ((len (unital_poly F_Complex ,n)) -' 1) = (unital_poly F_Complex ,n) . n by NAT_D:34
.= 1_ F_Complex by Th42 ;
hence unital_poly F_Complex ,n = poly_with_roots (BRoots (unital_poly F_Complex ,n)) by UPROOTS:67
.= poly_with_roots ((n -roots_of_1 ),1 -bag ) by Th49 ;
:: thesis: verum