set cMGFC = the carrier of (MultGroup F_Complex);
set cPRFC = the carrier of (Polynom-Ring F_Complex);
let n, ni be non zero Element of NAT ; :: thesis:
let f be FinSequence of the carrier of (Polynom-Ring F_Complex); :: thesis:
let s be finite Subset of F_Complex; :: thesis:
assume that
A1: s = { y where y is Element of the carrier of (MultGroup F_Complex) : ( 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 = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; :: thesis:
deffunc H₁( Nat) -> set = { y where y is Element of the carrier of (MultGroup F_Complex) : ( y in s & ord y <= $1 ) } ;

A4: now :: thesis:

let i be Element of NAT ; :: thesis:
H₁(i) c= s

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in H₁(i) ; :: thesis:
then ex y being Element of the carrier of (MultGroup F_Complex) st
( x = y & y in s & ord y <= i ) ;
hence x in s ; :: thesis:

end;

hence H₁(i) is finite Subset of F_Complex by XBOOLE_1:1; :: thesis:

end;

then reconsider sB = H₁(n) as finite Subset of F_Complex ;
A5: len f = n by A2, FINSEQ_1:def 3;
defpred S₁[ Nat, set ] means for fi being FinSequence of the carrier of (Polynom-Ring F_Complex) st fi = f | (Seg $1) holds
$2 = Product fi;

A6: now :: thesis:

let i be Nat; :: thesis:
assume i in Seg (len f) ; :: thesis:
reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
set x = Product fi;
take x = Product fi; :: thesis:
thus S₁[i,x] ; :: thesis:

end;

consider F being FinSequence of the carrier of (Polynom-Ring F_Complex) such that
dom F = Seg (len f) and
A7: for i being Nat st i in Seg (len f) holds
S₁[i,F . i] from FINSEQ_1:sch 5(A6);
defpred S₂[ Nat] means ex t being finite Subset of F_Complex st
( t = H₁($1) & F . $1 = poly_with_roots ((t,1) -bag) );
A8: for i being Element of NAT st 1 <= i & i < len f & S₂[i] holds
S₂[i + 1]

proof

let i be Element of NAT ; :: thesis:
assume that
A9: 1 <= i and
A10: i < len f and
A11: S₂[i] ; :: thesis:
reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
i in Seg (len f) by A9, A10, FINSEQ_1:1;
then A12: F . i = Product fi by A7;
reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
A13: i + 1 <= len f by A10, NAT_1:13;
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 = H₁(i + 1) as finite Subset of F_Complex by A4;
take sB ; :: thesis:
thus sB = H₁(i + 1) ; :: thesis:
set B = (sB,1) -bag ;
consider sb being finite Subset of F_Complex such that
A15: sb = H₁(i) and
A16: F . i = poly_with_roots ((sb,1) -bag) by A11;
1 <= i + 1 by A9, NAT_1:13;
then A17: i + 1 in Seg (len f) by A13, FINSEQ_1:1;
then A18: i + 1 in dom f by FINSEQ_1:def 3;
A19: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by FINSEQ_1:4, FUNCT_1:49;
then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A18, FINSEQ_2:11;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
A20: F . (i + 1) = Product fi1 by A7, A17;
set b = (sb,1) -bag ;
fi = fi1 | (Seg i) by Lm2, NAT_1:12;
then fi1 = fi ^ <*fi1d1*> by A14, FINSEQ_3:55;
then Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;
then A21: Product fi1 = (poly_with_roots ((sb,1) -bag)) *' fi1d1p by A12, A16, POLYNOM3:def 10;

per cases ;

suppose A22: ( not i + 1 divides n or i + 1 divides ni or i + 1 = n ) ; :: thesis:

A23: now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in sB ; :: thesis:
then consider y being Element of (MultGroup F_Complex) such that
A24: x = y and
A25: y in s and
A26: ord y <= i + 1 ;
ex y1 being Element of the carrier of (MultGroup F_Complex) st
( y = y1 & ord y1 divides n & not ord y1 divides ni & ord y1 <> n ) by A1, A25;
then ord y < i + 1 by A22, A26, XXREAL_0:1;
then ord y <= i by NAT_1:13;
hence x in sb by A15, A24, A25; :: thesis:

end;

assume x in sb ; :: thesis:
then consider y being Element of (MultGroup F_Complex) such that
A27: ( x = y & y in s ) and
A28: ord y <= i by A15;
ord y <= i + 1 by A28, NAT_1:12;
hence x in sB by A27; :: thesis:

end;

f . (i + 1) = <%(1_ F_Complex)%> by A3, A18, A22;
then F . (i + 1) = poly_with_roots ((sb,1) -bag) by A20, A19, A21, UPROOTS:32
.= poly_with_roots ((sB,1) -bag) by A23, TARSKI:2 ;
hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis:

end;

suppose A29: ( i + 1 divides n & not i + 1 divides ni & i + 1 <> n ) ; :: thesis:

consider scb being non empty finite Subset of F_Complex such that
A30: scb = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = i + 1 } and
A31: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in sB ; :: thesis:
then consider y being Element of the carrier of (MultGroup F_Complex) 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 A34, NAT_1:8;
then ( y in sb or y in scb ) by A15, A30, A33;
hence x in sb \/ scb by A32, XBOOLE_0:def 3; :: thesis:

end;

assume A35: x in sb \/ scb ; :: thesis:

per cases by A35, XBOOLE_0:def 3;

suppose x in sb ; :: thesis:

then consider y being Element of the carrier of (MultGroup F_Complex) such that
A36: ( x = y & y in s ) and
A37: ord y <= i by A15;
ord y <= i + 1 by A37, NAT_1:12;
hence x in sB by A36; :: thesis:

end;

suppose x in scb ; :: thesis:

then consider y being Element of the carrier of (MultGroup F_Complex) 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 A38, A39; :: thesis:

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:
then consider x being object such that
A42: x in sb /\ scb by XBOOLE_0:def 1;
x in scb by A42, XBOOLE_0:def 4;
then A43: ex y2 being Element of the carrier of (MultGroup F_Complex) st
( x = y2 & ord y2 = i + 1 ) by A30;
x in sb by A42, XBOOLE_0:def 4;
then ex y1 being Element of the carrier of (MultGroup F_Complex) st
( x = y1 & y1 in s & ord y1 <= i ) by A15;
hence contradiction by A43, NAT_1:13; :: thesis:

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 A40, A41, UPROOTS:10 ;
hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume A44: x in s ; :: thesis:
then consider y being Element of (MultGroup F_Complex) 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 A46, NAT_D:7;
hence x in sB by A44, A45; :: thesis:

end;

assume x in sB ; :: thesis:
then ex y being Element of (MultGroup F_Complex) st
( y = x & y in s & ord y <= n ) ;
hence x in s ; :: thesis:

end;

then A47: s = sB by TARSKI:2;
A48: 0 + 1 <= n by NAT_1:13;
A49: S₂[1]

proof

reconsider t = H₁(1) as finite Subset of F_Complex by A4;
take t ; :: thesis:
thus t = H₁(1) ; :: thesis:
reconsider f1 = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
A50: 1 in dom f by A5, A48, FINSEQ_3:25;
A51: 1 divides ni by NAT_D:6;

now :: thesis:

assume not t is empty ; :: thesis:
then consider x being object such that
A52: x in t ;
consider y being Element of the carrier of (MultGroup F_Complex) such that
x = y and
A53: y in s and
A54: ord y <= 1 by A52;
consider y1 being Element of the carrier of (MultGroup F_Complex) such that
A55: y = y1 and
A56: ord y1 divides n and
A57: not ord y1 divides ni and
ord y1 <> n by A1, A53;

now :: thesis:

assume ord y1 = 0 ; :: thesis:
then ex u being Nat st n = 0 * u by A56, NAT_D:def 3;
hence contradiction ; :: thesis:

end;

then 0 + 1 <= ord y1 by NAT_1:13;
hence contradiction by A51, A54, A55, A57, XXREAL_0:1; :: thesis:

end;

then A58: (t,1) -bag = EmptyBag the carrier of F_Complex by UPROOTS:9;
A59: 1 in Seg (len f) by A5, A48, FINSEQ_1:1;
then 1 in dom f by FINSEQ_1:def 3;
then reconsider fd1 = f . 1 as Element of the carrier of (Polynom-Ring F_Complex) by FINSEQ_2:11;
f1 = <*(f . 1)*> by A5, A48, Th1;
then F . 1 = Product <*fd1*> by A7, A59
.= fd1 by FINSOP_1:11
.= <%(1_ F_Complex)%> by A3, A50, A51 ;
hence F . 1 = poly_with_roots ((t,1) -bag) by A58, UPROOTS:60; :: thesis:

end;

for i being Element of NAT st 1 <= i & i <= len f holds
S₂[i] from INT_1:sch 7(A49, A8);
then ( f = f | (Seg (len f)) & ex S being finite Subset of F_Complex st
( S = H₁( len f) & F . (len f) = poly_with_roots ((S,1) -bag) ) ) by A5, A48, FINSEQ_3:49;
hence Product f = poly_with_roots ((s,1) -bag) by A5, A7, A47, FINSEQ_1:3; :: thesis: