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

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;
for h being non-zero 0 -convergent Real_Sequence
for c being constant 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

set a = seq_const 0;
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant 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 constant 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 such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
consider n being Nat such that
A11: for m being Nat st n <= m holds
|.(((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 object ; :: 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 |.((((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 object ; :: 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;
set c1 = c ^\ n;
A16: rng (c ^\ n) c= A

proof

A17: rng (c ^\ n) c= rng c by VALUED_0:21;
let x be object ; :: 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 A18: x = x0 by A6, A17, TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence x in A by A4, A18; :: thesis: verum

end;

A19: abs (h ^\ n) is non-zero by SEQ_1:53;
A20: for m being Nat holds
( (seq_const 0) . m <= (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m & (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= |.(h ^\ n).| . m )

proof

let m be Nat; :: thesis: ( (seq_const 0) . m <= (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m & (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= |.(h ^\ n).| . m )
A21: m in NAT by ORDINAL1:def 12;
A22: (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 |.((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))).| <= ((((h + c) ^\ n) . m) - ((c ^\ n) . m)) ^2 by A2, A12, A16, A22;
then A23: |.((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))).| <= |.((((h + c) ^\ n) . m) - ((c ^\ n) . m)).| ^2 by COMPLEX1:75;
A24: (((abs (h ^\ n)) . m) ") * (|.(((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
.= |.(((h ^\ n) ") (#) (((f /* (h + c)) - (f /* c)) ^\ n)).| . m by SEQ_1:52
.= |.(((h ") ^\ n) (#) (((f /* (h + c)) - (f /* c)) ^\ n)).| . m by SEQM_3:18
.= |.(((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n).| . m by SEQM_3:19 ;
0 <= |.((((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n) . m).| by COMPLEX1:46;
then (seq_const 0) . m <= |.((((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n) . m).| ;
hence (seq_const 0) . m <= (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m by SEQ_1:12; :: thesis: (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= |.(h ^\ n).| . m
A25: |.((((h + c) ^\ n) . m) - ((c ^\ n) . m)).| ^2 = |.((((h ^\ n) + (c ^\ n)) . m) - ((c ^\ n) . m)).| ^2 by SEQM_3:15
.= |.((((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 <= |.((h ^\ n) . m).| by COMPLEX1:46;
then A26: 0 <= (abs (h ^\ n)) . m by SEQ_1:12;
A27: (abs (h ^\ n)) . m <> 0 by A19, SEQ_1:5;
A28: (((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 A27, XCMPLX_0:def 7
.= (abs (h ^\ n)) . m ;
|.((f . (((h + c) ^\ n) . m)) - (f . ((c ^\ n) . m))).| = |.(((f /* ((h + c) ^\ n)) . m) - (f . ((c ^\ n) . m))).| by A1, A12, FUNCT_2:108, XBOOLE_1:1, A21
.= |.(((f /* ((h + c) ^\ n)) . m) - ((f /* (c ^\ n)) . m)).| by A1, A16, FUNCT_2:108, XBOOLE_1:1, A21
.= |.(((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . m).| by RFUNCT_2:1
.= |.((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))).| . m by SEQ_1:12
.= |.(((f /* (h + c)) ^\ n) - (f /* (c ^\ n))).| . m by A7, VALUED_0:27
.= |.(((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)).| . m by A14, VALUED_0:27
.= |.(((f /* (h + c)) - (f /* c)) ^\ n).| . m by SEQM_3:17 ;
hence (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) . m <= |.(h ^\ n).| . m by A23, A25, A26, A28, A24, XREAL_1:64; :: thesis: verum

end;

lim (h ^\ n) = 0 ;
then A29: lim (abs (h ^\ n)) = |.0.| by SEQ_4:14
.= 0 by ABSVALUE:2 ;
A30: lim (seq_const 0) = (seq_const 0) . 0 by SEQ_4:26
.= 0 ;
then A31: lim (abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n)) = 0 by A29, A20, SEQ_2:20;
A32: abs (((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n) is convergent by A30, A29, A20, SEQ_2:19;
then A33: ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ n is convergent by A31, 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 A32, A31, SEQ_4:15;
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 by A33, 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