let f be PartFunc of REAL,REAL; :: thesis: ( f is total & ( for r1, r2 being Real holds |.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) implies ( f is_differentiable_on [#] REAL & f | ([#] REAL) is constant ) )
assume that
A1: f is total and
A2: for r1, r2 being Real holds |.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ; :: thesis: ( f is_differentiable_on [#] REAL & f | ([#] REAL) is constant )
A3: dom f = [#] REAL by A1, PARTFUN1:def 2;

A4: now :: thesis: for r1, r2 being Element of REAL st r1 in ([#] REAL) /\ (dom f) & r2 in ([#] REAL) /\ (dom f) holds
f . r1 = f . r2

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

end;

for r1, r2 being Real st r1 in [#] REAL & r2 in [#] REAL holds
|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 by A2;
hence ( f is_differentiable_on [#] REAL & f | ([#] REAL) is constant ) by A3, A4, Th24, PARTFUN2:58; :: thesis: verum