theorem Th38: :: FDIFF_2:38

for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds diff (f,x0) < 0 ) holds
( f | ([#] REAL) is decreasing & f is one-to-one )