:: deftheorem Def21 defines P_cos SIN_COS:def 21 :
for th being Real
for b₂ being Real_Sequence holds
( b₂ = th P_cos iff for n being Nat holds b₂ . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) );