let A be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st A c= dom f & ( for r, p being Real st r in A & p in A holds
abs ((f . r) - (f . p)) <= (r - p) ^2 ) holds
( f is_differentiable_on A & ( for x0 being Real st x0 in A holds
diff (f,x0) = 0 ) )
let f be PartFunc of REAL,REAL; :: thesis: ( A c= dom f & ( for r, p being Real st r in A & p in A holds
abs ((f . r) - (f . p)) <= (r - p) ^2 ) implies ( f is_differentiable_on A & ( for x0 being Real st x0 in A holds
diff (f,x0) = 0 ) ) )
assume that
A1: A c= dom f and
A2: for r, p being Real st r in A & p in A holds
abs ((f . r) - (f . p)) <= (r - p) ^2 ; :: thesis: ( f is_differentiable_on A & ( for x0 being Real st x0 in A holds
diff (f,x0) = 0 ) )

A3: now

let x0 be Real; :: thesis: ( x0 in A implies ( f is_differentiable_in x0 & diff (f,x0) = 0 ) )
assume x0 in A ; :: thesis: ( f is_differentiable_in x0 & diff (f,x0) = 0 )
then consider N being Neighbourhood of x0 such that
A4: N c= A by RCOMP_1:18;
A5: N c= dom f by A1, A4, XBOOLE_1:1;
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 )

proof

reconsider a = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
let h be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 )
let c be V8() Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 ) )
assume that
A6: rng c = {x0} and
A7: rng (h + c) c= dom f ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 )
A8: lim (h + c) = x0 by A6, Th4;
consider r being real number such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
h + c is convergent by A6, Th4;
then consider n being Element of NAT such that
A11: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - x0) < r by A8, A9, SEQ_2:def 7;
set hc = (h + c) ^\ n;
A12: rng ((h + c) ^\ n) c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((h + c) ^\ n) or x in A )
assume x in rng ((h + c) ^\ n) ; :: thesis: x in A
then consider m being Element of NAT such that
A13: x = ((h + c) ^\ n) . m by FUNCT_2:113;
x = (h + c) . (m + n) by A13, NAT_1:def 3;
then abs ((((h + c) ^\ n) . m) - x0) < r by A11, A13, NAT_1:12;
then x in N by A10, A13, RCOMP_1:1;
hence x in A by A4; :: thesis: verum

end;

A14: rng c c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in dom f )
assume x in rng c ; :: thesis: x in dom f
then A15: x = x0 by A6, TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence x in dom f by A5, A15; :: thesis: verum

end;

set fn = ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n;
set h1 = h ^\ n;
A16: h ^\ n is convergent by FDIFF_1:def 1;
then A17: abs (h ^\ n) is convergent ;
set c1 = c ^\ n;
A18: rng (c ^\ n) c= A

proof

A19: rng (c ^\ n) c= rng c by VALUED_0:21;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (c ^\ n) or x in A )
assume x in rng (c ^\ n) ; :: thesis: x in A
then A20: x = x0 by A6, A19, TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence x in A by A4, A20; :: thesis: verum

end;

h ^\ n is non-empty by FDIFF_1:def 1;
then A21: abs (h ^\ n) is non-empty by SEQ_1:53;
A22: for m being Element of NAT holds
( a . m <= (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m & (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= (abs (h ^\ n)) . m )

proof

let m be Element of NAT ; :: thesis: ( a . m <= (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m & (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= (abs (h ^\ n)) . m )
A23: (c ^\ n) . m in rng (c ^\ n) by VALUED_0:28;
((h + c) ^\ n) . m in rng ((h + c) ^\ n) by VALUED_0:28;
then abs ((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))) <= ((((h + c) ^\ n) . m) - ((c ^\ n) . m)) ^2 by A2, A12, A18, A23;
then A24: abs ((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))) <= (abs ((((h + c) ^\ n) . m) - ((c ^\ n) . m))) ^2 by COMPLEX1:75;
A25: (((abs (h ^\ n)) . m) ") * ((abs (((f /* (h + c)) - (f /* c)) ^\ n)) . m) = (((abs (h ^\ n)) ") . m) * ((abs (((f /* (h + c)) - (f /* c)) ^\ n)) . m) by VALUED_1:10
.= (((abs (h ^\ n)) ") (#) (abs (((f /* (h + c)) - (f /* c)) ^\ n))) . m by SEQ_1:8
.= ((abs ((h ^\ n) ")) (#) (abs (((f /* (h + c)) - (f /* c)) ^\ n))) . m by SEQ_1:54
.= (abs (((h ^\ n) ") (#) (((f /* (h + c)) - (f /* c)) ^\ n))) . m by SEQ_1:52
.= (abs (((h ") ^\ n) (#) (((f /* (h + c)) - (f /* c)) ^\ n))) . m by SEQM_3:18
.= (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m by SEQM_3:19 ;
0 <= abs ((((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n) . m) by COMPLEX1:46;
then a . m <= abs ((((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n) . m) by FUNCOP_1:7;
hence a . m <= (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m by SEQ_1:12; :: thesis: (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= (abs (h ^\ n)) . m
A26: (abs ((((h + c) ^\ n) . m) - ((c ^\ n) . m))) ^2 = (abs ((((h ^\ n) + (c ^\ n)) . m) - ((c ^\ n) . m))) ^2 by SEQM_3:15
.= (abs ((((h ^\ n) . m) + ((c ^\ n) . m)) - ((c ^\ n) . m))) ^2 by SEQ_1:7
.= ((abs (h ^\ n)) . m) ^2 by SEQ_1:12
.= ((abs (h ^\ n)) . m) * ((abs (h ^\ n)) . m) ;
0 <= abs ((h ^\ n) . m) by COMPLEX1:46;
then A27: 0 <= (abs (h ^\ n)) . m by SEQ_1:12;
A28: (abs (h ^\ n)) . m <> 0 by A21, SEQ_1:5;
A29: (((abs (h ^\ n)) . m) * ((abs (h ^\ n)) . m)) * (((abs (h ^\ n)) . m) ") = ((abs (h ^\ n)) . m) * (((abs (h ^\ n)) . m) * (((abs (h ^\ n)) . m) "))
.= ((abs (h ^\ n)) . m) * 1 by A28, XCMPLX_0:def 7
.= (abs (h ^\ n)) . m ;
abs ((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))) = abs (((f /* ((h + c) ^\ n)) . m) - (f . ((c ^\ n) . m))) by A1, A12, FUNCT_2:108, XBOOLE_1:1
.= abs (((f /* ((h + c) ^\ n)) . m) - ((f /* (c ^\ n)) . m)) by A1, A18, FUNCT_2:108, XBOOLE_1:1
.= abs (((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . m) by RFUNCT_2:1
.= (abs ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n)))) . m by SEQ_1:12
.= (abs (((f /* (h + c)) ^\ n) - (f /* (c ^\ n)))) . m by A7, VALUED_0:27
.= (abs (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n))) . m by A14, VALUED_0:27
.= (abs (((f /* (h + c)) - (f /* c)) ^\ n)) . m by SEQM_3:17 ;
hence (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= (abs (h ^\ n)) . m by A24, A26, A27, A29, A25, XREAL_1:64; :: thesis: verum

end;

lim (h ^\ n) = 0 by FDIFF_1:def 1;
then A30: lim (abs (h ^\ n)) = abs 0 by A16, SEQ_4:14
.= 0 by ABSVALUE:2 ;
A31: lim a = a . 0 by SEQ_4:26
.= 0 by FUNCOP_1:7 ;
then A32: lim (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) = 0 by A17, A30, A22, SEQ_2:20;
A33: abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n) is convergent by A31, A17, A30, A22, SEQ_2:19;
then A34: ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n is convergent by A32, SEQ_4:15;
hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_4:21; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0
lim (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n) = 0 by A33, A32, SEQ_4:15;
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 by A34, SEQ_4:22; :: thesis: verum

end;

hence ( f is_differentiable_in x0 & diff (f,x0) = 0 ) by A5, Th12; :: thesis: verum

end;

then for x0 being Real st x0 in A holds
f is_differentiable_in x0 ;
hence f is_differentiable_on A by A1, FDIFF_1:9; :: thesis: for x0 being Real st x0 in A holds
diff (f,x0) = 0
let x0 be Real; :: thesis: ( x0 in A implies diff (f,x0) = 0 )
assume x0 in A ; :: thesis: diff (f,x0) = 0
hence diff (f,x0) = 0 by A3; :: thesis: verum