let n be non zero Element of NAT ; :: thesis: BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag

set p = unital_poly (F_Complex,n);

A1: degree (BRoots (unital_poly (F_Complex,n))) = (len (unital_poly (F_Complex,n))) -' 1 by UPROOTS:59

.= (n + 1) -' 1 by Th40

.= n by NAT_D:34 ;

A2: card (n -roots_of_1) = n by Th27;

( Roots (unital_poly (F_Complex,n)) = n -roots_of_1 & support (BRoots (unital_poly (F_Complex,n))) = Roots (unital_poly (F_Complex,n)) ) by Th42, UPROOTS:def 9;

hence BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag by A1, A2, UPROOTS:13; :: thesis: verum

set p = unital_poly (F_Complex,n);

A1: degree (BRoots (unital_poly (F_Complex,n))) = (len (unital_poly (F_Complex,n))) -' 1 by UPROOTS:59

.= (n + 1) -' 1 by Th40

.= n by NAT_D:34 ;

A2: card (n -roots_of_1) = n by Th27;

( Roots (unital_poly (F_Complex,n)) = n -roots_of_1 & support (BRoots (unital_poly (F_Complex,n))) = Roots (unital_poly (F_Complex,n)) ) by Th42, UPROOTS:def 9;

hence BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag by A1, A2, UPROOTS:13; :: thesis: verum