let n be non zero 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 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 ;

:: thesis: verum

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 ;

:: thesis: verum