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 A1: ( 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 ) ) ; :: thesis: ( f is_differentiable_on A & ( for x0 being Real st x0 in A holds
diff f,x0 = 0 ) )

A2: 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
A3: N c= A by RCOMP_1:39;
A4: N c= dom f by A1, A3, 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

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 A5: ( rng c = {x0} & rng (h + c) c= dom f ) ; :: thesis: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = 0 )
then A6: ( h + c is convergent & lim (h + c) = x0 ) by Th4;
consider r being real number such that
A7: ( 0 < r & N = ].(x0 - r),(x0 + r).[ ) by RCOMP_1:def 7;
consider n being Element of NAT such that
A8: for m being Element of NAT st n <= m holds
abs (((h + c) . m) - x0) < r by A6, A7, SEQ_2:def 7;
set h1 = h ^\ n;
set c1 = c ^\ n;
set hc = (h + c) ^\ n;
A9: 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
A10: x = ((h + c) ^\ n) . m by FUNCT_2:190;
x = (h + c) . (m + n) by A10, NAT_1:def 3;
then abs ((((h + c) ^\ n) . m) - x0) < r by A8, A10, NAT_1:12;
then x in N by A7, A10, RCOMP_1:8;
hence x in A by A3; :: thesis: verum

end;

A11: rng (c ^\ n) c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (c ^\ n) or x in A )
assume A12: x in rng (c ^\ n) ; :: thesis: x in A
rng (c ^\ n) c= rng c by VALUED_0:21;
then A13: x = x0 by A5, A12, TARSKI:def 1;
x0 in N by RCOMP_1:37;
hence x in A by A3, A13; :: thesis: verum

end;

reconsider a = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
A15: lim a = a . 0 by SEQ_4:41
.= 0 by FUNCOP_1:13 ;
A16: ( h ^\ n is non-zero & h ^\ n is convergent & lim (h ^\ n) = 0 ) by FDIFF_1:def 1;
then A17: abs (h ^\ n) is convergent by SEQ_4:26;
A18: lim (abs (h ^\ n)) = abs 0 by A16, SEQ_4:27
.= 0 by ABSVALUE:7 ;
A19: abs (h ^\ n) is non-zero by A16, SEQ_1:61;
set fn = ((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n;
A20: 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 A21: x = x0 by A5, TARSKI:def 1;
x0 in N by RCOMP_1:37;
hence x in dom f by A4, A21; :: thesis: verum

end;

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 )
0 <= abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n) . m) by COMPLEX1:132;
then a . m <= abs ((((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n) . m) by FUNCOP_1:13;
hence a . m <= (abs (((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m by SEQ_1:16; :: thesis: (abs (((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= (abs (h ^\ n)) . m
A23: ((h + c) ^\ n) . m in rng ((h + c) ^\ n) by VALUED_0:28;
(c ^\ n) . m in rng (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 A1, A9, A11, A23;
then A24: abs ((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))) <= (abs ((((h + c) ^\ n) . m) - ((c ^\ n) . m))) ^2 by COMPLEX1:161;
A25: rng (c ^\ n) c= dom f by A1, A11, XBOOLE_1:1;
rng ((h + c) ^\ n) c= dom f by A1, A9, XBOOLE_1:1;
then A26: abs ((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))) = abs (((f /* ((h + c) ^\ n)) . m) - (f . ((c ^\ n) . m))) by FUNCT_2:185
.= abs (((f /* ((h + c) ^\ n)) . m) - ((f /* (c ^\ n)) . m)) by A25, FUNCT_2:185
.= abs (((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . m) by RFUNCT_2:6
.= (abs ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n)))) . m by SEQ_1:16
.= (abs (((f /* (h + c)) ^\ n) - (f /* (c ^\ n)))) . m by A5, VALUED_0:27
.= (abs (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n))) . m by A20, VALUED_0:27
.= (abs (((f /* (h + c)) - (f /* c)) ^\ n)) . m by SEQM_3:39 ;
A27: (abs ((((h + c) ^\ n) . m) - ((c ^\ n) . m))) ^2 = (abs ((((h ^\ n) + (c ^\ n)) . m) - ((c ^\ n) . m))) ^2 by SEQM_3:37
.= (abs ((((h ^\ n) . m) + ((c ^\ n) . m)) - ((c ^\ n) . m))) ^2 by SEQ_1:11
.= ((abs (h ^\ n)) . m) ^2 by SEQ_1:16
.= ((abs (h ^\ n)) . m) * ((abs (h ^\ n)) . m) ;
A28: (abs (h ^\ n)) . m <> 0 by A19, SEQ_1:7;
0 <= abs ((h ^\ n) . m) by COMPLEX1:132;
then 0 <= (abs (h ^\ n)) . m by SEQ_1:16;
then A29: 0 <= ((abs (h ^\ n)) . m) " ;
A30: (((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 (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:12
.= ((abs ((h ^\ n) " )) (#) (abs (((f /* (h + c)) - (f /* c)) ^\ n))) . m by SEQ_1:62
.= (abs (((h ^\ n) " ) (#) (((f /* (h + c)) - (f /* c)) ^\ n))) . m by SEQ_1:60
.= (abs (((h " ) ^\ n) (#) (((f /* (h + c)) - (f /* c)) ^\ n))) . m by SEQM_3:41
.= (abs (((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m by SEQM_3:42 ;
hence (abs (((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= (abs (h ^\ n)) . m by A24, A26, A27, A29, A30, XREAL_1:66; :: thesis: verum

end;

then A31: abs (((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n) is convergent by A15, A17, A18, SEQ_2:33;
lim (abs (((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n)) = 0 by A15, A17, A18, A22, SEQ_2:34;
then A32: ( ((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n is convergent & lim (((h " ) (#) ((f /* (h + c)) - (f /* c))) ^\ n) = 0 ) by A31, SEQ_4:28;
hence (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_4:35; :: thesis: lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = 0
thus lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = 0 by A32, SEQ_4:36; :: thesis: verum

end;

hence ( f is_differentiable_in x0 & diff f,x0 = 0 ) by A4, 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:16; :: 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 A2; :: thesis: verum