for t being Real
for n being Nat
for e being Element of F_Real st 1 <= n & e = 2 * (cos t) holds
ex p being INT -valued monic Polynomial of F_Real st
( eval (p,e) = 2 * (cos (n * t)) & deg p = n & ( n = 1 implies p = <%(0. F_Real),(1. F_Real)%> ) & ( n = 2 implies ex r being Element of F_Real st
( r = - 2 & p = <%r,(0. F_Real),(1. F_Real)%> ) ) )