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
|.((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
|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) implies ( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is constant ) )
assume that
A1: right_open_halfline r c= dom f and
A2: for r1, r2 being Real st r1 in right_open_halfline r & r2 in right_open_halfline r holds
|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ; :: thesis: ( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is constant )

now :: thesis: for r1, r2 being Element of REAL st r1 in (right_open_halfline r) /\ (dom f) & r2 in (right_open_halfline r) /\ (dom f) holds
f . r1 = f . r2

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

end;

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