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

now

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

end;

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