theorem Th9: :: INTEGR26:9

for a, b, x being Real
for f being PartFunc of REAL,REAL st a < x & x <= b & ].a,b.[ c= dom f & f is_left_convergent_in x holds
( f | ].a,b.[ is_left_convergent_in x & lim_left ((f | ].a,b.[),x) = lim_left (f,x) )