let L be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr ; :: thesis: poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%>
set b = EmptyBag the carrier of L;
consider f being FinSequence of the carrier of (Polynom-Ring L) * , s being FinSequence of L such that
A1: len f = card (support (EmptyBag the carrier of L)) and
s = canFS (support (EmptyBag the carrier of L)) and
for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),((EmptyBag the carrier of L) . (s /. i))) and
A2: poly_with_roots (EmptyBag the carrier of L) = Product (FlattenSeq f) by Def10;
f = <*> ( the carrier of (Polynom-Ring L) *) by A1;
then ( 1_ (Polynom-Ring L) = 1. (Polynom-Ring L) & FlattenSeq f = <*> the carrier of (Polynom-Ring L) ) ;
then Product (FlattenSeq f) = 1. (Polynom-Ring L) by GROUP_4:8
.= 1_. L by POLYNOM3:37 ;
hence poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%> by A2, Th28; :: thesis: verum