let T, S be non trivial RealNormSpace; :: thesis:
let f be PartFunc of S,T; :: thesis:
let x0 be Point of S; :: thesis:
assume A1: f is_differentiable_in x0 ; :: thesis:
let z be Point of S; :: thesis:
let h be convergent_to_0 Real_Sequence; :: thesis:
let c be V8() sequence of S; :: thesis:
assume that
A2: rng c = {x0} and
A3: rng ((h * z) + c) c= dom f ; :: thesis:
consider N being Neighbourhood of x0 such that
A4: N c= dom f and
A5: for z being Point of S
for h being convergent_to_0 Real_Sequence
for c being V8() 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 A1, Th1;
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 3;
A8: for n being Element of NAT holds c . n = x0

proof

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

end;

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

proof

A9: c is convergent by NDIFF_1:21;
c . 0 in rng c by NFCONT_1:6;
then c . 0 = x0 by A2, TARSKI:def 1;
then A10: lim c = x0 by NDIFF_1:21;
A11: ( h * z is convergent & lim (h * z) = 0. S )

proof

A12: now

let p be Real; :: thesis:
assume A13: 0 < p ; :: thesis:
ex pp being Real st
( pp > 0 & pp * ||.z.|| < p )

proof

take pp = p / (||.z.|| + 1); :: thesis:
A14: ||.z.|| + 1 > 0 + 0 by NORMSP_1:8, XREAL_1:10;
then A15: 0 < p / (||.z.|| + 1) by A13, XREAL_1:141;
A16: ||.z.|| + 0 < ||.z.|| + 1 by XREAL_1:10;
0 <= ||.z.|| by NORMSP_1:8;
then pp * ||.z.|| < pp * (||.z.|| + 1) by A15, A16, XREAL_1:99;
hence ( pp > 0 & pp * ||.z.|| < p ) by A13, A14, XCMPLX_1:88; :: thesis:

end;

then consider pp being Real such that
A17: ( pp > 0 & pp * ||.z.|| < p ) ;
( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
then consider n being Element of NAT such that
A18: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < pp by A17, SEQ_2:def 7;
take n = n; :: thesis:
let m be Element of NAT ; :: thesis:
assume A19: n <= m ; :: thesis:
A20: abs ((h . m) - 0 ) < pp by A18, A19;
A21: ||.(((h * z) . m) - (0. S)).|| = ||.(((h . m) * z) - (0. S)).|| by NDIFF_1:def 3
.= ||.((h . m) * z).|| by RLVECT_1:26
.= (abs (h . m)) * ||.z.|| by NORMSP_1:def 2 ;
0 <= ||.z.|| by NORMSP_1:8;
then (abs (h . m)) * ||.z.|| <= pp * ||.z.|| by A20, XREAL_1:66;
hence ||.(((h * z) . m) - (0. S)).|| < p by A17, A21, XXREAL_0:2; :: thesis:

end;

hence h * z is convergent by NORMSP_1:def 9; :: thesis:
hence lim (h * z) = 0. S by A12, NORMSP_1:def 11; :: thesis:

end;

then A22: lim ((h * z) + c) = (0. S) + x0 by A9, A10, NORMSP_1:42
.= x0 by RLVECT_1:10 ;
(h * z) + c is convergent by A9, A11, NORMSP_1:34;
then consider n being Element of NAT such that
A23: for m being Element of NAT st n <= m holds
||.((((h * z) + c) . m) - x0).|| < g by A6, A22, NORMSP_1:def 11;
take n ; :: thesis:
let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (((h ^\ n) * z) + c) ; :: thesis:
then consider m being Element of NAT such that
A24: y = (((h ^\ n) * z) + c) . m by NFCONT_1:6;
||.((((h * z) + c) . (n + m)) - x0).|| < g by A23, NAT_1:11;
then ||.((((h * z) . (n + m)) + (c . (n + m))) - x0).|| < g by NORMSP_1:def 5;
then ||.((((h * z) . (n + m)) + x0) - x0).|| < g by A8;
then ||.((((h * z) . (n + m)) + (c . m)) - x0).|| < g by A8;
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 A25: ||.(((((h ^\ n) * z) + c) . m) - x0).|| < g by NORMSP_1:def 5;
reconsider y1 = y as Point of S by A24;
y1 in { w where w is Point of S : ||.(w - x0).|| < g } by A24, A25;
hence y in N by A7; :: thesis:

end;

then consider n being Element of NAT such that
A26: rng (((h ^\ n) * z) + c) c= N ;
A27: ( ((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 A2, A5, A26;

A28: now

let m be Element of NAT ; :: thesis:
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 5
.= ((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 5 ; :: thesis:

end;

x0 in N by NFCONT_1:4;
then A29: rng c c= dom f by A2, A4, ZFMISC_1:37;
((h ^\ n) " ) (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c)) = ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n

proof

now

let m be Element of NAT ; :: thesis:
A30: ((f /* ((h * z) + c)) ^\ n) . m = (f /* ((h * z) + c)) . (n + m) by NAT_1:def 3
.= f /. (((h * z) + c) . (n + m)) by A3, FUNCT_2:186
.= f /. ((((h * z) + c) ^\ n) . m) by NAT_1:def 3
.= f /. ((((h ^\ n) * z) + c) . m) by A28 ;
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 6
.= (((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 A29, A30, FUNCT_2:186
.= (((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 A29, FUNCT_2:186
.= (((h ^\ n) . m) " ) * (((f /* (((h ^\ n) * z) + c)) . m) - ((f /* c) . m)) by A4, A26, FUNCT_2:186, XBOOLE_1:1
.= (((h ^\ n) . m) " ) * (((f /* (((h ^\ n) * z) + c)) - (f /* c)) . m) by NORMSP_1:def 6
.= (((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:

end;

hence ((h ^\ n) " ) (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c)) = ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n by FUNCT_2:113; :: thesis:

end;

hence ( (h " ) (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff f,x0) . z = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A27, LOPBAN_3:15, LOPBAN_3:16; :: thesis: