set cPRFC = the carrier of ;
let n be non zero Element of NAT ; :: thesis: ex f being FinSequence of the carrier of ex p being Polynomial of F_Complex st
( p = Product f & dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds
( ( ( not i divides n or i = n ) implies f . i = ) & ( i divides n & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = () *' p )

defpred S1[ set , set ] means ex i being non zero Element of NAT st
( i = \$1 & ( not i divides n implies \$2 = ) & ( i divides n implies \$2 = cyclotomic_poly i ) );
consider m being Nat such that
A1: n = m + 1 by NAT_1:6;
A2: for k being Nat st k in Seg n holds
ex x being Element of the carrier of st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg n implies ex x being Element of the carrier of st S1[k,x] )
assume k in Seg n ; :: thesis: ex x being Element of the carrier of st S1[k,x]
then reconsider i = k as non zero Element of NAT by FINSEQ_1:1;
per cases ( not i divides n or i divides n ) ;
suppose A3: not i divides n ; :: thesis: ex x being Element of the carrier of st S1[k,x]
reconsider FC1 = as Element of the carrier of by POLYNOM3:def 10;
take FC1 ; :: thesis: S1[k,FC1]
take i ; :: thesis: ( i = k & ( not i divides n implies FC1 = ) & ( i divides n implies FC1 = cyclotomic_poly i ) )
thus i = k ; :: thesis: ( ( not i divides n implies FC1 = ) & ( i divides n implies FC1 = cyclotomic_poly i ) )
thus ( ( not i divides n implies FC1 = ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A3; :: thesis: verum
end;
suppose A4: i divides n ; :: thesis: ex x being Element of the carrier of st S1[k,x]
reconsider FC1 = cyclotomic_poly i as Element of the carrier of by POLYNOM3:def 10;
take FC1 ; :: thesis: S1[k,FC1]
take i ; :: thesis: ( i = k & ( not i divides n implies FC1 = ) & ( i divides n implies FC1 = cyclotomic_poly i ) )
thus i = k ; :: thesis: ( ( not i divides n implies FC1 = ) & ( i divides n implies FC1 = cyclotomic_poly i ) )
thus ( ( not i divides n implies FC1 = ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A4; :: thesis: verum
end;
end;
end;
consider f being FinSequence of the carrier of such that
A5: dom f = Seg n and
A6: for k being Nat st k in Seg n holds
S1[k,f /. k] from reconsider fm = f | (Seg m) as FinSequence of the carrier of by FINSEQ_1:18;
A7: len f = n by ;
A8: now :: thesis: for i being non zero Element of NAT st i in dom f holds
( ( not i divides n implies f . i = ) & ( i divides n implies f . i = cyclotomic_poly i ) )
let i be non zero Element of NAT ; :: thesis: ( i in dom f implies ( ( not i divides n implies f . i = ) & ( i divides n implies f . i = cyclotomic_poly i ) ) )
assume A9: i in dom f ; :: thesis: ( ( not i divides n implies f . i = ) & ( i divides n implies f . i = cyclotomic_poly i ) )
then A10: i <= n by ;
( ex j being non zero Element of NAT st
( j = i & ( not j divides n implies f /. i = ) & ( j divides n implies f /. i = cyclotomic_poly j ) ) & 1 <= i ) by ;
hence ( ( not i divides n implies f . i = ) & ( i divides n implies f . i = cyclotomic_poly i ) ) by ; :: thesis: verum
end;
reconsider FC1 = as Element of the carrier of by POLYNOM3:def 10;
<*FC1*> is FinSequence of the carrier of ;
then reconsider h = fm ^ as FinSequence of the carrier of by FINSEQ_1:75;
reconsider p = Product h as Polynomial of F_Complex by POLYNOM3:def 10;
take h ; :: thesis: ex p being Polynomial of F_Complex st
( p = Product h & dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds
( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = () *' p )

take p ; :: thesis: ( p = Product h & dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds
( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = () *' p )

thus p = Product h ; :: thesis: ( dom h = Seg n & ( for i being non zero Element of NAT st i in Seg n holds
( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = () *' p )

A11: m <= n by ;
then A12: len fm = m by ;
reconsider cpn = cyclotomic_poly n as Element of the carrier of by POLYNOM3:def 10;
reconsider fn = f | (Seg n) as FinSequence of the carrier of by FINSEQ_1:18;
1 <= n by NAT_1:53;
then A13: n in Seg n by FINSEQ_1:1;
then A14: f . n = cyclotomic_poly n by A5, A8;
len = 1 by FINSEQ_1:40;
hence dom h = Seg n by ; :: thesis: ( ( for i being non zero Element of NAT st i in Seg n holds
( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = () *' p )

A15: dom fm = Seg m by ;
thus for i being non zero Element of NAT st i in Seg n holds
( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) :: thesis:
proof
let i be non zero Element of NAT ; :: thesis: ( i in Seg n implies ( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) )
assume A16: i in Seg n ; :: thesis: ( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) )
per cases ( i in Seg m or not i in Seg m ) ;
suppose A17: i in Seg m ; :: thesis: ( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) )
then A18: ( fm . i = f . i & i <= m ) by ;
h . i = fm . i by ;
hence ( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) by A5, A1, A8, A16, A18, NAT_1:13; :: thesis: verum
end;
suppose not i in Seg m ; :: thesis: ( ( ( not i divides n or i = n ) implies h . i = ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) )
then ( not 1 <= i or not i <= m ) by FINSEQ_1:1;
then A19: n <= i by ;
A20: i <= n by ;
1 in Seg 1 by FINSEQ_1:1;
then 1 in dom by FINSEQ_1:38;
then h . n = . 1 by
.= by FINSEQ_1:40 ;
hence ( ( not i divides n or i = n ) implies h . i = ) by ; :: thesis: ( i divides n & i <> n implies h . i = cyclotomic_poly i )
thus ( i divides n & i <> n implies h . i = cyclotomic_poly i ) by ; :: thesis: verum
end;
end;
end;
reconsider p1 = as Element of the carrier of by POLYNOM3:def 10;
reconsider Pfm = Product fm as Polynomial of F_Complex by POLYNOM3:def 10;
A21: Product h = (Product fm) * p1 by GROUP_4:6
.= Pfm *' by POLYNOM3:def 10
.= Product fm by UPROOTS:32 ;
f = fn by
.= fm ^ by ;
then A22: Product f = (Product fm) * cpn by GROUP_4:6;
unital_poly (F_Complex,n) = Product f by A7, A8, Th49;
hence unital_poly (F_Complex,n) = () *' p by ; :: thesis: verum