A1: now

let n be Element of NAT ; :: thesis: (dseq ^\ 1) . n = (1 + (1 / (n + 1))) ^ (n + 1)
thus (dseq ^\ 1) . n = dseq . (n + 1) by NAT_1:def 3
.= (1 + (1 / (n + 1))) ^ (n + 1) by Def4 ; :: thesis: verum

end;

then A2: dseq ^\ 1 is convergent by POWER:67;
hence dseq is convergent by SEQ_4:35; :: thesis: lim dseq = number_e
number_e = lim (dseq ^\ 1) by A1, POWER:def 4;
hence lim dseq = number_e by A2, SEQ_4:36; :: thesis: verum