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:63
.= ((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:80;
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 Th12 ;
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