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
ex N being Neighbourhood of x0 st
( N c= dom f & ( 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))) ) ) )
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 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))) ) ) )
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 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))) ) ) ) )
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 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))) ) ) )
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: ex R being RestFunc 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 RestFunc 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 :: 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= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = (diff (f,x0)) . z )

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= 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 non-zero 0 -convergent 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 :: thesis: ( ( z = 0. S & ((abs h) ") (#) (R /* (h * z)) is convergent & lim (((abs h) ") (#) (R /* (h * z))) = 0. T ) or ( z <> 0. S & ((abs h) ") (#) (R /* (h * z)) is convergent & lim (((abs h) ") (#) (R /* (h * z))) = 0. T ) )

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;
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
.= (|.(h . n).| ") * ((R /* (h * z)) . n) by SEQ_1:12
.= (|.(h . n).| ") * (R /. ((h * z) . n)) by A10, A9, FUNCT_2:109
.= (|.(h . n).| ") * (R /. ((h . n) * (0. S))) by A8, NDIFF_1:def 3
.= (|.(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 A11: ( h * z is non-zero & h * z is 0. S -convergent ) by NDIFF_1:21;
then reconsider s = h * z as 0. S -convergent sequence of S ;

now :: thesis: for n being Element of NAT holds (((abs h) ") (#) (R /* (h * z))) . n = (||.z.|| * ((||.s.|| ") (#) (R /* s))) . n

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 A12: rng s c= dom R ;
h . n <> 0 by SEQ_1:5;
then A13: |.(h . n).| <> 0 by COMPLEX1:47;
s . n <> 0. S by NDIFF_1:7, A11;
then A14: ||.(s . n).|| <> 0 by NORMSP_0:def 5;
||.(s . n).|| = ||.((h . n) * z).|| by NDIFF_1:def 3
.= |.(h . n).| * ||.z.|| by NORMSP_1:def 1 ;
then (|.(h . n).| ") * ||.(s . n).|| = ((|.(h . n).| ") * |.(h . n).|) * ||.z.||
.= 1 * ||.z.|| by A13, XCMPLX_0:def 7
.= ||.z.|| ;
then ||.z.|| * (||.(s . n).|| ") = (|.(h . n).| ") * (||.(s . n).|| * (||.(s . n).|| "))
.= (|.(h . n).| ") * (||.(s . n).|| / ||.(s . n).||) by XCMPLX_0:def 9
.= (|.(h . n).| ") * 1 by A14, XCMPLX_1:60
.= |.(h . n).| " ;
then A15: ||.z.|| * ((||.s.|| . n) ") = |.(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 A16: 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
.= (|.(h . n).| ") * ((R /* (h * z)) . n) by SEQ_1:12
.= (|.(h . n).| ") * (R /. ((h * z) . n)) by A16, FUNCT_2:109
.= (||.z.|| * ((||.s.|| ") . n)) * (R /. (s . n)) by A15, VALUED_1:10
.= ||.z.|| * (((||.s.|| ") . n) * (R /. (s . n))) by RLVECT_1:def 7
.= ||.z.|| * (((||.s.|| ") . n) * ((R /* s) . n)) by A12, 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 A17: ((abs h) ") (#) (R /* (h * z)) = ||.z.|| * ((||.s.|| ") (#) (R /* s)) by FUNCT_2:63;
A18: (||.s.|| ") (#) (R /* s) is convergent by A11, NDIFF_1:def 5;
hence ((abs h) ") (#) (R /* (h * z)) is convergent by A17, NORMSP_1:22; :: thesis: lim (((abs h) ") (#) (R /* (h * z))) = 0. T
lim ((||.s.|| ") (#) (R /* s)) = 0. T by A11, NDIFF_1:def 5;
hence lim (((abs h) ") (#) (R /* (h * z))) = ||.z.|| * (0. T) by A17, A18, 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;

A19: now :: thesis: for e being Real st 0 < e holds
ex m being Nat st
for n being Nat st m <= n holds
||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e

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

now :: thesis: for n being Nat st m <= n holds
||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e

let n be Nat; :: thesis: ( m <= n implies ||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e )
assume A21: 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
.= |.|.((h . n) ").|.| * ||.((R /* (h * z)) . n).|| by NORMSP_1:def 1
.= ||.(|.((h . n) ").| * ((R /* (h * z)) . n)).|| by NORMSP_1:def 1
.= ||.(|.((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 A20, A21; :: thesis: verum

end;

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

end;

x0 in N by NFCONT_1:4;
then A22: rng c c= dom f by A1, A5, ZFMISC_1:31;
A23: for n being 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 A24: 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 Nat; :: thesis: ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| = ||.(((h ") (#) (R /* (h * z))) . n).||
A25: n in NAT by ORDINAL1:def 12;
A26: 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, A25;
then A27: 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, A25;
then ((h * z) + c) . n in N by A6;
then ((h * z) . n) + (c . n) in N by NORMSP_1:def 2;
then A28: ((h . n) * z) + x0 in N by A27, 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, A25
.= (((h . n) ") * ((f /. (((h * z) + c) . n)) - (f /. (c . n)))) - ((diff (f,x0)) . z) by A22, FUNCT_2:109, A25
.= (((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, A27, A28
.= (((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 A26, 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 A24, FUNCT_2:109, A25
.= ((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;

A29: now :: thesis: for e being Real st 0 < e holds
ex m being Nat st
for n being Nat st m <= n holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| < e

let e be Real; :: thesis: ( 0 < e implies ex m being Nat st
for n being 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 Nat st
for n being Nat st m <= n holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| < e
then consider m being Nat such that
A30: for n being Nat st m <= n holds
||.((((h ") (#) (R /* (h * z))) . n) - (0. T)).|| < e by A19;

now :: thesis: for n being Nat st m <= n holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - ((diff (f,x0)) . z)).|| < e

let n be 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 A30;
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 A23; :: thesis: verum

end;

hence ex m being Nat st
for n being 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 A29, 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 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 A1; :: thesis: verum