:: deftheorem Def3 defines Coef LOPBAN_4:def 3 :
for n being Nat
for b₂ being Real_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 ) ) );