let T, S be non trivial RealNormSpace; :: thesis:
let f be PartFunc of S,T; :: thesis:
let x0 be Point of S; :: thesis:
assume f is_differentiable_in x0 ; :: thesis:
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) by NDIFF_1:52;
consider R being REST of S,T such that
A3: R /. (0. S) = 0. T and
R is_continuous_in 0. S and
A4: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) by A2;

now

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
A5: rng c = {x0} and
A6: rng ((h * z) + c) c= N ; :: thesis:
A7: ( ((abs h) " ) (#) (R /* (h * z)) is convergent & lim (((abs h) " ) (#) (R /* (h * z))) = 0. T )

proof

now

per cases ;

case A8: z = 0. S ; :: thesis:

for n being Nat holds (((abs h) " ) (#) (R /* (h * z))) . n = 0. T

proof

let n be Nat; :: thesis:
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A9: rng (h * z) c= dom R ;
A10: n in NAT by ORDINAL1:def 13;
hence (((abs h) " ) (#) (R /* (h * z))) . n = (((abs h) " ) . n) * ((R /* (h * z)) . n) by NDIFF_1:def 2
.= (((abs h) . n) " ) * ((R /* (h * z)) . n) by VALUED_1:10
.= ((abs (h . n)) " ) * ((R /* (h * z)) . n) by A10, SEQ_1:16
.= ((abs (h . n)) " ) * (R /. ((h * z) . n)) by A10, A9, FUNCT_2:186
.= ((abs (h . n)) " ) * (R /. ((h . n) * (0. S))) by A8, A10, NDIFF_1:def 3
.= ((abs (h . n)) " ) * (R /. (0. S)) by RLVECT_1:23
.= 0. T by A3, RLVECT_1:23 ;
:: thesis:

end;

then ( ((abs h) " ) (#) (R /* (h * z)) is constant & (((abs h) " ) (#) (R /* (h * z))) . 0 = 0. T ) by VALUED_0:def 18;
hence ( ((abs h) " ) (#) (R /* (h * z)) is convergent & lim (((abs h) " ) (#) (R /* (h * z))) = 0. T ) by NDIFF_1:21; :: thesis:

end;

case z <> 0. S ; :: thesis:

then reconsider s = h * z as convergent_to_0 sequence of S by NDIFF_1:24;

now

let n be Element of NAT ; :: thesis:
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A11: rng s c= dom R ;
h is non-empty by FDIFF_1:def 1;
then h . n <> 0 by SEQ_1:7;
then A12: abs (h . n) <> 0 by COMPLEX1:133;
s is non-zero by NDIFF_1:def 4;
then s . n <> 0. S by NDIFF_1:7;
then A13: ||.(s . n).|| <> 0 by NORMSP_0:def 5;
||.(s . n).|| = ||.((h . n) * z).|| by NDIFF_1:def 3
.= (abs (h . n)) * ||.z.|| by NORMSP_1:def 2 ;
then ((abs (h . n)) " ) * ||.(s . n).|| = (((abs (h . n)) " ) * (abs (h . n))) * ||.z.||
.= 1 * ||.z.|| by A12, XCMPLX_0:def 7
.= ||.z.|| ;
then ||.z.|| * (||.(s . n).|| " ) = ((abs (h . n)) " ) * (||.(s . n).|| * (||.(s . n).|| " ))
.= ((abs (h . n)) " ) * (||.(s . n).|| / ||.(s . n).||) by XCMPLX_0:def 9
.= ((abs (h . n)) " ) * 1 by A13, XCMPLX_1:60
.= (abs (h . n)) " ;
then A14: ||.z.|| * ((||.s.|| . n) " ) = (abs (h . n)) " by NORMSP_0:def 4;
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A15: rng (h * z) c= dom R ;
thus (((abs h) " ) (#) (R /* (h * z))) . n = (((abs h) " ) . n) * ((R /* (h * z)) . n) by NDIFF_1:def 2
.= (((abs h) . n) " ) * ((R /* (h * z)) . n) by VALUED_1:10
.= ((abs (h . n)) " ) * ((R /* (h * z)) . n) by SEQ_1:16
.= ((abs (h . n)) " ) * (R /. ((h * z) . n)) by A15, FUNCT_2:186
.= (||.z.|| * ((||.s.|| " ) . n)) * (R /. (s . n)) by A14, VALUED_1:10
.= ||.z.|| * (((||.s.|| " ) . n) * (R /. (s . n))) by RLVECT_1:def 10
.= ||.z.|| * (((||.s.|| " ) . n) * ((R /* s) . n)) by A11, FUNCT_2:186
.= ||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n) by NDIFF_1:def 2
.= (||.z.|| * ((||.s.|| " ) (#) (R /* s))) . n by NORMSP_1:def 8 ; :: thesis:

end;

then A16: ((abs h) " ) (#) (R /* (h * z)) = ||.z.|| * ((||.s.|| " ) (#) (R /* s)) by FUNCT_2:113;
A17: (||.s.|| " ) (#) (R /* s) is convergent by NDIFF_1:def 5;
hence ((abs h) " ) (#) (R /* (h * z)) is convergent by A16, NORMSP_1:37; :: thesis:
lim ((||.s.|| " ) (#) (R /* s)) = 0. T by NDIFF_1:def 5;
hence lim (((abs h) " ) (#) (R /* (h * z))) = ||.z.|| * (0. T) by A16, A17, NORMSP_1:45
.= 0. T by RLVECT_1:23 ;
:: thesis:

end;

hence ( ((abs h) " ) (#) (R /* (h * z)) is convergent & lim (((abs h) " ) (#) (R /* (h * z))) = 0. T ) ; :: thesis:

end;

A18: now

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider m being Element of NAT such that
A19: for n being Element of NAT st m <= n holds
||.(((((abs h) " ) (#) (R /* (h * z))) . n) - (0. T)).|| < e by A7, NORMSP_1:def 11;

now

let n be Element of NAT ; :: thesis:
assume A20: m <= n ; :: thesis:
||.((((h " ) (#) (R /* (h * z))) . n) - (0. T)).|| = ||.(((h " ) (#) (R /* (h * z))) . n).|| by RLVECT_1:26
.= ||.(((h " ) . n) * ((R /* (h * z)) . n)).|| by NDIFF_1:def 2
.= ||.(((h . n) " ) * ((R /* (h * z)) . n)).|| by VALUED_1:10
.= (abs (abs ((h . n) " ))) * ||.((R /* (h * z)) . n).|| by NORMSP_1:def 2
.= ||.((abs ((h . n) " )) * ((R /* (h * z)) . n)).|| by NORMSP_1:def 2
.= ||.((abs ((h " ) . n)) * ((R /* (h * z)) . n)).|| by VALUED_1:10
.= ||.(((abs (h " )) . n) * ((R /* (h * z)) . n)).|| by SEQ_1:16
.= ||.((((abs h) " ) . n) * ((R /* (h * z)) . n)).|| by SEQ_1:62
.= ||.((((abs h) " ) (#) (R /* (h * z))) . n).|| by NDIFF_1:def 2
.= ||.(((((abs h) " ) (#) (R /* (h * z))) . n) - (0. T)).|| by RLVECT_1:26 ;
hence ||.((((h " ) (#) (R /* (h * z))) . n) - (0. T)).|| < e by A19, A20; :: thesis:

end;

hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((((h " ) (#) (R /* (h * z))) . n) - (0. T)).|| < e ; :: thesis:

end;

x0 in N by NFCONT_1:4;
then A21: rng c c= dom f by A1, A5, ZFMISC_1:37;
A22: for n being Element of NAT holds ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff f,x0) . z)).|| = ||.(((h " ) (#) (R /* (h * z))) . n).||

proof

R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A23: rng (h * z) c= dom R ;
R_NormSpace_of_BoundedLinearOperators S,T = NORMSTR(# (BoundedLinearOperators S,T),(Zero_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Add_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Mult_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(BoundedLinearOperatorsNorm S,T) #) by LOPBAN_1:def 15;
then reconsider L = diff f,x0 as Element of BoundedLinearOperators S,T ;
let n be Element of NAT ; :: thesis:
h is non-empty by FDIFF_1:def 1;
then A24: h . n <> 0 by SEQ_1:7;
dom c = NAT by FUNCT_2:def 1;
then c . n in rng c by FUNCT_1:12;
then A25: c . n = x0 by A5, TARSKI:def 1;
dom ((h * z) + c) = NAT by FUNCT_2:def 1;
then ((h * z) + c) . n in rng ((h * z) + c) by FUNCT_1:12;
then ((h * z) + c) . n in N by A6;
then ((h * z) . n) + (c . n) in N by NORMSP_1:def 5;
then A26: ((h . n) * z) + x0 in N by A25, NDIFF_1:def 3;
(((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff f,x0) . z) = (((h " ) . n) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - ((diff f,x0) . z) by NDIFF_1:def 2
.= (((h . n) " ) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - ((diff f,x0) . z) by VALUED_1:10
.= (((h . n) " ) * (((f /* ((h * z) + c)) . n) - ((f /* c) . n))) - ((diff f,x0) . z) by NORMSP_1:def 6
.= (((h . n) " ) * ((f /. (((h * z) + c) . n)) - ((f /* c) . n))) - ((diff f,x0) . z) by A1, A6, FUNCT_2:186, XBOOLE_1:1
.= (((h . n) " ) * ((f /. (((h * z) + c) . n)) - (f /. (c . n)))) - ((diff f,x0) . z) by A21, FUNCT_2:186
.= (((h . n) " ) * ((f /. (((h * z) . n) + (c . n))) - (f /. (c . n)))) - ((diff f,x0) . z) by NORMSP_1:def 5
.= (((h . n) " ) * ((f /. (((h . n) * z) + (c . n))) - (f /. (c . n)))) - ((diff f,x0) . z) by NDIFF_1:def 3
.= (((h . n) " ) * (((diff f,x0) . ((((h . n) * z) + x0) - x0)) + (R /. ((((h . n) * z) + x0) - x0)))) - ((diff f,x0) . z) by A4, A25, A26
.= (((h . n) " ) * (((diff f,x0) . (((h . n) * z) + (x0 - x0))) + (R /. ((((h . n) * z) + x0) - x0)))) - ((diff f,x0) . z) by RLVECT_1:def 6
.= (((h . n) " ) * (((diff f,x0) . (((h . n) * z) + (x0 - x0))) + (R /. (((h . n) * z) + (x0 - x0))))) - ((diff f,x0) . z) by RLVECT_1:def 6
.= (((h . n) " ) * (((diff f,x0) . (((h . n) * z) + (0. S))) + (R /. (((h . n) * z) + (x0 - x0))))) - ((diff f,x0) . z) by RLVECT_1:28
.= (((h . n) " ) * (((diff f,x0) . (((h . n) * z) + (0. S))) + (R /. (((h . n) * z) + (0. S))))) - ((diff f,x0) . z) by RLVECT_1:28
.= (((h . n) " ) * (((diff f,x0) . ((h . n) * z)) + (R /. (((h . n) * z) + (0. S))))) - ((diff f,x0) . z) by RLVECT_1:10
.= (((h . n) " ) * (((diff f,x0) . ((h . n) * z)) + (R /. ((h . n) * z)))) - ((diff f,x0) . z) by RLVECT_1:10
.= ((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * ((diff f,x0) . ((h . n) * z)))) - ((diff f,x0) . z) by RLVECT_1:def 8
.= ((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * ((modetrans L,S,T) . ((h . n) * z)))) - ((diff f,x0) . z) by LOPBAN_1:def 12
.= ((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * ((h . n) * ((modetrans L,S,T) . z)))) - ((diff f,x0) . z) by LOPBAN_1:def 6
.= ((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * ((h . n) * (L . z)))) - ((diff f,x0) . z) by LOPBAN_1:def 12
.= ((((h . n) " ) * (R /. ((h . n) * z))) + ((((h . n) " ) * (h . n)) * ((diff f,x0) . z))) - ((diff f,x0) . z) by RLVECT_1:def 10
.= ((((h . n) " ) * (R /. ((h . n) * z))) + (1 * ((diff f,x0) . z))) - ((diff f,x0) . z) by A24, XCMPLX_0:def 7
.= ((((h . n) " ) * (R /. ((h . n) * z))) + ((diff f,x0) . z)) - ((diff f,x0) . z) by RLVECT_1:def 11
.= (((h . n) " ) * (R /. ((h . n) * z))) + (((diff f,x0) . z) - ((diff f,x0) . z)) by RLVECT_1:def 6
.= (((h . n) " ) * (R /. ((h . n) * z))) + (0. T) by RLVECT_1:28
.= ((h . n) " ) * (R /. ((h . n) * z)) by RLVECT_1:10
.= ((h " ) . n) * (R /. ((h . n) * z)) by VALUED_1:10
.= ((h " ) . n) * (R /. ((h * z) . n)) by NDIFF_1:def 3
.= ((h " ) . n) * ((R /* (h * z)) . n) by A23, FUNCT_2:186
.= ((h " ) (#) (R /* (h * z))) . n by NDIFF_1:def 2 ;
hence ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff f,x0) . z)).|| = ||.(((h " ) (#) (R /* (h * z))) . n).|| ; :: thesis:

end;

A27: now

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider m being Element of NAT such that
A28: for n being Element of NAT st m <= n holds
||.((((h " ) (#) (R /* (h * z))) . n) - (0. T)).|| < e by A18;

now

let n be Element of NAT ; :: thesis:
assume m <= n ; :: thesis:
then ||.((((h " ) (#) (R /* (h * z))) . n) - (0. T)).|| < e by A28;
then ||.(((h " ) (#) (R /* (h * z))) . n).|| < e by RLVECT_1:26;
hence ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff f,x0) . z)).|| < e by A22; :: thesis:

end;

hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff f,x0) . z)).|| < e ; :: thesis:

end;

hence (h " ) (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent by NORMSP_1:def 9; :: thesis:
hence lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) = (diff f,x0) . z by A27, NORMSP_1:def 11; :: thesis:

end;

hence ex N being Neighbourhood of x0 st
( N c= dom f & ( 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; :: thesis: