set cPRFC = the carrier of (Polynom-Ring F_Complex);
let n be non zero Element of NAT ; :: thesis:
defpred S₁[ set , set ] means ex i being non zero Element of NAT st
( i = $1 & ( not i divides n implies $2 = <%(1_ F_Complex)%> ) & ( 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 (Polynom-Ring F_Complex) st S₁[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg n ; :: thesis:
then reconsider i = k as non zero Element of NAT by FINSEQ_1:1;

per cases ;

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

reconsider FC1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;
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 A3; :: thesis:

end;

suppose A4: i divides n ; :: thesis:

reconsider FC1 = cyclotomic_poly i as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;
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;

end;

end;

consider f being FinSequence of the carrier of (Polynom-Ring F_Complex) such that
A5: dom f = Seg n and
A6: for k being Nat st k in Seg n holds
S₁[k,f /. k] from RECDEF_1:sch 17(A2);
reconsider fm = f | (Seg m) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
A7: len f = n by A5, FINSEQ_1:def 3;

A8: now :: thesis:

let i be non zero Element of NAT ; :: thesis:
assume A9: i in dom f ; :: thesis:
then A10: i <= n by A5, FINSEQ_1:1;
( ex j being non zero Element of NAT st
( j = i & ( not j divides n implies f /. i = <%(1_ F_Complex)%> ) & ( j divides n implies f /. i = cyclotomic_poly j ) ) & 1 <= i ) by A5, A6, A9, FINSEQ_1:1;
hence ( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) by A7, A10, FINSEQ_4:15; :: thesis:

end;

reconsider FC1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;
<*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:75;
reconsider p = Product h as Polynomial of F_Complex by POLYNOM3:def 10;
take h ; :: thesis:
take p ; :: thesis:
thus p = Product h ; :: thesis:
A11: m <= n by A1, NAT_1:13;
then A12: len fm = m by A7, FINSEQ_1:17;
reconsider cpn = cyclotomic_poly n as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;
reconsider fn = f | (Seg n) as FinSequence of the carrier of (Polynom-Ring F_Complex) 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_ F_Complex)%>*> = 1 by FINSEQ_1:40;
hence dom h = Seg n by A1, A12, FINSEQ_1:def 7; :: thesis:
A15: dom fm = Seg m by A7, A11, FINSEQ_1:17;
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 = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly i ) ) :: thesis:

proof

let i be non zero Element of NAT ; :: thesis:
assume A16: i in Seg n ; :: thesis:

per cases ;

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

then A18: ( fm . i = f . i & i <= m ) by FINSEQ_1:1, FUNCT_1:49;
h . i = fm . i by A15, A17, 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 A5, A1, A8, A16, A18, NAT_1:13; :: thesis:

end;

suppose not i in Seg m ; :: thesis:

then ( not 1 <= i or not i <= m ) by FINSEQ_1:1;
then A19: n <= i by A1, A16, FINSEQ_1:1, NAT_1:13;
A20: i <= n by A16, FINSEQ_1:1;
1 in Seg 1 by FINSEQ_1:1;
then 1 in dom <*<%(1_ F_Complex)%>*> by FINSEQ_1:38;
then h . n = <*<%(1_ F_Complex)%>*> . 1 by A1, A12, FINSEQ_1:def 7
.= <%(1_ F_Complex)%> ;
hence ( ( not i divides n or i = n ) implies h . i = <%(1_ F_Complex)%> ) by A19, A20, XXREAL_0:1; :: thesis:
thus ( i divides n & i <> n implies h . i = cyclotomic_poly i ) by A19, A20, XXREAL_0:1; :: thesis:

end;

end;

end;

reconsider p1 = <%(1_ F_Complex)%> as Element of the carrier of (Polynom-Ring F_Complex) 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 *' <%(1_ F_Complex)%> by POLYNOM3:def 10
.= Product fm by UPROOTS:32 ;
f = fn by A7, FINSEQ_2:20
.= fm ^ <*(cyclotomic_poly n)*> by A5, A1, A13, A14, FINSEQ_5:10 ;
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) = (cyclotomic_poly n) *' p by A21, A22, POLYNOM3:def 10; :: thesis: