theorem :: FDIFF_2:27

for r being Real
for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in right_open_halfline r & r2 in right_open_halfline r holds
|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) holds
( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is constant )