let T, S be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
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 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))) ) ) )
let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_differentiable_in x0 holds
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 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))) ) ) )
let x0 be Point of S; :: thesis: ( f is_differentiable_in x0 implies 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 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))) ) ) ) )
assume f is_differentiable_in x0 ; :: thesis: 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 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))) ) ) )
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:47;
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: for h being convergent_to_0 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 & lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = (diff (f,x0)) . z )
let h be convergent_to_0 Real_Sequence; :: thesis: 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 & lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = (diff (f,x0)) . z )
let c be constant sequence of S; :: thesis: ( rng c = {x0} & rng ((h * z) + c) c= N implies ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = (diff (f,x0)) . z ) )
assume that
A5: rng c = {x0} and
A6: rng ((h * z) + c) c= N ; :: thesis: ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = (diff (f,x0)) . z )
A7: ( ((abs h) ") (#) (R /* (h * z)) is convergent & lim (((abs h) ") (#) (R /* (h * z))) = 0. T )

proof

now

per cases ( z = 0. S or z <> 0. S ) ;

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

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

proof

let n be Nat; :: thesis: (((abs h) ") (#) (R /* (h * z))) . n = 0. T
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 2;
then A9: rng (h * z) c= dom R ;
A10: n in NAT by ORDINAL1:def 12;
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:12
.= ((abs (h . n)) ") * (R /. ((h * z) . n)) by A10, A9, FUNCT_2:109
.= ((abs (h . n)) ") * (R /. ((h . n) * (0. S))) by A8, A10, NDIFF_1:def 3
.= ((abs (h . n)) ") * (R /. (0. S)) by RLVECT_1:10
.= 0. T by A3, RLVECT_1:10 ;
:: thesis: verum

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

end;

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

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

now

let n be Element of NAT ; :: thesis: (((abs h) ") (#) (R /* (h * z))) . n = (||.z.|| * ((||.s.|| ") (#) (R /* s))) . n
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 2;
then A11: rng s c= dom R ;
h is non-empty by FDIFF_1:def 1;
then h . n <> 0 by SEQ_1:5;
then A12: abs (h . n) <> 0 by COMPLEX1:47;
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 1 ;
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 2;
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:12
.= ((abs (h . n)) ") * (R /. ((h * z) . n)) by A15, FUNCT_2:109
.= (||.z.|| * ((||.s.|| ") . n)) * (R /. (s . n)) by A14, VALUED_1:10
.= ||.z.|| * (((||.s.|| ") . n) * (R /. (s . n))) by RLVECT_1:def 7
.= ||.z.|| * (((||.s.|| ") . n) * ((R /* s) . n)) by A11, FUNCT_2:109
.= ||.z.|| * (((||.s.|| ") (#) (R /* s)) . n) by NDIFF_1:def 2
.= (||.z.|| * ((||.s.|| ") (#) (R /* s))) . n by NORMSP_1:def 5 ; :: thesis: verum

end;

then A16: ((abs h) ") (#) (R /* (h * z)) = ||.z.|| * ((||.s.|| ") (#) (R /* s)) by FUNCT_2:63;
A17: (||.s.|| ") (#) (R /* s) is convergent by NDIFF_1:def 5;
hence ((abs h) ") (#) (R /* (h * z)) is convergent by A16, NORMSP_1:22; :: thesis: lim (((abs h) ") (#) (R /* (h * z))) = 0. T
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:28
.= 0. T by RLVECT_1:10 ;
:: thesis: verum

end;

end;

end;

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

end;

A18: now

let e be Real; :: thesis: ( 0 < e implies 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 )
assume 0 < e ; :: thesis: 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
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 7;

now

let n be Element of NAT ; :: thesis: ( m <= n implies ||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e )
assume A20: m <= n ; :: thesis: ||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e
||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| = ||.(((h ") (#) (R /* (h * z))) . n).|| by RLVECT_1:13
.= ||.(((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 1
.= ||.((abs ((h . n) ")) * ((R /* (h * z)) . n)).|| by NORMSP_1:def 1
.= ||.((abs ((h ") . n)) * ((R /* (h * z)) . n)).|| by VALUED_1:10
.= ||.(((abs (h ")) . n) * ((R /* (h * z)) . n)).|| by SEQ_1:12
.= ||.((((abs h) ") . n) * ((R /* (h * z)) . n)).|| by SEQ_1:54
.= ||.((((abs h) ") (#) (R /* (h * z))) . n).|| by NDIFF_1:def 2
.= ||.(((((abs h) ") (#) (R /* (h * z))) . n) - (0. T)).|| by RLVECT_1:13 ;
hence ||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e by A19, A20; :: thesis: verum

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

end;

x0 in N by NFCONT_1:4;
then A21: rng c c= dom f by A1, A5, ZFMISC_1:31;
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 2;
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 14;
then reconsider L = diff (f,x0) as Element of BoundedLinearOperators (S,T) ;
let n be Element of NAT ; :: thesis: ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| = ||.(((h ") (#) (R /* (h * z))) . n).||
h is non-empty by FDIFF_1:def 1;
then A24: h . n <> 0 by SEQ_1:5;
dom c = NAT by FUNCT_2:def 1;
then c . n in rng c by FUNCT_1:3;
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:3;
then ((h * z) + c) . n in N by A6;
then ((h * z) . n) + (c . n) in N by NORMSP_1:def 2;
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 3
.= (((h . n) ") * ((f /. (((h * z) + c) . n)) - ((f /* c) . n))) - ((diff (f,x0)) . z) by A1, A6, FUNCT_2:109, XBOOLE_1:1
.= (((h . n) ") * ((f /. (((h * z) + c) . n)) - (f /. (c . n)))) - ((diff (f,x0)) . z) by A21, FUNCT_2:109
.= (((h . n) ") * ((f /. (((h * z) . n) + (c . n))) - (f /. (c . n)))) - ((diff (f,x0)) . z) by NORMSP_1:def 2
.= (((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 3
.= (((h . n) ") * (((diff (f,x0)) . (((h . n) * z) + (x0 - x0))) + (R /. (((h . n) * z) + (x0 - x0))))) - ((diff (f,x0)) . z) by RLVECT_1:def 3
.= (((h . n) ") * (((diff (f,x0)) . (((h . n) * z) + (0. S))) + (R /. (((h . n) * z) + (x0 - x0))))) - ((diff (f,x0)) . z) by RLVECT_1:15
.= (((h . n) ") * (((diff (f,x0)) . (((h . n) * z) + (0. S))) + (R /. (((h . n) * z) + (0. S))))) - ((diff (f,x0)) . z) by RLVECT_1:15
.= (((h . n) ") * (((diff (f,x0)) . ((h . n) * z)) + (R /. (((h . n) * z) + (0. S))))) - ((diff (f,x0)) . z) by RLVECT_1:4
.= (((h . n) ") * (((diff (f,x0)) . ((h . n) * z)) + (R /. ((h . n) * z)))) - ((diff (f,x0)) . z) by RLVECT_1:4
.= ((((h . n) ") * (R /. ((h . n) * z))) + (((h . n) ") * ((diff (f,x0)) . ((h . n) * z)))) - ((diff (f,x0)) . z) by RLVECT_1:def 5
.= ((((h . n) ") * (R /. ((h . n) * z))) + (((h . n) ") * ((modetrans (L,S,T)) . ((h . n) * z)))) - ((diff (f,x0)) . z) by LOPBAN_1:def 11
.= ((((h . n) ") * (R /. ((h . n) * z))) + (((h . n) ") * ((h . n) * ((modetrans (L,S,T)) . z)))) - ((diff (f,x0)) . z) by LOPBAN_1:def 5
.= ((((h . n) ") * (R /. ((h . n) * z))) + (((h . n) ") * ((h . n) * (L . z)))) - ((diff (f,x0)) . z) by LOPBAN_1:def 11
.= ((((h . n) ") * (R /. ((h . n) * z))) + ((((h . n) ") * (h . n)) * ((diff (f,x0)) . z))) - ((diff (f,x0)) . z) by RLVECT_1:def 7
.= ((((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 8
.= (((h . n) ") * (R /. ((h . n) * z))) + (((diff (f,x0)) . z) - ((diff (f,x0)) . z)) by RLVECT_1:def 3
.= (((h . n) ") * (R /. ((h . n) * z))) + (0. T) by RLVECT_1:15
.= ((h . n) ") * (R /. ((h . n) * z)) by RLVECT_1:4
.= ((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:109
.= ((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: verum

end;

A27: now

let e be Real; :: thesis: ( 0 < e implies 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 )
assume 0 < e ; :: thesis: 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
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: ( m <= n implies ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| < e )
assume m <= n ; :: thesis: ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| < e
then ||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e by A28;
then ||.(((h ") (#) (R /* (h * z))) . n).|| < e by RLVECT_1:13;
hence ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| < e by A22; :: thesis: verum

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

end;

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

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