let n, i, j be Element of NAT ; :: thesis: [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] * [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] = [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**]
(((2 * PI) * i) / n) + (((2 * PI) * j) / n) = (((2 * PI) * i) + ((2 * PI) * j)) / n by XCMPLX_1:62
.= ((2 * PI) * (i + j)) / n ;
then ( ((cos (((2 * PI) * i) / n)) * (cos (((2 * PI) * j) / n))) - ((sin (((2 * PI) * i) / n)) * (sin (((2 * PI) * j) / n))) = cos (((2 * PI) * (i + j)) / n) & ((cos (((2 * PI) * i) / n)) * (sin (((2 * PI) * j) / n))) + ((cos (((2 * PI) * j) / n)) * (sin (((2 * PI) * i) / n))) = sin (((2 * PI) * (i + j)) / n) ) by SIN_COS:75;
then [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] * [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] = [**(cos (((2 * PI) * (i + j)) / n)),(sin (((2 * PI) * (i + j)) / n))**]
.= [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**] by Th10 ;
hence [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] * [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] = [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**] ; :: thesis: verum