set FC = F_Complex ;
let s be non empty finite Subset of F_Complex; :: thesis: for x being Element of F_Complex
for r being FinSequence of REAL st len r = card s & ( for i being Element of NAT
for c being Element of F_Complex st i in dom r & c = () . i holds
r . i = |.(x - c).| ) holds
|.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r

let x be Element of F_Complex; :: thesis: for r being FinSequence of REAL st len r = card s & ( for i being Element of NAT
for c being Element of F_Complex st i in dom r & c = () . i holds
r . i = |.(x - c).| ) holds
|.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r

let r be FinSequence of REAL ; :: thesis: ( len r = card s & ( for i being Element of NAT
for c being Element of F_Complex st i in dom r & c = () . i holds
r . i = |.(x - c).| ) implies |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r )

assume that
A1: len r = card s and
A2: for i being Element of NAT
for c being Element of F_Complex st i in dom r & c = () . i holds
r . i = |.(x - c).| ; :: thesis: |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r
defpred S1[ set , set ] means ex c being Element of F_Complex st
( c = () . \$1 & \$2 = eval (<%(- c),()%>,x) );
len () = card s by FINSEQ_1:93;
then A3: dom () = Seg (card s) by FINSEQ_1:def 3;
A4: for k being Nat st k in Seg (card s) holds
ex y being Element of F_Complex st S1[k,y]
proof
let k be Nat; :: thesis: ( k in Seg (card s) implies ex y being Element of F_Complex st S1[k,y] )
assume A5: k in Seg (card s) ; :: thesis: ex y being Element of F_Complex st S1[k,y]
set c = () . k;
(canFS s) . k in s by ;
then reconsider c = () . k as Element of F_Complex ;
reconsider fi = eval (<%(- c),()%>,x) as Element of F_Complex ;
take fi ; :: thesis: S1[k,fi]
take c ; :: thesis: ( c = () . k & fi = eval (<%(- c),()%>,x) )
thus ( c = () . k & fi = eval (<%(- c),()%>,x) ) ; :: thesis: verum
end;
consider f being FinSequence of F_Complex such that
A6: dom f = Seg (card s) and
A7: for k being Nat st k in Seg (card s) holds
S1[k,f /. k] from
A8: now :: thesis: for i being Element of NAT
for c being Element of F_Complex st i in dom f & c = () . i holds
f . i = eval (<%(- c),()%>,x)
let i be Element of NAT ; :: thesis: for c being Element of F_Complex st i in dom f & c = () . i holds
f . i = eval (<%(- c),()%>,x)

let c be Element of F_Complex; :: thesis: ( i in dom f & c = () . i implies f . i = eval (<%(- c),()%>,x) )
assume that
A9: i in dom f and
A10: c = () . i ; :: thesis: f . i = eval (<%(- c),()%>,x)
ex c1 being Element of F_Complex st
( c1 = () . i & f /. i = eval (<%(- c1),()%>,x) ) by A6, A7, A9;
hence f . i = eval (<%(- c),()%>,x) by ; :: thesis: verum
end;
A11: dom r = Seg (card s) by ;
A12: for i being Element of NAT st i in dom f holds
|.(f /. i).| = r . i
proof
let i be Element of NAT ; :: thesis: ( i in dom f implies |.(f /. i).| = r . i )
set c = () . i;
assume A13: i in dom f ; :: thesis: |.(f /. i).| = r . i
then (canFS s) . i in s by ;
then reconsider c = () . i as Element of F_Complex ;
A14: f . i = eval (<%(- c),()%>,x) by ;
f /. i = f . i by
.= (- c) + x by
.= x - c ;
hence |.(f /. i).| = r . i by A2, A11, A6, A13; :: thesis: verum
end;
A15: len f = len r by ;
then eval ((poly_with_roots ((s,1) -bag)),x) = Product f by ;
hence |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r by ; :: thesis: verum