theorem Th8: :: INTEGR26:8

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_right_convergent_in x holds
( f | ].a,b.[ is_right_convergent_in x & lim_right ((f | ].a,b.[),x) = lim_right (f,x) )