let S, T be RealNormSpace; for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
let f be PartFunc of S,T; for x0 being Point of S st f is_differentiable_in x0 holds
for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
let x0 be Point of S; ( f is_differentiable_in x0 implies for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) )
assume
f is_differentiable_in x0
; for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
then consider N being Neighbourhood of x0 such that
A1:
N c= dom f
and
A2:
for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
by Th1;
let z be Point of S; for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
let h be non-zero 0 -convergent Real_Sequence; for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
let c be constant sequence of S; ( rng c = {x0} & rng ((h * z) + c) c= dom f implies ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) )
assume that
A3:
rng c = {x0}
and
A4:
rng ((h * z) + c) c= dom f
; ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
x0 in N
by NFCONT_1:4;
then A5:
rng c c= dom f
by A3, A1, ZFMISC_1:31;
consider g being Real such that
A6:
0 < g
and
A7:
{ y where y is Point of S : ||.(y - x0).|| < g } c= N
by NFCONT_1:def 1;
A8:
for n being Element of NAT holds c . n = x0
ex n being Element of NAT st rng (((h ^\ n) * z) + c) c= N
proof
then A18:
h * z is
convergent
by NORMSP_1:def 6;
c . 0 in rng c
by NFCONT_1:6;
then
c . 0 = x0
by A3, TARSKI:def 1;
then A19:
lim c = x0
by NDIFF_1:18;
A20:
c is
convergent
by NDIFF_1:18;
then A21:
(h * z) + c is
convergent
by A18, NORMSP_1:19;
lim (h * z) = 0. S
by A9, A18, NORMSP_1:def 7;
then lim ((h * z) + c) =
(0. S) + x0
by A20, A19, A18, NORMSP_1:25
.=
x0
by RLVECT_1:4
;
then consider n being
Nat such that A22:
for
m being
Nat st
n <= m holds
||.((((h * z) + c) . m) - x0).|| < g
by A6, A21, NORMSP_1:def 7;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
take
n
;
rng (((h ^\ n) * z) + c) c= N
let y be
object ;
TARSKI:def 3 ( not y in rng (((h ^\ n) * z) + c) or y in N )
assume
y in rng (((h ^\ n) * z) + c)
;
y in N
then consider m being
Nat such that A23:
y = (((h ^\ n) * z) + c) . m
by NFCONT_1:6;
A24:
n + m in NAT
by ORDINAL1:def 12;
A25:
m in NAT
by ORDINAL1:def 12;
reconsider y1 =
y as
Point of
S by A23;
||.((((h * z) + c) . (n + m)) - x0).|| < g
by A22, NAT_1:11;
then
||.((((h * z) . (n + m)) + (c . (n + m))) - x0).|| < g
by NORMSP_1:def 2;
then
||.((((h * z) . (n + m)) + x0) - x0).|| < g
by A8, A24;
then
||.((((h * z) . (n + m)) + (c . m)) - x0).|| < g
by A8, A25;
then
||.((((h . (n + m)) * z) + (c . m)) - x0).|| < g
by NDIFF_1:def 3;
then
||.(((((h ^\ n) . m) * z) + (c . m)) - x0).|| < g
by NAT_1:def 3;
then
||.(((((h ^\ n) * z) . m) + (c . m)) - x0).|| < g
by NDIFF_1:def 3;
then
||.(((((h ^\ n) * z) + c) . m) - x0).|| < g
by NORMSP_1:def 2;
then
y1 in { w where w is Point of S : ||.(w - x0).|| < g }
by A23;
hence
y in N
by A7;
verum
end;
then consider n being Element of NAT such that
A26:
rng (((h ^\ n) * z) + c) c= N
;
then A29:
((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c)) = ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n
by FUNCT_2:63;
( ((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim (((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) )
by A3, A2, A26;
hence
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
by A29, LOPBAN_3:10, LOPBAN_3:11; verum