let r be Real; 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 V8() )
let f be PartFunc of REAL,REAL; ( 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 V8() ) )
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
; ( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is V8() )
now 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 . r2let r1,
r2 be
Element of
REAL ;
( 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)
;
f . r1 = f . r2set 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
V8()
by A6, Th25;
hence
f . r1 = f . r2
by A12, A9, PARTFUN2:58;
verum end;
hence
( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is V8() )
by A1, A2, Th24, PARTFUN2:58; verum