:: deftheorem Def7 defines Coef_e SIN_COS:def 7 :
for n being Nat
for b₂ being Complex_Sequence holds
( b₂ = Coef_e n iff for k being Nat holds
( ( k <= n implies b₂ . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies b₂ . k = 0 ) ) );