let n, i, j be Element of NAT ; [**(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))**]
; verum