let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for c being Element of L holds poly_with_roots ({c},1 -bag ) = <%(- c),(1. L)%>
let c be Element of L; :: thesis: poly_with_roots ({c},1 -bag ) = <%(- c),(1. L)%>
set b = {c},1 -bag ;
consider f being FinSequence of the carrier of (Polynom-Ring L) * , s being FinSequence of L such that
A1: len f = card (support ({c},1 -bag )) and
A2: s = canFS (support ({c},1 -bag )) and
A3: for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root (s /. i),(({c},1 -bag ) . (s /. i)) and
A4: poly_with_roots ({c},1 -bag ) = Product (FlattenSeq f) by Def11;
A5: support ({c},1 -bag ) = {c} by Th10;
then A6: card (support ({c},1 -bag )) = 1 by CARD_1:50;
A7: f = <*(f /. 1)*> by A1, A5, CARD_1:50, FINSEQ_5:15;
A8: 1 in dom f by A1, A6, FINSEQ_3:27;
then f . 1 = f /. 1 by PARTFUN1:def 8;
then A9: FlattenSeq f = f . 1 by A7, DTCONSTR:13;
A10: f . 1 = fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1)) by A3, A8;
set f1 = fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1));
A11: s = <*c*> by A2, A5, Th6;
len s = 1 by A2, A6, Def1;
then 1 in dom s by FINSEQ_3:27;
then A12: s /. 1 = s . 1 by PARTFUN1:def 8
.= c by A11, FINSEQ_1:57 ;
c in {c} by TARSKI:def 1;
then ({c},1 -bag ) . (s /. 1) = 1 by A12, Th9;
then A13: len (fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) = 1 by Def10;
then A14: fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1)) = <*((fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) /. 1)*> by FINSEQ_5:15;
A15: 1 in dom (fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) by A13, FINSEQ_3:27;
thus poly_with_roots ({c},1 -bag ) = (fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) /. 1 by A4, A9, A10, A14, FINSOP_1:12
.= (fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) . 1 by A15, PARTFUN1:def 8
.= <%(- c),(1. L)%> by A12, A15, Def10 ; :: thesis: verum