let n be non zero Element of NAT ; for x0 being Real
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n)
for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
let x0 be Real; for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n)
for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
let f be PartFunc of REAL,(REAL n); for g being PartFunc of REAL,(REAL-NS n)
for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
let g be PartFunc of REAL,(REAL-NS n); for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
let N be Neighbourhood of x0; ( f = g & f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) )
assume that
A1:
f = g
and
A2:
f is_differentiable_in x0
and
A3:
N c= dom f
; for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
A4:
g is_differentiable_in x0
by A1, A2;
let h be non-zero 0 -convergent Real_Sequence; for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
let c be constant Real_Sequence; ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) )
assume
( rng c = {x0} & rng (h + c) c= N )
; ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
then
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (g,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
by A4, A1, A3, NDIFF_3:13;
hence
( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) )
by A1, Th3; verum