:: deftheorem Def6 defines Coef SIN_COS:def 6 :
for n being Nat
for b₂ being Complex_Sequence holds
( b₂ = Coef n iff for k being Nat holds
( ( k <= n implies b₂ . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b₂ . k = 0 ) ) );