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:
consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: 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 A1, NDIFF_1:52;
consider R being REST of S,T such that
A4: R /. (0. S) = 0. T and
R is_continuous_in 0. S and
A5: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) by A3;

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
A6: rng c = {x0} and
A7: rng ((h * z) + c) c= N ; :: thesis:
x0 in N by NFCONT_1:4;
then A8: rng c c= dom f by A2, A6, ZFMISC_1:37;
A9: 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

let n be Element of NAT ; :: thesis:
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 ;
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A10: rng (h * z) c= dom R ;
dom c = NAT by FUNCT_2:def 1;
then c . n in rng c by FUNCT_1:12;
then A11: c . n = x0 by A6, 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 A7;
then ((h * z) . n) + (c . n) in N by NORMSP_1:def 5;
then A12: ((h . n) * z) + x0 in N by A11, NDIFF_1:def 3;
h is non-zero by FDIFF_1:def 1;
then A13: h . n <> 0 by SEQ_1:7;
(((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 A2, A7, FUNCT_2:186, XBOOLE_1:1
.= (((h . n) " ) * ((f /. (((h * z) + c) . n)) - (f /. (c . n)))) - ((diff f,x0) . z) by A8, 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 A5, A11, A12
.= (((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 9
.= ((((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 9
.= ((((h . n) " ) * (R /. ((h . n) * z))) + (1 * ((diff f,x0) . z))) - ((diff f,x0) . z) by A13, XCMPLX_0:def 7
.= ((((h . n) " ) * (R /. ((h . n) * z))) + ((diff f,x0) . z)) - ((diff f,x0) . z) by RLVECT_1:def 9
.= (((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 A10, 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;

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

proof

now

per cases ;

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

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

proof

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

end;

then A18: ((abs h) " ) (#) (R /* (h * z)) is constant by VALUED_0:def 18;
(((abs h) " ) (#) (R /* (h * z))) . 0 = 0. T by A16;
hence ( ((abs h) " ) (#) (R /* (h * z)) is convergent & lim (((abs h) " ) (#) (R /* (h * z))) = 0. T ) by A18, 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 A19: rng s c= dom R ;
h is non-zero by FDIFF_1:def 1;
then h . n <> 0 by SEQ_1:7;
then A20: 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 A21: ||.(s . n).|| <> 0 by NORMSP_1:def 2;
||.(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 A20, 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 A21, XCMPLX_1:60
.= (abs (h . n)) " ;
then A22: ||.z.|| * ((||.s.|| . n) " ) = (abs (h . n)) " by NORMSP_1:def 10;
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 ;
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 A23, FUNCT_2:186
.= (||.z.|| * ((||.s.|| " ) . n)) * (R /. (s . n)) by A22, VALUED_1:10
.= ||.z.|| * (((||.s.|| " ) . n) * (R /. (s . n))) by RLVECT_1:def 9
.= ||.z.|| * (((||.s.|| " ) . n) * ((R /* s) . n)) by A19, 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 A24: ((abs h) " ) (#) (R /* (h * z)) = ||.z.|| * ((||.s.|| " ) (#) (R /* s)) by FUNCT_2:113;
A25: ( (||.s.|| " ) (#) (R /* s) is convergent & lim ((||.s.|| " ) (#) (R /* s)) = 0. T ) by NDIFF_1:def 5;
hence ((abs h) " ) (#) (R /* (h * z)) is convergent by A24, NORMSP_1:37; :: thesis:
thus lim (((abs h) " ) (#) (R /* (h * z))) = ||.z.|| * (0. T) by A24, A25, 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;

A26: ( (h " ) (#) (R /* (h * z)) is convergent & lim ((h " ) (#) (R /* (h * z))) = 0. T )

proof

A27: now

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

now

let n be Element of NAT ; :: thesis:
assume A30: 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 A29, A30; :: 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;

hence (h " ) (#) (R /* (h * z)) is convergent by NORMSP_1:def 9; :: thesis:
hence lim ((h " ) (#) (R /* (h * z))) = 0. T by A27, NORMSP_1:def 11; :: thesis:

end;

A31: now

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

now

let n be Element of NAT ; :: thesis:
assume A34: m <= n ; :: thesis:
||.((((h " ) (#) (R /* (h * z))) . n) - (0. T)).|| < e by A33, A34;
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 A9; :: 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 A31, 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 A2; :: thesis: