theorem Th37: :: FDIFF_2:37

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