let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL holds
( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
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
|.((f . r1) - g).| < g1 ) ) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
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
|.((f . r1) - g).| < g1 ) ) ) )
thus ( f is_left_convergent_in x0 implies ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
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
|.((f . r1) - g).| < g1 ) ) ) ) :: thesis: ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
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
|.((f . r1) - g).| < g1 ) ) implies f is_left_convergent_in x0 )

proof

assume that
A1: f is_left_convergent_in x0 and
A2: ( ex r being Real st
( r < x0 & ( for g being Real holds
( not r < g or not g < x0 or not g in dom f ) ) ) or for g being Real 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 & |.((f . r1) - g).| >= g1 ) ) ) ) ; :: thesis: contradiction
consider g being Real such that
A3: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = g ) by A1;
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 & |.((f . r1) - g).| >= g1 ) by A1, A2;
defpred S₁[ Nat, Real] means ( x0 - (1 / ($1 + 1)) < $2 & $2 < x0 & $2 in dom f & |.((f . $2) - g).| >= g1 );

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

let n be Element of NAT ; :: thesis: ex g2 being Element of 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: |.((f . g2) - g).| >= g1 by A5;
reconsider g2 = g2 as Element of REAL by XREAL_0:def 1;
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: 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 A11; :: thesis: verum

end;

A13: rng s c= (dom f) /\ (left_open_halfline x0) by A12, Th5;
A14: lim s = x0 by A12, Th5;
A15: s is convergent by A12, Th5;
then A16: lim (f /* s) = g by A3, A14, A13;
f /* s is convergent by A3, A15, A14, A13;
then consider n being Nat such that
A17: for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1 by A4, A16, SEQ_2:def 7;
A18: |.(((f /* s) . n) - g).| < g1 by A17;
A19: n in NAT by ORDINAL1:def 12;
rng s c= dom f by A12, Th5;
then |.((f . (s . n)) - g).| < g1 by A18, FUNCT_2:108, A19;
hence contradiction by A12; :: thesis: verum

end;

assume A20: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ; :: thesis: ( for g being Real ex g1 being Real st
( 0 < g1 & ( for r being Real holds
( not r < x0 or ex r1 being Real st
( r < r1 & r1 < x0 & r1 in dom f & not |.((f . r1) - g).| < g1 ) ) ) ) or f is_left_convergent_in x0 )
given g being Real such that A21: 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
|.((f . r1) - g).| < g1 ) ) ; :: thesis: f is_left_convergent_in x0

now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_open_halfline x0) holds
( f /* s is convergent & lim (f /* s) = g )

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
A22: s is convergent and
A23: lim s = x0 and
A24: rng s c= (dom f) /\ (left_open_halfline x0) ; :: thesis: ( f /* s is convergent & lim (f /* s) = g )
A25: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;

A26: now :: thesis: for g1 being Real st 0 < g1 holds
ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1

let g1 be Real; :: thesis: ( 0 < g1 implies ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1 )
assume A27: 0 < g1 ; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1
consider r being Real such that
A28: r < x0 and
A29: for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < g1 by A21, A27;
consider n being Nat such that
A30: for k being Nat st n <= k holds
r < s . k by A22, A23, A28, Th1;
take n = n; :: thesis: for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1
let k be Nat; :: thesis: ( n <= k implies |.(((f /* s) . k) - g).| < g1 )
assume A31: n <= k ; :: thesis: |.(((f /* s) . k) - g).| < g1
A32: s . k in rng s by VALUED_0:28;
then s . k in left_open_halfline x0 by A24, XBOOLE_0:def 4;
then s . k in { g2 where g2 is Real : g2 < x0 } by XXREAL_1:229;
then A33: ex g2 being Real st
( g2 = s . k & g2 < x0 ) ;
A34: k in NAT by ORDINAL1:def 12;
s . k in dom f by A24, A32, XBOOLE_0:def 4;
then |.((f . (s . k)) - g).| < g1 by A29, A30, A31, A33;
hence |.(((f /* s) . k) - g).| < g1 by A24, A25, FUNCT_2:108, XBOOLE_1:1, A34; :: thesis: verum

end;

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

end;

hence f is_left_convergent_in x0 by A20; :: thesis: verum