A1: 1_. F_Complex = (1_ F_Complex) * (1_. F_Complex) by POLYNOM5:27
.= <%(1_ F_Complex)%> by POLYNOM5:29 ;
let i be Integer; :: thesis:
let c be Element of F_Complex; :: thesis:
let f be FinSequence of the carrier of (Polynom-Ring F_Complex); :: thesis:
let p be Polynomial of F_Complex; :: thesis:
assume that
A2: p = Product f and
A3: c = i and
A4: for i being non zero Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ; :: thesis:
A5: eval ((1_. F_Complex),c) = 1 by COMPLFLD:8, POLYNOM4:18;

suppose len f = 0 ; :: thesis:

then f = <*> the carrier of (Polynom-Ring F_Complex) ;
then p = 1_ (Polynom-Ring F_Complex) by A2, GROUP_4:8
.= 1. (Polynom-Ring F_Complex) ;
hence eval (p,c) is integer by A5, POLYNOM3:def 10; :: thesis:

end;

suppose A6: 0 < len f ; :: thesis:

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;
A7: f = f | (Seg (len f)) by FINSEQ_3:49;

A8: 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
A9: for i being Nat st i in Seg (len f) holds
S₁[i,F . i] from FINSEQ_1:sch 5(A8);
defpred S₂[ Nat] means ex r being Polynomial of F_Complex st
( r = F . $1 & eval (r,c) is integer );

A10: now :: thesis:

let i be Element of NAT ; :: thesis:
assume that
A11: 1 <= i and
A12: i < len f ; :: thesis:
A13: i in Seg (len f) by A11, A12, FINSEQ_1:1;
reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
A14: i + 1 <= len f by A12, NAT_1:13;
then i + 1 = min ((i + 1),(len f)) by XXREAL_0:def 9;
then A15: len fi1 = i + 1 by FINSEQ_2:21;
1 <= i + 1 by A11, NAT_1:13;
then A16: i + 1 in Seg (len f) by A14, FINSEQ_1:1;
then A17: i + 1 in dom f by FINSEQ_1:def 3;
reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
assume A18: S₂[i] ; :: thesis:
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 A17, FINSEQ_2:11;
reconsider pfi1 = Product fi1, pfi = Product fi as Polynomial of F_Complex by POLYNOM3:def 10;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
fi = fi1 | (Seg i) by Lm2, NAT_1:12;
then fi1 = fi ^ <*fi1d1*> by A15, FINSEQ_3:55;
then A20: Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;
thus S₂[i + 1] :: thesis:

reconsider epfi = eval (pfi,c), efi1d1p = eval (fi1d1p,c) as Element of COMPLEX by COMPLFLD:def 1;

reconsider i1 = i + 1 as non zero Element of NAT by ORDINAL1:def 12;

per cases by A4, A17;

suppose f . i1 = <%(1_ F_Complex)%> ; :: thesis:

hence eval (fi1d1p,c) is integer by A5, A1, FINSEQ_1:4, FUNCT_1:49; :: thesis:

end;

suppose f . i1 = cyclotomic_poly i1 ; :: thesis:

hence eval (fi1d1p,c) is integer by A3, A19, Th52; :: thesis:

end;

end;

end;

then reconsider iefi1d1p = efi1d1p as Integer ;
reconsider iepfi = epfi as Integer by A9, A18, A13;
take pfi1 ; :: thesis:
thus pfi1 = F . (i + 1) by A9, A16; :: thesis:
pfi1 = pfi *' fi1d1p by A20, POLYNOM3:def 10;
then eval (pfi1,c) = (eval (pfi,c)) * (eval (fi1d1p,c)) by POLYNOM4:24
.= iepfi * iefi1d1p ;
hence eval (pfi1,c) is integer ; :: thesis:

end;

end;

A21: 0 + 1 <= len f by A6, NAT_1:13;
then A22: 1 in Seg (len f) by FINSEQ_1:1;
A23: S₂[1]

reconsider f1 = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;
A24: 1 in dom f by A22, FINSEQ_1:def 3;
then reconsider fd1 = f . 1 as Element of the carrier of (Polynom-Ring F_Complex) by FINSEQ_2:11;
reconsider fd1 = fd1 as Polynomial of F_Complex by POLYNOM3:def 10;
take fd1 ; :: thesis:
f1 = <*(f . 1)*> by A21, Th1;
hence fd1 = Product f1 by FINSOP_1:11
.= F . 1 by A9, A22 ;
:: thesis:

per cases by A4, A24;

suppose f . 1 = <%(1_ F_Complex)%> ; :: thesis:

hence eval (fd1,c) is integer by A1, COMPLFLD:8, POLYNOM4:18; :: thesis:

end;

suppose f . 1 = cyclotomic_poly 1 ; :: thesis:

hence eval (fd1,c) is integer by A3, Th52; :: thesis:

end;

end;

end;

for i being Element of NAT st 1 <= i & i <= len f holds
S₂[i] from INT_1:sch 7(A23, A10);
then ex r being Polynomial of F_Complex st
( r = F . (len f) & eval (r,c) is integer ) by A21;
hence eval (p,c) is integer by A2, A6, A9, A7, FINSEQ_1:3; :: thesis:

end;

end;