now

let k be Element of NAT ; :: thesis: eseq . k = (1 rExpSeq ) . k
thus eseq . k = 1 / (k ! ) by Def5
.= (1 |^ k) / (k ! ) by NEWTON:15
.= (1 rExpSeq ) . k by SIN_COS:def 9 ; :: thesis: verum

end;

then A1: eseq = 1 rExpSeq by FUNCT_2:113;
hence eseq is summable by SIN_COS:49; :: thesis: Sum eseq = exp_R 1
thus exp_R 1 = exp_R . 1 by SIN_COS:def 27
.= Sum eseq by A1, SIN_COS:def 26 ; :: thesis: verum