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_{1}[ 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_{1}[k,y]

A6: dom f = Seg (card s) and

A7: for k being Nat st k in Seg (card s) holds

S_{1}[k,f /. k]
from RECDEF_1:sch 17(A4);

A12: for i being Element of NAT st i in dom f holds

|.(f /. i).| = r . i

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

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

( 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

proof

consider f being FinSequence of F_Complex such that
let k be Nat; :: thesis: ( k in Seg (card s) implies ex y being Element of F_Complex st S_{1}[k,y] )

assume A5: k in Seg (card s) ; :: thesis: ex y being Element of F_Complex st S_{1}[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_{1}[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;assume A5: k in Seg (card s) ; :: thesis: ex y being Element of F_Complex st S

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

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

A6: dom f = Seg (card s) and

A7: for k being Nat st k in Seg (card s) holds

S

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)

A11:
dom r = Seg (card s)
by A1, FINSEQ_1:def 3;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;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

A12: for i being Element of NAT st i in dom f holds

|.(f /. i).| = r . i

proof

A15:
len f = len r
by A1, A6, FINSEQ_1:def 3;
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;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

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