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 = (canFS s) . 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 = (canFS s) . 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 = (canFS s) . 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 = (canFS s) . i holds
r . i = |.(x - c).| ; :: thesis: |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r
defpred S₁[ set , set ] means ex c being Element of F_Complex st
( c = (canFS s) . $1 & $2 = eval (<%(- c),(1_ F_Complex)%>,x) );
len (canFS s) = card s by FINSEQ_1:93;
then A3: dom (canFS s) = 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 S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg (card s) implies ex y being Element of F_Complex st S₁[k,y] )
assume A5: k in Seg (card s) ; :: thesis: ex y being Element of F_Complex st S₁[k,y]
set c = (canFS s) . k;
(canFS s) . k in s by A3, A5, FINSEQ_2:11;
then reconsider c = (canFS s) . k as Element of F_Complex ;
reconsider fi = eval (<%(- c),(1_ F_Complex)%>,x) as Element of F_Complex ;
take fi ; :: thesis: S₁[k,fi]
take c ; :: thesis: ( c = (canFS s) . k & fi = eval (<%(- c),(1_ F_Complex)%>,x) )
thus ( c = (canFS s) . k & fi = eval (<%(- c),(1_ F_Complex)%>,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
S₁[k,f /. k] from RECDEF_1:sch 17(A4);

A8: now :: thesis: for i being Element of NAT
for c being Element of F_Complex st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1_ F_Complex)%>,x)

let i be Element of NAT ; :: thesis: for c being Element of F_Complex st i in dom f & c = (canFS s) . i holds
f . i = eval (<%(- c),(1_ F_Complex)%>,x)
let c be Element of F_Complex; :: thesis: ( i in dom f & c = (canFS s) . i implies f . i = eval (<%(- c),(1_ F_Complex)%>,x) )
assume that
A9: i in dom f and
A10: c = (canFS s) . i ; :: thesis: f . i = eval (<%(- c),(1_ F_Complex)%>,x)
ex c1 being Element of F_Complex st
( c1 = (canFS s) . i & f /. i = eval (<%(- c1),(1_ F_Complex)%>,x) ) by A6, A7, A9;
hence f . i = eval (<%(- c),(1_ F_Complex)%>,x) by A9, A10, PARTFUN1:def 6; :: thesis: verum

end;

A11: dom r = Seg (card s) by A1, FINSEQ_1:def 3;
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 = (canFS s) . i;
assume A13: i in dom f ; :: thesis: |.(f /. i).| = r . i
then (canFS s) . i in s by A3, A6, FINSEQ_2:11;
then reconsider c = (canFS s) . i as Element of F_Complex ;
A14: f . i = eval (<%(- c),(1_ F_Complex)%>,x) by A8, A13;
f /. i = f . i by A13, PARTFUN1:def 6
.= (- c) + x by A14, POLYNOM5:47
.= x - c ;
hence |.(f /. i).| = r . i by A2, A11, A6, A13; :: thesis: verum

end;

A15: len f = len r by A1, A6, FINSEQ_1:def 3;
then eval ((poly_with_roots ((s,1) -bag)),x) = Product f by A1, A8, UPROOTS:67;
hence |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r by A15, A12, Th2; :: thesis: verum