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

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