let n be non zero Element of NAT ; 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 Th40;
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 Th38
;
hence unital_poly (F_Complex,n) =
poly_with_roots (BRoots (unital_poly (F_Complex,n)))
by UPROOTS:65
.=
poly_with_roots (((n -roots_of_1),1) -bag)
by Th45
;
verum