:: deftheorem Def2 defines bseq IRRAT_1:def 2 :
for k being Nat
for b₂ being Real_Sequence holds
( b₂ = bseq k iff for n being Nat holds b₂ . n = (n choose k) * (n ^ (- k)) );