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

proof

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

A6: now

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

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) /\ (left_open_halfline x0) by A11, Th5;
A13: lim s = x0 by A11, Th5;
A14: s is convergent by A11, Th5;
then A15: lim (f /* s) = g by A1, A2, A13, A12, Def7;
f /* s is convergent by A1, A2, A14, A13, A12, Def7;
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, Th5;
then abs ((f . (s . n)) - g) < g1 by A17, FUNCT_2:185;
hence contradiction by A11; :: thesis: verum

end;

assume A18: for g1 being Real st 0 < g1 holds
ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ; :: thesis: lim_left (f,x0) = g

now

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_open_halfline x0) implies ( f /* s is convergent & lim (f /* s) = g ) )
assume that
A19: s is convergent and
A20: lim s = x0 and
A21: rng s c= (dom f) /\ (left_open_halfline x0) ; :: thesis: ( f /* s is convergent & lim (f /* s) = g )
A22: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;

A23: now

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

end;

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

end;

hence lim_left (f,x0) = g by A1, Def7; :: thesis: verum