let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_convergent_in x0 & lim (f,x0) = f . x0 holds
f is_continuous_in x0
let x0 be Real; :: thesis: ( f is_convergent_in x0 & lim (f,x0) = f . x0 implies f is_continuous_in x0 )
assume that
A1: f is_convergent_in x0 and
A2: lim (f,x0) = f . 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 ) )
then consider d being Real such that
A4: ( 0 < d & ( for x being Real st 0 < |.(x0 - x).| & |.(x0 - x).| < d & x in dom f holds
|.((f . x) - (f . x0)).| < e ) ) by A1, A2, LIMFUNC3:28;
take d ; :: 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; :: 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
A5: x in dom f and
A6: |.(x - x0).| < d ; :: thesis: |.((f . x) - (f . x0)).| < e
A7: |.(- (x - x0)).| = |.(x - x0).| by COMPLEX1:52;

per cases ( x = x0 or x <> x0 ) ;

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

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

end;

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

then x0 - x <> 0 ;
hence |.((f . x) - (f . x0)).| < e by A4, A5, A6, A7, COMPLEX1:47; :: thesis: verum

end;

end;

end;

end;

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