let S, T be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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

proof

let n be Element of NAT ; :: thesis: c . n = x0
c . n in rng c by NFCONT_1:6;
hence c . n = x0 by A3, TARSKI:def 1; :: thesis: verum

end;

ex n being Element of NAT st rng (((h ^\ n) * z) + c) c= N

proof

A9: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((h * z) . m) - (0. S)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.(((h * z) . m) - (0. S)).|| < p )
assume A10: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((h * z) . m) - (0. S)).|| < p
ex pp being Real st
( pp > 0 & pp * ||.z.|| < p )

proof

take pp = p / (||.z.|| + 1); :: thesis: ( pp > 0 & pp * ||.z.|| < p )
A11: ( ||.z.|| + 0 < ||.z.|| + 1 & 0 <= ||.z.|| ) by NORMSP_1:4, XREAL_1:8;
A12: ||.z.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.z.|| + 1) by A10, XREAL_1:139;
then pp * ||.z.|| < pp * (||.z.|| + 1) by A11, XREAL_1:97;
hence ( pp > 0 & pp * ||.z.|| < p ) by A10, A12, XCMPLX_1:87; :: thesis: verum

end;

then consider pp being Real such that
A13: pp > 0 and
A14: pp * ||.z.|| < p ;
( h is convergent & lim h = 0 ) ;
then consider n being Nat such that
A15: for m being Nat st n <= m holds
|.((h . m) - 0).| < pp by A13, SEQ_2:def 7;
take n = n; :: thesis: for m being Nat st n <= m holds
||.(((h * z) . m) - (0. S)).|| < p
let m be Nat; :: thesis: ( n <= m implies ||.(((h * z) . m) - (0. S)).|| < p )
assume n <= m ; :: thesis: ||.(((h * z) . m) - (0. S)).|| < p
then A16: |.((h . m) - 0).| < pp by A15;
A17: ||.(((h * z) . m) - (0. S)).|| = ||.(((h . m) * z) - (0. S)).|| by NDIFF_1:def 3
.= ||.((h . m) * z).|| by RLVECT_1:13
.= |.(h . m).| * ||.z.|| by NORMSP_1:def 1 ;
0 <= ||.z.|| by NORMSP_1:4;
then |.(h . m).| * ||.z.|| <= pp * ||.z.|| by A16, XREAL_1:64;
hence ||.(((h * z) . m) - (0. S)).|| < p by A14, A17, XXREAL_0:2; :: thesis: verum

end;

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 ; :: thesis: rng (((h ^\ n) * z) + c) c= N
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (((h ^\ n) * z) + c) or y in N )
assume y in rng (((h ^\ n) * z) + c) ; :: thesis: 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; :: thesis: verum

end;

then consider n being Element of NAT such that
A26: rng (((h ^\ n) * z) + c) c= N ;

A27: now :: thesis: for m being Element of NAT holds (((h * z) + c) ^\ n) . m = (((h ^\ n) * z) + c) . m

let m be Element of NAT ; :: thesis: (((h * z) + c) ^\ n) . m = (((h ^\ n) * z) + c) . m
thus (((h * z) + c) ^\ n) . m = ((h * z) + c) . (n + m) by NAT_1:def 3
.= ((h * z) . (n + m)) + (c . (n + m)) by NORMSP_1:def 2
.= ((h * z) . (n + m)) + x0 by A8
.= ((h * z) . (n + m)) + (c . m) by A8
.= ((h . (n + m)) * z) + (c . m) by NDIFF_1:def 3
.= (((h ^\ n) . m) * z) + (c . m) by NAT_1:def 3
.= (((h ^\ n) * z) . m) + (c . m) by NDIFF_1:def 3
.= (((h ^\ n) * z) + c) . m by NORMSP_1:def 2 ; :: thesis: verum

end;

now :: thesis: for m being Element of NAT holds (((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n) . m = (((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) . m

let m be Element of NAT ; :: thesis: (((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n) . m = (((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) . m
A28: ((f /* ((h * z) + c)) ^\ n) . m = (f /* ((h * z) + c)) . (n + m) by NAT_1:def 3
.= f /. (((h * z) + c) . (n + m)) by A4, FUNCT_2:109
.= f /. ((((h * z) + c) ^\ n) . m) by NAT_1:def 3
.= f /. ((((h ^\ n) * z) + c) . m) by A27 ;
thus (((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n) . m = ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . (n + m) by NAT_1:def 3
.= ((h ") . (n + m)) * (((f /* ((h * z) + c)) - (f /* c)) . (n + m)) by NDIFF_1:def 2
.= ((h . (n + m)) ") * (((f /* ((h * z) + c)) - (f /* c)) . (n + m)) by VALUED_1:10
.= (((h ^\ n) . m) ") * (((f /* ((h * z) + c)) - (f /* c)) . (n + m)) by NAT_1:def 3
.= (((h ^\ n) . m) ") * (((f /* ((h * z) + c)) . (n + m)) - ((f /* c) . (n + m))) by NORMSP_1:def 3
.= (((h ^\ n) . m) ") * ((((f /* ((h * z) + c)) ^\ n) . m) - ((f /* c) . (n + m))) by NAT_1:def 3
.= (((h ^\ n) . m) ") * ((f /. ((((h ^\ n) * z) + c) . m)) - (f /. (c . (n + m)))) by A5, A28, FUNCT_2:109
.= (((h ^\ n) . m) ") * ((f /. ((((h ^\ n) * z) + c) . m)) - (f /. x0)) by A8
.= (((h ^\ n) . m) ") * ((f /. ((((h ^\ n) * z) + c) . m)) - (f /. (c . m))) by A8
.= (((h ^\ n) . m) ") * ((f /. ((((h ^\ n) * z) + c) . m)) - ((f /* c) . m)) by A5, FUNCT_2:109
.= (((h ^\ n) . m) ") * (((f /* (((h ^\ n) * z) + c)) . m) - ((f /* c) . m)) by A1, A26, FUNCT_2:109, XBOOLE_1:1
.= (((h ^\ n) . m) ") * (((f /* (((h ^\ n) * z) + c)) - (f /* c)) . m) by NORMSP_1:def 3
.= (((h ^\ n) ") . m) * (((f /* (((h ^\ n) * z) + c)) - (f /* c)) . m) by VALUED_1:10
.= (((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) . m by NDIFF_1:def 2 ; :: thesis: verum

end;

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