A1: now :: thesis: for n being Nat holds (dseq ^\ 1) . n = (1 + (1 / (n + 1))) ^ (n + 1)

let n be 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:59;
hence dseq is convergent by SEQ_4:21; :: thesis: lim dseq = number_e
for n being Nat holds (dseq ^\ 1) . n = (1 + (1 / (n + 1))) ^ (n + 1) by A1;
then number_e = lim (dseq ^\ 1) by POWER:def 4;
hence lim dseq = number_e by A2, SEQ_4:22; :: thesis: verum