let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st x0 in dom f & f is_left_convergent_in x0 & lim_left (f,x0) = f . x0 holds
f is_Lcontinuous_in x0
let f be PartFunc of REAL,REAL; :: thesis: ( x0 in dom f & f is_left_convergent_in x0 & lim_left (f,x0) = f . x0 implies f is_Lcontinuous_in x0 )
assume that
A1: x0 in dom f and
A2: f is_left_convergent_in x0 and
A3: lim_left (f,x0) = f . x0 ; :: thesis: f is_Lcontinuous_in x0
for seq being Real_Sequence st rng seq c= (left_open_halfline x0) /\ (dom f) & seq is convergent & lim seq = x0 holds
( f /* seq is convergent & f . x0 = lim (f /* seq) ) by A2, A3, L_HOSPIT:3;
hence f is_Lcontinuous_in x0 by A1, FDIFF_3:def 1; :: thesis: verum