set FC = F_Complex ;
let s be non empty finite Subset of F_Complex; 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; 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 ; ( 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).|
; |.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r
defpred S1[ 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 S1[k,y]
proof
let k be
Nat;
( k in Seg (card s) implies ex y being Element of F_Complex st S1[k,y] )
assume A5:
k in Seg (card s)
;
ex y being Element of F_Complex st S1[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
;
S1[k,fi]
take
c
;
( c = (canFS s) . k & fi = eval (<%(- c),(1_ F_Complex)%>,x) )
thus
(
c = (canFS s) . k &
fi = eval (
<%(- c),(1_ F_Complex)%>,
x) )
;
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 RECDEF_1:sch 17(A4);
A8:
now 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 ;
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;
( 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
;
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;
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 ;
( i in dom f implies |.(f /. i).| = r . i )
set c =
(canFS s) . i;
assume A13:
i in dom f
;
|.(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;
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; verum