let n, ni be non zero Element of NAT ; :: thesis:
let q be Integer; :: thesis:
assume A1: ( ni < n & ni divides n ) ; :: thesis:
set ttt = (unital_poly (F_Complex,ni)) *' (cyclotomic_poly n);
consider f being FinSequence of the carrier of (Polynom-Ring F_Complex), p being Polynomial of F_Complex such that
A2: p = Product f and
A3: ( dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n 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 ) ) ) ) and
A4: unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p by A1, Th54;

A5: now :: thesis:

let i be non zero Element of NAT ; :: thesis:
assume A6: i in dom f ; :: thesis:

per cases ;

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

hence ( f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) by A3, A6; :: thesis:

end;

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

hence ( f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) by A3, A6; :: thesis:

end;

end;

end;

let qc be Element of F_Complex; :: thesis:
assume qc = q ; :: thesis:
then eval (p,qc) is integer by A2, A5, Th55;
then consider m being Integer such that
A7: m = eval (p,qc) ;
let j, k, l be Integer; :: thesis:
assume A8: ( j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) ) ; :: thesis:
reconsider jc = j, lc = l, mc = m as Element of COMPLEX by XCMPLX_0:def 2;
reconsider jcf = jc, lcf = lc, mcf = mc as Element of F_Complex by COMPLFLD:def 1;
eval ((unital_poly (F_Complex,n)),qc) = (eval (((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)),qc)) * (eval (p,qc)) by A4, POLYNOM4:24;
then A9: k = (lcf * jcf) * mcf by A8, A7, POLYNOM4:24
.= (l * j) * m ;

now :: thesis:

per cases ;

suppose A10: l <> 0 ; :: thesis:

k = l * (j * m) by A9;
then l divides k by INT_1:def 3;
then k / l is integer by A10, WSIERP_1:17;
then [\(k / l)/] = k / l by INT_1:25;
then k div l = ((j * m) * l) / l by A9, INT_1:def 9;
then k div l = j * m by A10, XCMPLX_1:89;
hence j divides k div l by INT_1:def 3; :: thesis:

end;

suppose l = 0 ; :: thesis:

then k div l = 0 by INT_1:48;
hence j divides k div l by INT_2:12; :: thesis:

end;

end;

end;

hence j divides k div l ; :: thesis: