let n, i be Nat; :: thesis: [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] = [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * (i mod n)) / n))**]
[**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] = [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * i) / n))**] by Th9
.= [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * (i mod n)) / n))**] by Th9 ;
hence [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] = [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * (i mod n)) / n))**] ; :: thesis: verum