:: deftheorem defines number_e POWER:def 4 :
for b₁ being Real holds
( b₁ = number_e iff for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b₁ = lim s );