let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st x0 in dom f & f is_continuous_in x0 holds
( f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 )
let x0 be Real; :: thesis: ( x0 in dom f & f is_continuous_in x0 implies ( f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 ) )
assume that
A1: x0 in dom f and
A2: f is_continuous_in x0 ; :: thesis: ( f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 )
for s being Real_Sequence st rng s c= (left_open_halfline x0) /\ (dom f) & s is convergent & lim s = x0 holds
( f /* s is convergent & f . x0 = lim (f /* s) )

proof

let s be Real_Sequence; :: thesis: ( rng s c= (left_open_halfline x0) /\ (dom f) & s is convergent & lim s = x0 implies ( f /* s is convergent & f . x0 = lim (f /* s) ) )
assume that
A3: rng s c= (left_open_halfline x0) /\ (dom f) and
A4: s is convergent and
A5: lim s = x0 ; :: thesis: ( f /* s is convergent & f . x0 = lim (f /* s) )
rng s c= dom f by A3, XBOOLE_1:18;
hence ( f /* s is convergent & f . x0 = lim (f /* s) ) by A2, A4, A5, FCONT_1:def 1; :: thesis: verum

end;

hence f is_Lcontinuous_in x0 by A1, FDIFF_3:def 1; :: thesis: f is_Rcontinuous_in x0
for s being Real_Sequence st rng s c= (right_open_halfline x0) /\ (dom f) & s is convergent & lim s = x0 holds
( f /* s is convergent & f . x0 = lim (f /* s) )

proof

let s be Real_Sequence; :: thesis: ( rng s c= (right_open_halfline x0) /\ (dom f) & s is convergent & lim s = x0 implies ( f /* s is convergent & f . x0 = lim (f /* s) ) )
assume that
A6: rng s c= (right_open_halfline x0) /\ (dom f) and
A7: s is convergent and
A8: lim s = x0 ; :: thesis: ( f /* s is convergent & f . x0 = lim (f /* s) )
rng s c= dom f by A6, XBOOLE_1:18;
hence ( f /* s is convergent & f . x0 = lim (f /* s) ) by A2, A7, A8, FCONT_1:def 1; :: thesis: verum

end;

hence f is_Rcontinuous_in x0 by A1, FDIFF_3:def 2; :: thesis: verum