defpred S₁[ Element of NAT , Real] means ( x0 - (1 / ($1 + 1)) < $2 & $2 < x0 & $2 in dom f );

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

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

end;

consider s being Real_Sequence such that
A7: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A2);
A8: rng s c= (dom f) \ {x0} by A7, Th6;
A9: lim s = x0 by A7, Th6;
let g1, g2 be Real; :: thesis: ( ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {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) \ {x0} holds
( f /* seq is convergent & lim (f /* seq) = g2 ) ) implies g1 = g2 )
assume that
A10: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
( f /* seq is convergent & lim (f /* seq) = g1 ) and
A11: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
( f /* seq is convergent & lim (f /* seq) = g2 ) ; :: thesis: g1 = g2
A12: s is convergent by A7, Th6;
then lim (f /* s) = g1 by A9, A8, A10;
hence g1 = g2 by A12, A9, A8, A11; :: thesis: verum