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 Def11;
A5:
support ({c},1 -bag ) = {c}
by Th10;
then A6:
s = <*c*>
by A2, Th6;
A7:
card (support ({c},1 -bag )) = 1
by A5, CARD_1:50;
then A8:
1 in dom f
by A1, FINSEQ_3:27;
then A9:
f . 1 = f /. 1
by PARTFUN1:def 8;
len s = 1
by A2, A7, Th5;
then
1 in dom s
by FINSEQ_3:27;
then A10: s /. 1 =
s . 1
by PARTFUN1:def 8
.=
c
by A6, FINSEQ_1:57
;
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, Th9;
then A11:
len (fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) = 1
by Def10;
then A12:
1 in dom (fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1)))
by FINSEQ_3:27;
f = <*(f /. 1)*>
by A1, A5, CARD_1:50, FINSEQ_5:15;
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;
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:15;
hence poly_with_roots ({c},1 -bag ) =
(fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) /. 1
by A4, A13, A14, FINSOP_1:12
.=
(fpoly_mult_root (s /. 1),(({c},1 -bag ) . (s /. 1))) . 1
by A12, PARTFUN1:def 8
.=
<%(- c),(1. L)%>
by A10, A12, Def10
;
verum