theorem Th42: :: FDIFF_2:42

for p being Real
for f being PartFunc of REAL,REAL st left_open_halfline p c= dom f & f is_differentiable_on left_open_halfline p & ( for x0 being Real st x0 in left_open_halfline p holds
0 < diff (f,x0) or for x0 being Real st x0 in left_open_halfline p holds
diff (f,x0) < 0 ) holds
rng (f | (left_open_halfline p)) is open