let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 holds
f is_continuous_in x0
let x0 be Real; :: thesis: ( f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 implies f is_continuous_in x0 )
assume that
A1: f is_Lcontinuous_in x0 and
A2: f is_Rcontinuous_in x0 ; :: thesis: f is_continuous_in x0
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom f & |.(x - x0).| < d holds
|.((f . x) - (f . x0)).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex d being Real st
( 0 < d & ( for x being Real st x in dom f & |.(x - x0).| < d holds
|.((f . x) - (f . x0)).| < e ) ) )
assume A3: 0 < e ; :: thesis: ex d being Real st
( 0 < d & ( for x being Real st x in dom f & |.(x - x0).| < d holds
|.((f . x) - (f . x0)).| < e ) )
consider d1 being Real such that
A4: ( 0 < d1 & ( for x being Real st x in dom f & x0 - d1 < x & x < x0 holds
|.((f . x) - (f . x0)).| < e ) ) by A3, A1, Th27;
consider d2 being Real such that
A5: ( 0 < d2 & ( for x being Real st x in dom f & x0 < x & x < x0 + d2 holds
|.((f . x) - (f . x0)).| < e ) ) by A3, A2, Th28;
take d = min (d1,d2); :: thesis: ( 0 < d & ( for x being Real st x in dom f & |.(x - x0).| < d holds
|.((f . x) - (f . x0)).| < e ) )
thus 0 < d by A4, A5, XXREAL_0:21; :: thesis: for x being Real st x in dom f & |.(x - x0).| < d holds
|.((f . x) - (f . x0)).| < e
thus for x being Real st x in dom f & |.(x - x0).| < d holds
|.((f . x) - (f . x0)).| < e :: thesis: verum

proof

let x be Real; :: thesis: ( x in dom f & |.(x - x0).| < d implies |.((f . x) - (f . x0)).| < e )
assume that
A6: x in dom f and
A7: |.(x - x0).| < d ; :: thesis: |.((f . x) - (f . x0)).| < e
A8: - d < - |.(x - x0).| by A7, XREAL_1:24;
( - |.(x - x0).| <= x - x0 & x - x0 <= |.(x - x0).| ) by ABSVALUE:4;
then A9: ( - d < x - x0 & x - x0 < d ) by A7, A8, XXREAL_0:2;

per cases ( x = x0 or x < x0 or x0 < x ) by XXREAL_0:1;

suppose x = x0 ; :: thesis: |.((f . x) - (f . x0)).| < e

hence |.((f . x) - (f . x0)).| < e by A3, COMPLEX1:44; :: thesis: verum

end;

suppose A10: x < x0 ; :: thesis: |.((f . x) - (f . x0)).| < e

A11: x0 - d < x by A9, XREAL_1:20;
x0 - d1 <= x0 - d by XXREAL_0:17, XREAL_1:10;
then x0 - d1 < x by A11, XXREAL_0:2;
hence |.((f . x) - (f . x0)).| < e by A4, A6, A10; :: thesis: verum

end;

suppose A12: x0 < x ; :: thesis: |.((f . x) - (f . x0)).| < e

A13: x < x0 + d by A9, XREAL_1:19;
x0 + d <= x0 + d2 by XXREAL_0:17, XREAL_1:6;
then x < x0 + d2 by A13, XXREAL_0:2;
hence |.((f . x) - (f . x0)).| < e by A5, A6, A12; :: thesis: verum

end;

end;

end;

end;

hence f is_continuous_in x0 by FCONT_1:3; :: thesis: verum