let n, ni be non empty Element of NAT ; :: thesis: ( ni divides n implies ni -roots_of_1 c= n -roots_of_1 )
assume A1: ni divides n ; :: thesis: ni -roots_of_1 c= n -roots_of_1
consider k being Nat such that
A2: n = ni * k by A1, NAT_D:def 3;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
for x being set st x in ni -roots_of_1 holds
x in n -roots_of_1

proof

let x be set ; :: thesis: ( x in ni -roots_of_1 implies x in n -roots_of_1 )
assume A3: x in ni -roots_of_1 ; :: thesis: x in n -roots_of_1
reconsider y = x as Element of F_Complex by A3;
y is CRoot of ni, 1_ F_Complex by A3, Th24;
then 1_ F_Complex = (power F_Complex ) . y,ni by COMPLFLD:def 2;
then 1_ F_Complex = (power F_Complex ) . ((power F_Complex ) . y,ni),k by Th10;
then 1_ F_Complex = (power F_Complex ) . y,n by A2, Th14;
then y is CRoot of n, 1_ F_Complex by COMPLFLD:def 2;
hence x in n -roots_of_1 ; :: thesis: verum

end;

hence ni -roots_of_1 c= n -roots_of_1 by TARSKI:def 3; :: thesis: verum