now :: thesis: for k being Element of NAT holds eseq . k = (1 rExpSeq) . k

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

end;

then A1: eseq = 1 rExpSeq by FUNCT_2:63;
hence eseq is summable by SIN_COS:45; :: thesis: Sum eseq = exp_R 1
thus exp_R 1 = exp_R . 1 by SIN_COS:def 23
.= Sum eseq by A1, SIN_COS:def 22 ; :: thesis: verum