theorem Th24: :: FDIFF_2:24

for A being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f & ( for r, p being Real st r in A & p in A holds
|.((f . r) - (f . p)).| <= (r - p) ^2 ) holds
( f is_differentiable_on A & ( for x0 being Real st x0 in A holds
diff (f,x0) = 0 ) )