theorem Th34: :: FDIFF_2:34

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