let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>
let c be Element of L; 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 Def10;
A5:
support (({c},1) -bag) = {c}
by Th5;
then A6:
s = <*c*>
by A2, FINSEQ_1:94;
A7:
card (support (({c},1) -bag)) = 1
by A5, CARD_1:30;
then A8:
1 in dom f
by A1, FINSEQ_3:25;
then A9:
f . 1 = f /. 1
by PARTFUN1:def 6;
len s = 1
by A2, A7, FINSEQ_1:93;
then
1 in dom s
by FINSEQ_3:25;
then A10: s /. 1 =
s . 1
by PARTFUN1:def 6
.=
c
by A6
;
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 A10, Th4;
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 A1, A5, CARD_1:30, FINSEQ_5:14;
then A13:
FlattenSeq f = f . 1
by A9, PRE_POLY:1;
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 PARTFUN1:def 6, A12;
fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1))) = <*((fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) . 1)*>
by A11, FINSEQ_5:14;
hence poly_with_roots (({c},1) -bag) =
(fpoly_mult_root ((s /. 1),((({c},1) -bag) . (s /. 1)))) . 1
by A, A4, A13, A14, FINSOP_1:11
.=
<%(- c),(1. L)%>
by A10, A12, Def9
;
verum