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