let n be non empty Element of NAT ; :: thesis: for x, y being Element of COMPLEX st x in n -roots_of_1 & y in n -roots_of_1 holds
x * y in n -roots_of_1
let x, y be Element of COMPLEX ; :: thesis: ( x in n -roots_of_1 & y in n -roots_of_1 implies x * y in n -roots_of_1 )
assume that
A1: x in n -roots_of_1 and
A2: y in n -roots_of_1 ; :: thesis: x * y in n -roots_of_1
reconsider a = x as Element of F_Complex by COMPLFLD:def 1;
consider i being Element of NAT such that
A3: a = [**(cos (((2 * PI ) * i) / n)),(sin (((2 * PI ) * i) / n))**] by A1, Th27;
reconsider b = y as Element of F_Complex by COMPLFLD:def 1;
consider j being Element of NAT such that
A4: b = [**(cos (((2 * PI ) * j) / n)),(sin (((2 * PI ) * j) / n))**] by A2, Th27;
a * b = [**(cos (((2 * PI ) * ((i + j) mod n)) / n)),(sin (((2 * PI ) * ((i + j) mod n)) / n))**] by A3, A4, Th13;
hence x * y in n -roots_of_1 by Th27; :: thesis: verum