let x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
thus ( f is_right_convergent_in x0 implies ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ) ) :: thesis:

proof

assume that
A1: f is_right_convergent_in x0 and
A2: ( ex r being Real st
( x0 < r & ( for g being Real holds
( not g < r or not x0 < g or not g in dom f ) ) ) or for g being Real ex g1 being Real st
( 0 < g1 & ( for r being Real st x0 < r holds
ex r1 being Real st
( r1 < r & x0 < r1 & r1 in dom f & abs ((f . r1) - g) >= g1 ) ) ) ) ; :: thesis:
consider g being Real such that
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) = g ) by A1, Def4;
consider g1 being Real such that
A4: 0 < g1 and
A5: for r being Real st x0 < r holds
ex r1 being Real st
( r1 < r & x0 < r1 & r1 in dom f & abs ((f . r1) - g) >= g1 ) by A1, A2, Def4;
defpred S₁[ Element of NAT , real number ] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f & g1 <= abs ((f . $2) - g) );

A6: now

let n be Element of NAT ; :: thesis:
x0 < x0 + (1 / (n + 1)) by Lm3;
then consider r1 being Real such that
A7: r1 < x0 + (1 / (n + 1)) and
A8: x0 < r1 and
A9: r1 in dom f and
A10: g1 <= abs ((f . r1) - g) by A5;
take r1 = r1; :: thesis:
thus S₁[n,r1] by A7, A8, A9, A10; :: thesis:

end;

consider s being Real_Sequence such that
A11: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A6);
A12: rng s c= (dom f) /\ (right_open_halfline x0) by A11, Th6;
A13: lim s = x0 by A11, Th6;
A14: s is convergent by A11, Th6;
then A15: lim (f /* s) = g by A3, A13, A12;
f /* s is convergent by A3, A14, A13, A12;
then consider n being Element of NAT such that
A16: for k being Element of NAT st n <= k holds
abs (((f /* s) . k) - g) < g1 by A4, A15, SEQ_2:def 7;
A17: abs (((f /* s) . n) - g) < g1 by A16;
rng s c= dom f by A11, Th6;
then abs ((f . (s . n)) - g) < g1 by A17, FUNCT_2:185;
hence contradiction by A11; :: thesis:

end;

assume A18: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ; :: thesis:
given g being Real such that A19: for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ; :: thesis:

now

let s be Real_Sequence; :: thesis:
assume that
A20: s is convergent and
A21: lim s = x0 and
A22: rng s c= (dom f) /\ (right_open_halfline x0) ; :: thesis:
A23: (dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;

A24: now

let g1 be real number ; :: thesis:
assume A25: 0 < g1 ; :: thesis:
g1 is Real by XREAL_0:def 1;
then consider r being Real such that
A26: x0 < r and
A27: for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 by A19, A25;
consider n being Element of NAT such that
A28: for k being Element of NAT st n <= k holds
s . k < r by A20, A21, A26, Th2;
take n = n; :: thesis:
let k be Element of NAT ; :: thesis:
assume A29: n <= k ; :: thesis:
A30: s . k in rng s by VALUED_0:28;
then s . k in right_open_halfline x0 by A22, XBOOLE_0:def 4;
then s . k in { g2 where g2 is Real : x0 < g2 } by XXREAL_1:230;
then A31: ex g2 being Real st
( g2 = s . k & x0 < g2 ) ;
s . k in dom f by A22, A30, XBOOLE_0:def 4;
then abs ((f . (s . k)) - g) < g1 by A27, A28, A29, A31;
hence abs (((f /* s) . k) - g) < g1 by A22, A23, FUNCT_2:185, XBOOLE_1:1; :: thesis:

end;

hence f /* s is convergent by SEQ_2:def 6; :: thesis:
hence lim (f /* s) = g by A24, SEQ_2:def 7; :: thesis:

end;

hence f is_right_convergent_in x0 by A18, Def4; :: thesis: