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 () * , 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 () by Def10;
A5: support (({c},1) -bag) = {c} by Th5;
then A6: s = <*c*> by ;
A7: card (support (({c},1) -bag)) = 1 by ;
then A8: 1 in dom f by ;
then A9: f . 1 = f /. 1 by PARTFUN1:def 6;
len s = 1 by ;
then 1 in dom s by FINSEQ_3:25;
then A10: s /. 1 = s . 1 by PARTFUN1:def 6
.= c by ;
set f1 = fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)));
c in {c} by TARSKI:def 1;
then (({c},1) -bag) . (s /. 1) = 1 by ;
then A11: len (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) = 1 by Def9;
then A12: 1 in dom (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) by FINSEQ_3:25;
f = <*(f . 1)*> by ;
then A13: FlattenSeq f = f . 1 by ;
A14: f . 1 = fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1))) by A3, A8;
A: (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) . 1 = (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) /. 1 by ;
fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1))) = <*((fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) . 1)*> by ;
hence poly_with_roots (({c},1) -bag) = (fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) . 1 by
.= <%(- c),(1. L)%> by ;
:: thesis: verum