:: deftheorem Def5 defines eseq IRRAT_1:def 5 :
for b₁ being Real_Sequence holds
( b₁ = eseq iff for k being Nat holds b₁ . k = 1 / (k !) );