let r be Real; :: thesis: for f being PartFunc of REAL ,REAL st left_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in left_open_halfline r & r2 in left_open_halfline r holds
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) holds
( f is_differentiable_on left_open_halfline r & f | (left_open_halfline r) is constant )
let f be PartFunc of REAL ,REAL ; :: thesis: ( left_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in left_open_halfline r & r2 in left_open_halfline r holds
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) implies ( f is_differentiable_on left_open_halfline r & f | (left_open_halfline r) is constant ) )
assume A1: ( left_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in left_open_halfline r & r2 in left_open_halfline r holds
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) ) ; :: thesis: ( f is_differentiable_on left_open_halfline r & f | (left_open_halfline r) is constant )

now

let r1, r2 be Real; :: thesis: ( r1 in (left_open_halfline r) /\ (dom f) & r2 in (left_open_halfline r) /\ (dom f) implies f . r1 = f . r2 )
assume ( r1 in (left_open_halfline r) /\ (dom f) & r2 in (left_open_halfline r) /\ (dom f) ) ; :: thesis: f . r1 = f . r2
then A2: ( r1 in left_open_halfline r & r1 in dom f & r2 in left_open_halfline r & r2 in dom f ) by XBOOLE_0:def 4;
set rr = min r1,r2;
A3: ].((min r1,r2) - 1),r.[ c= left_open_halfline r by XXREAL_1:263;
then A4: ].((min r1,r2) - 1),r.[ c= dom f by A1, XBOOLE_1:1;
r1 in { g where g is Real : g < r } by A2, XXREAL_1:229;
then A5: ex g1 being Real st
( g1 = r1 & g1 < r ) ;
r2 in { p where p is Real : p < r } by A2, XXREAL_1:229;
then A6: ex g2 being Real st
( g2 = r2 & g2 < r ) ;
A7: ( min r1,r2 <= r1 & min r1,r2 <= r2 ) by XXREAL_0:17;
then A8: (min r1,r2) - 1 < r1 - 0 by XREAL_1:17;
then r1 in { g1 where g1 is Real : ( (min r1,r2) - 1 < g1 & g1 < r ) } by A5;
then A9: r1 in ].((min r1,r2) - 1),r.[ by RCOMP_1:def 2;
A10: (min r1,r2) - 1 < r by A5, A8, XXREAL_0:2;
for g1, g2 being Real st g1 in ].((min r1,r2) - 1),r.[ & g2 in ].((min r1,r2) - 1),r.[ holds
abs ((f . g1) - (f . g2)) <= (g1 - g2) ^2 by A1, A3;
then A11: f | ].((min r1,r2) - 1),r.[ is constant by A4, A10, Th25;
(min r1,r2) - 1 < r2 - 0 by A7, XREAL_1:17;
then r2 in { g2 where g2 is Real : ( (min r1,r2) - 1 < g2 & g2 < r ) } by A6;
then A12: r2 in ].((min r1,r2) - 1),r.[ by RCOMP_1:def 2;
A13: r1 in ].((min r1,r2) - 1),r.[ /\ (dom f) by A2, A9, XBOOLE_0:def 4;
r2 in ].((min r1,r2) - 1),r.[ /\ (dom f) by A2, A12, XBOOLE_0:def 4;
hence f . r1 = f . r2 by A11, A13, PARTFUN2:77; :: thesis: verum

end;

hence ( f is_differentiable_on left_open_halfline r & f | (left_open_halfline r) is constant ) by A1, Th24, PARTFUN2:77; :: thesis: verum