theorem Th12: :: IRRAT_1:12

for k being Nat holds
( bseq k is convergent & lim (bseq k) = 1 / (k !) & lim (bseq k) = eseq . k )