:: deftheorem Def4 defines Coef_e LOPBAN_4:def 4 :
for n being Nat
for b₂ being Real_Sequence holds
( b₂ = Coef_e n iff for k being Nat holds
( ( k <= n implies b₂ . k = 1 / ((k !) * ((n -' k) !)) ) & ( k > n implies b₂ . k = 0 ) ) );