for f being PartFunc of REAL,REAL st f is total & ( for r1, r2 being Real holds |.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) holds
( f is_differentiable_on [#] REAL & f | ([#] REAL) is V8() )