theorem :: FDIFF_2:32

for r being Real
for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds
diff (f,x0) <= 0 ) holds
f | (left_open_halfline r) is non-increasing