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

then A2:
dseq ^\ 1 is convergent
by POWER:59;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;thus (dseq ^\ 1) . n = dseq . (n + 1) by NAT_1:def 3

.= (1 + (1 / (n + 1))) ^ (n + 1) by Def4 ; :: thesis: verum

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