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
defpred S₁[ Element of NAT , real number ] means ( $1 < $2 & $2 in dom f );
A4: for n being Element of NAT ex r being Real st S₁[n,r] by A1, Def6;
consider s2 being Real_Sequence such that
A6: for n being Element of NAT holds S₁[n,s2 . n] from FUNCT_2:sch 3(A4);

now

let n be Element of NAT ; :: thesis: (incl NAT ) . n <= s2 . n
n < s2 . n by A6;
hence (incl NAT ) . n <= s2 . n by FUNCT_1:35; :: thesis: verum

end;

then A8: s2 is divergent_to+infty by Lm7, Th47, Th69;
A9: rng s2 c= dom f

proof

let x be real number ; :: according to MEMBERED:def 9 :: thesis: ( not x in rng s2 or x in dom f )
assume x in rng s2 ; :: thesis: x in dom f
then ex n being Element of NAT st x = s2 . n by FUNCT_2:190;
hence x in dom f by A6; :: thesis: verum

end;

then lim (f /* s2) = g1 by A2, A8;
hence g1 = g2 by A3, A8, A9; :: thesis: verum