deffunc H₁( Nat) -> object = - $1;
defpred S₁[ Nat, Real] means ( $2 < - $1 & $2 in dom f );
let g1, g2 be Real; :: thesis: ( ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g1 ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g2 ) ) implies g1 = g2 )
assume that
A2: for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g1 ) and
A3: for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g2 ) ; :: thesis: g1 = g2
consider s2 being Real_Sequence such that
A4: for n being Nat holds s2 . n = H₁(n) from SEQ_1:sch 1();
A5: for n being Element of NAT ex r being Element of REAL st S₁[n,r]

proof

let n be Element of NAT ; :: thesis: ex r being Element of REAL st S₁[n,r]
consider r being Real such that
A6: S₁[n,r] by A1;
reconsider r = r as Real ;
S₁[n,r] by A6;
hence ex r being Element of REAL st S₁[n,r] ; :: thesis: verum

end;

consider s1 being Real_Sequence such that
A7: for n being Element of NAT holds S₁[n,s1 . n] from FUNCT_2:sch 3(A5);
A8: rng s1 c= dom f

proof

let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in rng s1 or x in dom f )
assume x in rng s1 ; :: thesis: x in dom f
then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence x in dom f by A7; :: thesis: verum

end;

now :: thesis: for n being Nat holds s1 . n <= s2 . n

let n be Nat; :: thesis: s1 . n <= s2 . n
n in NAT by ORDINAL1:def 12;
then s1 . n < - n by A7;
hence s1 . n <= s2 . n by A4; :: thesis: verum

end;

then A9: s1 is divergent_to-infty by A4, Th21, Th43;
then lim (f /* s1) = g1 by A2, A8;
hence g1 = g2 by A3, A9, A8; :: thesis: verum