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