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