defpred S₁[ Nat, Real] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f );
let g1, g2 be Real; :: thesis: ( ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = g1 ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = g2 ) ) implies g1 = g2 )
assume that
A2: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = g1 ) and
A3: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = g2 ) ; :: thesis: g1 = g2

A4: now :: thesis: for n being Element of NAT ex g being Element of REAL st S₁[n,g]

let n be Element of NAT ; :: thesis: ex g being Element of REAL st S₁[n,g]
x0 < x0 + (1 / (n + 1)) by Lm3;
then consider g being Real such that
A5: g < x0 + (1 / (n + 1)) and
A6: x0 < g and
A7: g in dom f by A1;
reconsider g = g as Element of REAL by XREAL_0:def 1;
take g = g; :: thesis: S₁[n,g]
thus S₁[n,g] by A5, A6, A7; :: thesis: verum

end;

consider s being Real_Sequence such that
A8: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A4);
A9: for n being Nat holds S₁[n,s . n]

proof

let n be Nat; :: thesis: S₁[n,s . n]
n in NAT by ORDINAL1:def 12;
hence S₁[n,s . n] by A8; :: thesis: verum

end;

A10: rng s c= (dom f) /\ (right_open_halfline x0) by A9, Th6;
A11: lim s = x0 by A9, Th6;
A12: s is convergent by A9, Th6;
then lim (f /* s) = g1 by A11, A10, A2;
hence g1 = g2 by A12, A11, A10, A3; :: thesis: verum