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