let n be non zero Element of NAT ; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( (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; :: thesis: verum

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; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( (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; :: thesis: verum