theorem Th25: :: FDIFF_2:25

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