let f be PartFunc of REAL,REAL; for x0 being Real
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let x0 be Real; for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let N be Neighbourhood of x0; ( f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
assume that
A1:
f is_differentiable_in x0
and
A2:
N c= dom f
; for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
consider N1 being Neighbourhood of x0 such that
N1 c= dom f
and
A3:
ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A1;
consider N2 being Neighbourhood of x0 such that
A4:
N2 c= N
and
A5:
N2 c= N1
by RCOMP_1:17;
A6:
N2 c= dom f
by A2, A4;
let h be non-zero 0 -convergent Real_Sequence; for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let c be V8() Real_Sequence; ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
assume that
A7:
rng c = {x0}
and
A8:
rng (h + c) c= N
; ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
consider g being Real such that
A9:
0 < g
and
A10:
N2 = ].(x0 - g),(x0 + g).[
by RCOMP_1:def 6;
( x0 + 0 < x0 + g & x0 - g < x0 - 0 )
by A9, XREAL_1:8, XREAL_1:15;
then A11:
x0 in N2
by A10;
A12:
rng c c= dom f
ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
then consider n being Element of NAT such that
rng (c ^\ n) c= N2
and
A19:
rng ((h + c) ^\ n) c= N2
;
consider L being LinearFunc, R being RestFunc such that
A20:
for x being Real st x in N1 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A3;
A21:
rng (c ^\ n) c= dom f
A23:
L is total
by Def3;
A24:
( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L . 1 )
A34:
rng ((h + c) ^\ n) c= dom f
by A19, A4, A2;
A35:
rng (h + c) c= dom f
by A8, A2;
A36:
for k being Element of NAT holds (f . (((h + c) ^\ n) . k)) - (f . ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))
A39:
R is total
by Def2;
then
(f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))
by FUNCT_2:63;
then A40: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") =
(((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) ")
by A35, VALUED_0:27
.=
(((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) ")
by A12, VALUED_0:27
.=
(((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) ")
by SEQM_3:17
.=
(((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ") ^\ n)
by SEQM_3:18
.=
(((f /* (h + c)) - (f /* c)) (#) (h ")) ^\ n
by SEQM_3:19
;
then A41:
L . 1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
by A24, SEQ_4:22;
thus
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
by A24, A40, SEQ_4:21; diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
for x being Real st x in N2 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
by A20, A5;
hence
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
by A1, A6, A41, Def5; verum