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 UPROOTS:5;
then A3: dom (canFS s) = Seg (card s) by FINSEQ_1:def 3;
A4: for k being Element of NAT st k in Seg (card s) holds
ex y being Element of F_Complex st S₁[k,y]

proof

let k be Element of 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:13;
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 Element of NAT st k in Seg (card s) holds
S₁[k,f /. k] from RECDEF_1:sch 17(A4);

A8: now

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 8; :: 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:13;
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 8
.= (- c) + x by A14, POLYNOM5:48
.= 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:69;
hence |.(eval (poly_with_roots (s,1 -bag )),x).| = Product r by A15, A12, Th3; :: thesis: verum