deffunc H₁( Element of NAT ) -> Real = (1 + (1 / ($1 + 1))) to_power ($1 + 1);
consider s1 being Real_Sequence such that
A1: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();
take lim s1 ; :: 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
lim s1 = lim s
let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) implies lim s1 = lim s )
assume A2: for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ; :: thesis: lim s1 = lim s

A3: now

let n be Element of NAT ; :: thesis: s1 . n = s . n
thus s1 . n = (1 + (1 / (n + 1))) to_power (n + 1) by A1
.= s . n by A2 ; :: thesis: verum

end;

thus lim s1 = lim s by A3, FUNCT_2:113; :: thesis: verum