:: deftheorem defines number_e IRRAT_1:def 6 :
number_e = Sum eseq;