set cMGFC = the carrier of ;
set cPRFC = the carrier of ;
let n, ni be non zero Element of NAT ; :: thesis: for f being FinSequence of the carrier of
for s being finite Subset of F_Complex st s = { y where y is Element of : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds
Product f = poly_with_roots ((s,1) -bag)

let f be FinSequence of the carrier of ; :: thesis: for s being finite Subset of F_Complex st s = { y where y is Element of : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds
Product f = poly_with_roots ((s,1) -bag)

let s be finite Subset of F_Complex; :: thesis: ( s = { y where y is Element of : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) implies Product f = poly_with_roots ((s,1) -bag) )

assume that
A1: s = { y where y is Element of the carrier of : ( ord y divides n & not ord y divides ni & ord y <> n ) } and
A2: dom f = Seg n and
A3: for i being non zero Element of NAT st i in dom f holds
( ( ( not i divides n or i divides ni or i = n ) implies f . i = ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; :: thesis: Product f = poly_with_roots ((s,1) -bag)
deffunc H1( Nat) -> set = { y where y is Element of the carrier of : ( y in s & ord y <= \$1 ) } ;
A4: now :: thesis: for i being Element of NAT holds H1(i) is finite Subset of F_Complex
let i be Element of NAT ; :: thesis: H1(i) is finite Subset of F_Complex
H1(i) c= s
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(i) or x in s )
assume x in H1(i) ; :: thesis: x in s
then ex y being Element of the carrier of st
( x = y & y in s & ord y <= i ) ;
hence x in s ; :: thesis: verum
end;
hence H1(i) is finite Subset of F_Complex by XBOOLE_1:1; :: thesis: verum
end;
then reconsider sB = H1(n) as finite Subset of F_Complex ;
A5: len f = n by ;
defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of st fi = f | (Seg \$1) holds
\$2 = Product fi;
A6: now :: thesis: for i being Nat st i in Seg (len f) holds
ex x being Element of the carrier of st S1[i,x]
let i be Nat; :: thesis: ( i in Seg (len f) implies ex x being Element of the carrier of st S1[i,x] )
assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of st S1[i,x]
reconsider fi = f | (Seg i) as FinSequence of the carrier of by FINSEQ_1:18;
set x = Product fi;
take x = Product fi; :: thesis: S1[i,x]
thus S1[i,x] ; :: thesis: verum
end;
consider F being FinSequence of the carrier of such that
dom F = Seg (len f) and
A7: for i being Nat st i in Seg (len f) holds
S1[i,F . i] from defpred S2[ Nat] means ex t being finite Subset of F_Complex st
( t = H1(\$1) & F . \$1 = poly_with_roots ((t,1) -bag) );
A8: for i being Element of NAT st 1 <= i & i < len f & S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] )
assume that
A9: 1 <= i and
A10: i < len f and
A11: S2[i] ; :: thesis: S2[i + 1]
reconsider fi = f | (Seg i) as FinSequence of the carrier of by FINSEQ_1:18;
i in Seg (len f) by ;
then A12: F . i = Product fi by A7;
reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of by FINSEQ_1:18;
A13: i + 1 <= len f by ;
then i + 1 = min ((i + 1),(len f)) by XXREAL_0:def 9;
then A14: len fi1 = i + 1 by FINSEQ_2:21;
i + 1 in NAT by ORDINAL1:def 12;
then reconsider sB = H1(i + 1) as finite Subset of F_Complex by A4;
take sB ; :: thesis: ( sB = H1(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) )
thus sB = H1(i + 1) ; :: thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag)
set B = (sB,1) -bag ;
consider sb being finite Subset of F_Complex such that
A15: sb = H1(i) and
A16: F . i = poly_with_roots ((sb,1) -bag) by A11;
1 <= i + 1 by ;
then A17: i + 1 in Seg (len f) by ;
then A18: i + 1 in dom f by FINSEQ_1:def 3;
A19: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by ;
then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of by ;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
A20: F . (i + 1) = Product fi1 by ;
set b = (sb,1) -bag ;
fi = fi1 | (Seg i) by ;
then fi1 = fi ^ <*fi1d1*> by ;
then Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;
then A21: Product fi1 = (poly_with_roots ((sb,1) -bag)) *' fi1d1p by ;
per cases ( not i + 1 divides n or i + 1 divides ni or i + 1 = n or ( i + 1 divides n & not i + 1 divides ni & i + 1 <> n ) ) ;
suppose A22: ( not i + 1 divides n or i + 1 divides ni or i + 1 = n ) ; :: thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag)
A23: now :: thesis: for x being object holds
( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )
let x be object ; :: thesis: ( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )
hereby :: thesis: ( x in sb implies x in sB )
assume x in sB ; :: thesis: x in sb
then consider y being Element of such that
A24: x = y and
A25: y in s and
A26: ord y <= i + 1 ;
ex y1 being Element of the carrier of st
( y = y1 & ord y1 divides n & not ord y1 divides ni & ord y1 <> n ) by ;
then ord y < i + 1 by ;
then ord y <= i by NAT_1:13;
hence x in sb by ; :: thesis: verum
end;
assume x in sb ; :: thesis: x in sB
then consider y being Element of such that
A27: ( x = y & y in s ) and
A28: ord y <= i by A15;
ord y <= i + 1 by ;
hence x in sB by A27; :: thesis: verum
end;
f . (i + 1) = by A3, A18, A22;
then F . (i + 1) = poly_with_roots ((sb,1) -bag) by
.= poly_with_roots ((sB,1) -bag) by ;
hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis: verum
end;
suppose A29: ( i + 1 divides n & not i + 1 divides ni & i + 1 <> n ) ; :: thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag)
consider scb being non empty finite Subset of F_Complex such that
A30: scb = { y where y is Element of the carrier of : ord y = i + 1 } and
A31: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5;
now :: thesis: for x being object holds
( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies x in sB ) )
let x be object ; :: thesis: ( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies b1 in sB ) )
hereby :: thesis: ( x in sb \/ scb implies b1 in sB )
assume x in sB ; :: thesis: x in sb \/ scb
then consider y being Element of the carrier of such that
A32: x = y and
A33: y in s and
A34: ord y <= i + 1 ;
( ord y <= i or ord y = i + 1 ) by ;
then ( y in sb or y in scb ) by ;
hence x in sb \/ scb by ; :: thesis: verum
end;
assume A35: x in sb \/ scb ; :: thesis: b1 in sB
per cases ( x in sb or x in scb ) by ;
suppose x in sb ; :: thesis: b1 in sB
then consider y being Element of the carrier of such that
A36: ( x = y & y in s ) and
A37: ord y <= i by A15;
ord y <= i + 1 by ;
hence x in sB by A36; :: thesis: verum
end;
suppose x in scb ; :: thesis: b1 in sB
then consider y being Element of the carrier of such that
A38: x = y and
A39: ord y = i + 1 by A30;
y in s by A1, A29, A39;
hence x in sB by ; :: thesis: verum
end;
end;
end;
then A40: sB = sb \/ scb by TARSKI:2;
set cb = (scb,1) -bag ;
A41: sb misses scb
proof
assume sb /\ scb <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being object such that
A42: x in sb /\ scb by XBOOLE_0:def 1;
x in scb by ;
then A43: ex y2 being Element of the carrier of st
( x = y2 & ord y2 = i + 1 ) by A30;
x in sb by ;
then ex y1 being Element of the carrier of st
( x = y1 & y1 in s & ord y1 <= i ) by A15;
hence contradiction by A43, NAT_1:13; :: thesis: verum
end;
f . (i + 1) = poly_with_roots ((scb,1) -bag) by A3, A18, A29, A31;
then F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ((scb,1) -bag)) by A7, A17, A19, A21
.= poly_with_roots (((sb,1) -bag) + ((scb,1) -bag)) by UPROOTS:64
.= poly_with_roots ((sB,1) -bag) by ;
hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis: verum
end;
end;
end;
now :: thesis: for x being object holds
( ( x in s implies x in sB ) & ( x in sB implies x in s ) )
let x be object ; :: thesis: ( ( x in s implies x in sB ) & ( x in sB implies x in s ) )
hereby :: thesis: ( x in sB implies x in s )
assume A44: x in s ; :: thesis: x in sB
then consider y being Element of such that
A45: x = y and
A46: ord y divides n and
not ord y divides ni and
ord y <> n by A1;
ord y <= n by ;
hence x in sB by ; :: thesis: verum
end;
assume x in sB ; :: thesis: x in s
then ex y being Element of st
( y = x & y in s & ord y <= n ) ;
hence x in s ; :: thesis: verum
end;
then A47: s = sB by TARSKI:2;
A48: 0 + 1 <= n by NAT_1:13;
A49: S2
proof
reconsider t = H1(1) as finite Subset of F_Complex by A4;
take t ; :: thesis: ( t = H1(1) & F . 1 = poly_with_roots ((t,1) -bag) )
thus t = H1(1) ; :: thesis: F . 1 = poly_with_roots ((t,1) -bag)
reconsider f1 = f | (Seg 1) as FinSequence of the carrier of by FINSEQ_1:18;
A50: 1 in dom f by ;
A51: 1 divides ni by NAT_D:6;
now :: thesis: t is empty
assume not t is empty ; :: thesis: contradiction
then consider x being object such that
A52: x in t ;
consider y being Element of the carrier of such that
x = y and
A53: y in s and
A54: ord y <= 1 by A52;
consider y1 being Element of the carrier of such that
A55: y = y1 and
A56: ord y1 divides n and
A57: not ord y1 divides ni and
ord y1 <> n by ;
now :: thesis: not ord y1 = 0
assume ord y1 = 0 ; :: thesis: contradiction
then ex u being Nat st n = 0 * u by ;
hence contradiction ; :: thesis: verum
end;
then 0 + 1 <= ord y1 by NAT_1:13;
hence contradiction by A51, A54, A55, A57, XXREAL_0:1; :: thesis: verum
end;
then A58: (t,1) -bag = EmptyBag the carrier of F_Complex by UPROOTS:9;
A59: 1 in Seg (len f) by ;
then 1 in dom f by FINSEQ_1:def 3;
then reconsider fd1 = f . 1 as Element of the carrier of by FINSEQ_2:11;
f1 = <*(f . 1)*> by A5, A48, Th1;
then F . 1 = Product <*fd1*> by
.= fd1 by FINSOP_1:11
.= by A3, A50, A51 ;
hence F . 1 = poly_with_roots ((t,1) -bag) by ; :: thesis: verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S2[i] from INT_1:sch 7(A49, A8);
then ( f = f | (Seg (len f)) & ex S being finite Subset of F_Complex st
( S = H1( len f) & F . (len f) = poly_with_roots ((S,1) -bag) ) ) by ;
hence Product f = poly_with_roots ((s,1) -bag) by ; :: thesis: verum