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

now :: thesis: for n being Element of NAT holds s1 . n = s . n

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;

hence lim s1 = lim s by FUNCT_2:63; :: thesis: verum