let g, p be Real; :: thesis: 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 V8() )
let f be PartFunc of REAL,REAL; :: thesis: ( ( 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 implies ( f is_differentiable_on ].p,g.[ & f | ].p,g.[ is V8() ) )
assume that
A1: for r1, r2 being Real st r1 in ].p,g.[ & r2 in ].p,g.[ holds
|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 and
A2: ].p,g.[ c= dom f ; :: thesis: ( f is_differentiable_on ].p,g.[ & f | ].p,g.[ is V8() )
thus A3: f is_differentiable_on ].p,g.[ by A1, A2, Th24; :: thesis: f | ].p,g.[ is V8()
for x0 being Real st x0 in ].p,g.[ holds
diff (f,x0) = 0 by A1, A2, Th24;
hence f | ].p,g.[ is V8() by A3, ROLLE:7; :: thesis: verum