let n be non empty Element of NAT ; :: thesis:
set cPRFC = the carrier of (Polynom-Ring F_Complex );
A1: 1 <= n by UPROOTS:1;
defpred S₁[ set , set ] means ex i being non empty Element of NAT st
( i = $1 & ( not i divides n implies $2 = <%(1_ F_Complex )%> ) & ( i divides n implies $2 = cyclotomic_poly i ) );
A2: for k being Element of NAT st k in Seg n holds
ex x being Element of the carrier of (Polynom-Ring F_Complex ) st S₁[k,x]

proof

let k be Element of NAT ; :: thesis:
assume A3: k in Seg n ; :: thesis:
reconsider i = k as non empty Element of NAT by A3, FINSEQ_1:3;

per cases ;

suppose A4: not i divides n ; :: thesis:

reconsider FC1 = <%(1_ F_Complex )%> as Element of the carrier of (Polynom-Ring F_Complex ) by POLYNOM3:def 12;
take FC1 ; :: thesis:
take i ; :: thesis:
thus i = k ; :: thesis:
thus ( ( not i divides n implies FC1 = <%(1_ F_Complex )%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A4; :: thesis:

end;

suppose A5: i divides n ; :: thesis:

reconsider FC1 = cyclotomic_poly i as Element of the carrier of (Polynom-Ring F_Complex ) by POLYNOM3:def 12;
take FC1 ; :: thesis:
take i ; :: thesis:
thus i = k ; :: thesis:
thus ( ( not i divides n implies FC1 = <%(1_ F_Complex )%> ) & ( i divides n implies FC1 = cyclotomic_poly i ) ) by A5; :: thesis:

end;

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex ) such that
A6: dom f = Seg n and
A7: for k being Element of NAT st k in Seg n holds
S₁[k,f /. k] from POLYNOM2:sch 1(A2);
consider m being Nat such that
A8: n = m + 1 by NAT_1:6;
A10: len f = n by A6, FINSEQ_1:def 3;

A11: now

let i be non empty Element of NAT ; :: thesis:
assume A12: i in dom f ; :: thesis:
then consider j being non empty Element of NAT such that
A13: j = i and
A14: ( ( not j divides n implies f /. i = <%(1_ F_Complex )%> ) & ( j divides n implies f /. i = cyclotomic_poly j ) ) by A6, A7;
( 1 <= i & i <= n ) by A6, A12, FINSEQ_1:3;
hence ( ( not i divides n implies f . i = <%(1_ F_Complex )%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) by A10, A13, A14, FINSEQ_4:24; :: thesis:

end;

then A15: unital_poly F_Complex ,n = Product f by A10, Th53;
reconsider fm = f | (Seg m) as FinSequence of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_1:23;
reconsider Pfm = Product fm as Polynomial of F_Complex by POLYNOM3:def 12;
A16: m <= n by A8, NAT_1:13;
then A17: dom fm = Seg m by A10, FINSEQ_1:21;
A18: len fm = m by A10, A16, FINSEQ_1:21;
A19: n in Seg n by A1, FINSEQ_1:3;
then A20: f . n = cyclotomic_poly n by A6, A11;
reconsider fn = f | (Seg n) as FinSequence of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_1:23;
A21: f = fn by A10, FINSEQ_2:23
.= fm ^ <*(cyclotomic_poly n)*> by A6, A8, A19, A20, FINSEQ_5:11 ;
reconsider FC1 = <%(1_ F_Complex )%> as Element of the carrier of (Polynom-Ring F_Complex ) by POLYNOM3:def 12;
<*FC1*> is FinSequence of the carrier of (Polynom-Ring F_Complex ) ;
then reconsider h = fm ^ <*<%(1_ F_Complex )%>*> as FinSequence of the carrier of (Polynom-Ring F_Complex ) by FINSEQ_1:96;
reconsider p = Product h as Polynomial of F_Complex by POLYNOM3:def 12;
take h ; :: thesis:
take p ; :: thesis:
thus p = Product h ; :: thesis:
len <*<%(1_ F_Complex )%>*> = 1 by FINSEQ_1:57;
hence dom h = Seg n by A8, A18, FINSEQ_1:def 7; :: thesis:
thus for i being non empty Element of NAT st i in Seg n holds
( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex )%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) :: thesis:

proof

let i be non empty Element of NAT ; :: thesis:
assume A22: i in Seg n ; :: thesis:

per cases ;

suppose A23: i in Seg m ; :: thesis:

then A24: fm . i = f . i by FUNCT_1:72;
A25: i <= m by A23, FINSEQ_1:3;
h . i = fm . i by A17, A23, FINSEQ_1:def 7;
hence ( ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex )%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) by A6, A8, A11, A22, A24, A25, NAT_1:13; :: thesis:

end;

suppose not i in Seg m ; :: thesis:

then ( ( not 1 <= i or not i <= m ) & 1 <= i & i <= n ) by A22, FINSEQ_1:3;
then A26: ( n <= i & i <= n ) by A8, NAT_1:13;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*<%(1_ F_Complex )%>*> by FINSEQ_1:55;
then h . n = <*<%(1_ F_Complex )%>*> . 1 by A8, A18, FINSEQ_1:def 7
.= <%(1_ F_Complex )%> by FINSEQ_1:57 ;
hence ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex )%> ) by A26, XXREAL_0:1; :: thesis:
thus ( i divides n & i <> n implies h . i = cyclotomic_poly i ) by A26, XXREAL_0:1; :: thesis:

end;

reconsider p1 = <%(1_ F_Complex )%> as Element of the carrier of (Polynom-Ring F_Complex ) by POLYNOM3:def 12;
A27: Product h = (Product fm) * p1 by GROUP_4:9
.= Pfm *' <%(1_ F_Complex )%> by POLYNOM3:def 12
.= Product fm by UPROOTS:34 ;
reconsider cpn = cyclotomic_poly n as Element of the carrier of (Polynom-Ring F_Complex ) by POLYNOM3:def 12;
Product f = (Product fm) * cpn by A21, GROUP_4:9;
hence unital_poly F_Complex ,n = (cyclotomic_poly n) *' p by A15, A27, POLYNOM3:def 12; :: thesis: