let L be non trivial comRing; :: thesis: for s being non empty finite Subset of L
for x being Element of L
for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = () . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f

set cL = the carrier of L;
let s be non empty finite Subset of the carrier of L; :: thesis: for x being Element of L
for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = () . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f

let x be Element of the carrier of L; :: thesis: for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = () . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f

let f be FinSequence of L; :: thesis: ( len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = () . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) implies eval ((poly_with_roots ((s,1) -bag)),x) = Product f )

assume that
A1: len f = card s and
A2: for i being Element of NAT
for c being Element of the carrier of L st i in dom f & c = () . i holds
f . i = eval (<%(- c),(1. L)%>,x) ; :: thesis: eval ((poly_with_roots ((s,1) -bag)),x) = Product f
set cs = canFS s;
A3: rng () = s by FUNCT_2:def 3;
defpred S1[ Nat] means ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of L st
( t = rng (() | (Seg \$1)) & g = f | (Seg \$1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g );
A4: len () = card s by FINSEQ_1:93;
then A5: dom f = dom () by ;
A6: for j being Element of NAT st 1 <= j & j < len f & S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; :: thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] )
assume that
A7: 1 <= j and
A8: j < len f ; :: thesis: ( not S1[j] or S1[j + 1] )
reconsider g1 = f | (Seg (j + 1)) as FinSequence of the carrier of L by FINSEQ_1:18;
A9: j + 1 <= len f by ;
then ex l being Nat st len f = (j + 1) + l by NAT_1:10;
then A10: len g1 = j + 1 by FINSEQ_3:53;
1 <= j + 1 by ;
then A11: j + 1 in dom () by ;
then (canFS s) . (j + 1) in s by FINSEQ_2:11;
then reconsider csj1 = () . (j + 1) as Element of the carrier of L ;
A12: g1 . (j + 1) = f . (j + 1) by
.= eval (<%(- csj1),(1. L)%>,x) by A2, A5, A11 ;
reconsider csja1 = () | (Seg (j + 1)) as FinSequence of s by FINSEQ_1:18;
reconsider csja = () | (Seg j) as FinSequence of s by FINSEQ_1:18;
given t being finite Subset of the carrier of L, g being FinSequence of the carrier of L such that A13: t = rng (() | (Seg j)) and
A14: g = f | (Seg j) and
A15: eval ((poly_with_roots ((t,1) -bag)),x) = Product g ; :: thesis: S1[j + 1]
j <= j + 1 by NAT_1:12;
then Seg j c= Seg (j + 1) by FINSEQ_1:5;
then g = g1 | (Seg j) by ;
then A16: g1 = g ^ <*(eval (<%(- csj1),(1. L)%>,x))*> by ;
reconsider pt = poly_with_roots ((t,1) -bag) as Polynomial of L ;
set t1 = rng csja1;
Seg (j + 1) = (Seg j) \/ {(j + 1)} by FINSEQ_1:9;
then A17: csja1 = csja \/ (() | {(j + 1)}) by RELAT_1:78;
(canFS s) | {(j + 1)} = (j + 1) .--> csj1 by ;
then rng (() | {(j + 1)}) = {csj1} by FUNCOP_1:8;
then A18: rng csja1 = t \/ {csj1} by ;
then reconsider t1 = rng csja1 as finite Subset of the carrier of L ;
take t1 ; :: thesis: ex g being FinSequence of the carrier of L st
( t1 = rng (() | (Seg (j + 1))) & g = f | (Seg (j + 1)) & eval ((poly_with_roots ((t1,1) -bag)),x) = Product g )

take g1 ; :: thesis: ( t1 = rng (() | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & eval ((poly_with_roots ((t1,1) -bag)),x) = Product g1 )
thus ( t1 = rng (() | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) ) ; :: thesis: eval ((poly_with_roots ((t1,1) -bag)),x) = Product g1
reconsider pj1 = poly_with_roots (({csj1},1) -bag) as Polynomial of L ;
A19: pj1 = <%(- csj1),(1. L)%> by Th58;
t misses {csj1}
proof
assume not t misses {csj1} ; :: thesis: contradiction
then t /\ {csj1} <> {} by XBOOLE_0:def 7;
then consider x being object such that
A20: x in t /\ {csj1} by XBOOLE_0:def 1;
x in {csj1} by ;
then A21: x = csj1 by TARSKI:def 1;
x in t by ;
then consider i being object such that
A22: i in dom (() | (Seg j)) and
A23: x = (() | (Seg j)) . i by ;
A24: i in Seg j by ;
reconsider i = i as Element of NAT by A22;
A25: 1 <= i by ;
i <= j by ;
then A26: i < j + 1 by NAT_1:13;
x = () . i by ;
hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7; :: thesis: verum
end;
then (t1,1) -bag = ((t,1) -bag) + (({csj1},1) -bag) by ;
then poly_with_roots ((t1,1) -bag) = pt *' pj1 by Th61;
hence eval ((poly_with_roots ((t1,1) -bag)),x) = () * (eval (pj1,x)) by
.= Product g1 by ;
:: thesis: verum
end;
f | (Seg (len f)) is FinSequence by FINSEQ_1:18;
then A27: ( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f ) by ;
A28: 0 + 1 <= len f by ;
A29: S1
proof
1 in dom () by ;
then reconsider cs1 = () . 1 as Element of s by FINSEQ_2:11;
reconsider g = f | (Seg 1) as FinSequence of the carrier of L by FINSEQ_1:18;
reconsider cs1a = () | (Seg 1) as FinSequence of s by FINSEQ_1:18;
A30: cs1 in the carrier of L ;
A31: 1 in Seg 1 by FINSEQ_1:1;
then A32: cs1a . 1 = cs1 by FUNCT_1:49;
reconsider cs1 = () . 1 as Element of the carrier of L by A30;
reconsider t = {cs1} as finite Subset of the carrier of L ;
take t ; :: thesis: ex g being FinSequence of the carrier of L st
( t = rng (() | (Seg 1)) & g = f | (Seg 1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g )

take g ; :: thesis: ( t = rng (() | (Seg 1)) & g = f | (Seg 1) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g )
consider s1 being Element of s such that
A33: cs1a = <*s1*> by ;
cs1a . 1 = s1 by ;
hence ( t = rng (() | (Seg 1)) & g = f | (Seg 1) ) by ; :: thesis: eval ((poly_with_roots ((t,1) -bag)),x) = Product g
consider p1 being Element of the carrier of L such that
A34: g = <*p1*> by ;
A35: ( g . 1 = p1 & Product g = p1 ) by ;
A36: 1 in dom f by ;
then reconsider f1 = f . 1 as Element of the carrier of L by FINSEQ_2:11;
A37: g . 1 = f1 by ;
f1 = eval (<%(- cs1),(1. L)%>,x) by ;
hence eval ((poly_with_roots ((t,1) -bag)),x) = Product g by ; :: thesis: verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S1[i] from INT_1:sch 7(A29, A6);
then ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of L st
( t = rng (() | (Seg (len f))) & g = f | (Seg (len f)) & eval ((poly_with_roots ((t,1) -bag)),x) = Product g ) by A28;
hence eval ((poly_with_roots ((s,1) -bag)),x) = Product f by ; :: thesis: verum