let a, b be Real; :: thesis: ( ( for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
a = lim s ) & ( 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 ) implies a = b )
assume that
A3: for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
a = lim s and
A4: 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 ; :: thesis: a = b
deffunc H₁( Nat) -> Real = (1 + (1 / ($1 + 1))) to_power ($1 + 1);
consider s1 being Real_Sequence such that
A5: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();
A6: for n being Nat holds s1 . n = H₁(n) by A5;
lim s1 = a by A3, A6;
hence a = b by A4, A6; :: thesis: verum