:: NDIFF_2 semantic presentation
begin
definition
let X, Y, Z be RealNormSpace;
let f be Element of BoundedLinearOperators (X,Y);
let g be Element of BoundedLinearOperators (Y,Z);
funcg * f -> Element of BoundedLinearOperators (X,Z) equals :: NDIFF_2:def 1
(modetrans (g,Y,Z)) * (modetrans (f,X,Y));
correctness
coherence
(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Element of BoundedLinearOperators (X,Z);
proof
(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2;
hence (modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Element of BoundedLinearOperators (X,Z) by LOPBAN_1:def_9; ::_thesis: verum
end;
end;
:: deftheorem defines * NDIFF_2:def_1_:_
for X, Y, Z being RealNormSpace
for f being Element of BoundedLinearOperators (X,Y)
for g being Element of BoundedLinearOperators (Y,Z) holds g * f = (modetrans (g,Y,Z)) * (modetrans (f,X,Y));
definition
let X, Y, Z be RealNormSpace;
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y));
let g be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z));
funcg * f -> Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) equals :: NDIFF_2:def 2
(modetrans (g,Y,Z)) * (modetrans (f,X,Y));
correctness
coherence
(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,Z));
proof
( R_NormSpace_of_BoundedLinearOperators (X,Z) = NORMSTR(# (BoundedLinearOperators (X,Z)),(Zero_ ((BoundedLinearOperators (X,Z)),(R_VectorSpace_of_LinearOperators (X,Z)))),(Add_ ((BoundedLinearOperators (X,Z)),(R_VectorSpace_of_LinearOperators (X,Z)))),(Mult_ ((BoundedLinearOperators (X,Z)),(R_VectorSpace_of_LinearOperators (X,Z)))),(BoundedLinearOperatorsNorm (X,Z)) #) & (modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Lipschitzian LinearOperator of X,Z ) by LOPBAN_1:def_14, LOPBAN_2:2;
hence (modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) by LOPBAN_1:def_9; ::_thesis: verum
end;
end;
:: deftheorem defines * NDIFF_2:def_2_:_
for X, Y, Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds g * f = (modetrans (g,Y,Z)) * (modetrans (f,X,Y));
theorem Th1: :: NDIFF_2:1
for T, S being non trivial RealNormSpace
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))) ) ) )
proof
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 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_)_)
percases ( z = 0. S or z <> 0. S ) ;
caseA8: 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 non-zero 0. S -convergent sequence of S by NDIFF_1:21;
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 A11: rng s c= dom R ;
h . n <> 0 by SEQ_1:5;
then A12: abs (h . n) <> 0 by COMPLEX1:47;
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__::_thesis:_for_e_being_Real_st_0_<_e_holds_
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
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__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((((h_")_(#)_(R_/*_(h_*_z)))_._n)_-_(0._T)).||_<_e
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).||
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__::_thesis:_for_e_being_Real_st_0_<_e_holds_
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
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__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((((h_")_(#)_((f_/*_((h_*_z)_+_c))_-_(f_/*_c)))_._n)_-_((diff_(f,x0))_._z)).||_<_e
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 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
end;
theorem :: NDIFF_2:2
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
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= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
proof
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
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= dom f 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
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= dom f 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 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= dom f 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: 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= dom f 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: 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 Th1;
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= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
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= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
let c be constant sequence of S; ::_thesis: ( rng c = {x0} & rng ((h * z) + c) c= dom f implies ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) )
assume that
A3: rng c = {x0} and
A4: rng ((h * z) + c) c= dom f ; ::_thesis: ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
x0 in N by NFCONT_1:4;
then A5: rng c c= dom f by A3, A1, ZFMISC_1:31;
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_1;
A8: for n being Element of NAT holds c . n = x0
proof
let n be Element of NAT ; ::_thesis: c . n = x0
c . n in rng c by NFCONT_1:6;
hence c . n = x0 by A3, TARSKI:def_1; ::_thesis: verum
end;
ex n being Element of NAT st rng (((h ^\ n) * z) + c) c= N
proof
A9: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((h_*_z)_._m)_-_(0._S)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((h * z) . m) - (0. S)).|| < p )
assume A10: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((h * z) . m) - (0. S)).|| < p
ex pp being Real st
( pp > 0 & pp * ||.z.|| < p )
proof
take pp = p / (||.z.|| + 1); ::_thesis: ( pp > 0 & pp * ||.z.|| < p )
A11: ( ||.z.|| + 0 < ||.z.|| + 1 & 0 <= ||.z.|| ) by NORMSP_1:4, XREAL_1:8;
A12: ||.z.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.z.|| + 1) by A10, XREAL_1:139;
then pp * ||.z.|| < pp * (||.z.|| + 1) by A11, XREAL_1:97;
hence ( pp > 0 & pp * ||.z.|| < p ) by A10, A12, XCMPLX_1:87; ::_thesis: verum
end;
then consider pp being Real such that
A13: pp > 0 and
A14: pp * ||.z.|| < p ;
( h is convergent & lim h = 0 ) ;
then consider n being Element of NAT such that
A15: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < pp by A13, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.(((h * z) . m) - (0. S)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((h * z) . m) - (0. S)).|| < p )
assume n <= m ; ::_thesis: ||.(((h * z) . m) - (0. S)).|| < p
then A16: abs ((h . m) - 0) < pp by A15;
A17: ||.(((h * z) . m) - (0. S)).|| = ||.(((h . m) * z) - (0. S)).|| by NDIFF_1:def_3
.= ||.((h . m) * z).|| by RLVECT_1:13
.= (abs (h . m)) * ||.z.|| by NORMSP_1:def_1 ;
0 <= ||.z.|| by NORMSP_1:4;
then (abs (h . m)) * ||.z.|| <= pp * ||.z.|| by A16, XREAL_1:64;
hence ||.(((h * z) . m) - (0. S)).|| < p by A14, A17, XXREAL_0:2; ::_thesis: verum
end;
then A18: h * z is convergent by NORMSP_1:def_6;
c . 0 in rng c by NFCONT_1:6;
then c . 0 = x0 by A3, TARSKI:def_1;
then A19: lim c = x0 by NDIFF_1:18;
A20: c is convergent by NDIFF_1:18;
then A21: (h * z) + c is convergent by A18, NORMSP_1:19;
lim (h * z) = 0. S by A9, A18, NORMSP_1:def_7;
then lim ((h * z) + c) = (0. S) + x0 by A20, A19, A18, NORMSP_1:25
.= x0 by RLVECT_1:4 ;
then consider n being Element of NAT such that
A22: for m being Element of NAT st n <= m holds
||.((((h * z) + c) . m) - x0).|| < g by A6, A21, NORMSP_1:def_7;
take n ; ::_thesis: rng (((h ^\ n) * z) + c) c= N
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (((h ^\ n) * z) + c) or y in N )
assume y in rng (((h ^\ n) * z) + c) ; ::_thesis: y in N
then consider m being Element of NAT such that
A23: y = (((h ^\ n) * z) + c) . m by NFCONT_1:6;
reconsider y1 = y as Point of S by A23;
||.((((h * z) + c) . (n + m)) - x0).|| < g by A22, NAT_1:11;
then ||.((((h * z) . (n + m)) + (c . (n + m))) - x0).|| < g by NORMSP_1:def_2;
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 ||.(((((h ^\ n) * z) + c) . m) - x0).|| < g by NORMSP_1:def_2;
then y1 in { w where w is Point of S : ||.(w - x0).|| < g } by A23;
hence y in N by A7; ::_thesis: verum
end;
then consider n being Element of NAT such that
A24: rng (((h ^\ n) * z) + c) c= N ;
A25: now__::_thesis:_for_m_being_Element_of_NAT_holds_(((h_*_z)_+_c)_^\_n)_._m_=_(((h_^\_n)_*_z)_+_c)_._m
let m be Element of NAT ; ::_thesis: (((h * z) + c) ^\ n) . m = (((h ^\ n) * z) + c) . m
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_2
.= ((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_2 ; ::_thesis: verum
end;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(((h_")_(#)_((f_/*_((h_*_z)_+_c))_-_(f_/*_c)))_^\_n)_._m_=_(((h_^\_n)_")_(#)_((f_/*_(((h_^\_n)_*_z)_+_c))_-_(f_/*_c)))_._m
let m be Element of NAT ; ::_thesis: (((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n) . m = (((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) . m
A26: ((f /* ((h * z) + c)) ^\ n) . m = (f /* ((h * z) + c)) . (n + m) by NAT_1:def_3
.= f /. (((h * z) + c) . (n + m)) by A4, FUNCT_2:109
.= f /. ((((h * z) + c) ^\ n) . m) by NAT_1:def_3
.= f /. ((((h ^\ n) * z) + c) . m) by A25 ;
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_3
.= (((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 A5, A26, FUNCT_2:109
.= (((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 A5, FUNCT_2:109
.= (((h ^\ n) . m) ") * (((f /* (((h ^\ n) * z) + c)) . m) - ((f /* c) . m)) by A1, A24, FUNCT_2:109, XBOOLE_1:1
.= (((h ^\ n) . m) ") * (((f /* (((h ^\ n) * z) + c)) - (f /* c)) . m) by NORMSP_1:def_3
.= (((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: verum
end;
then A27: ((h ^\ n) ") (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c)) = ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n by FUNCT_2:63;
( ((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 A3, A2, A24;
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:10, LOPBAN_3:11; ::_thesis: verum
end;
theorem Th3: :: NDIFF_2:3
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S
for N being Neighbourhood of x0 st N c= dom f holds
for z being Point of S
for dv being Point of T holds
( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for x0 being Point of S
for N being Neighbourhood of x0 st N c= dom f holds
for z being Point of S
for dv being Point of T holds
( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
let f be PartFunc of S,T; ::_thesis: for x0 being Point of S
for N being Neighbourhood of x0 st N c= dom f holds
for z being Point of S
for dv being Point of T holds
( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
let x0 be Point of S; ::_thesis: for N being Neighbourhood of x0 st N c= dom f holds
for z being Point of S
for dv being Point of T holds
( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
let N be Neighbourhood of x0; ::_thesis: ( N c= dom f implies for z being Point of S
for dv being Point of T holds
( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) )
assume A1: N c= dom f ; ::_thesis: for z being Point of S
for dv being Point of T holds
( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
let z be Point of S; ::_thesis: for dv being Point of T holds
( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
let dv be Point of T; ::_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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
A2: now__::_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_&_dv_=_lim_((h_")_(#)_((f_/*_((h_*_z)_+_c))_-_(f_/*_c)))_)_)_&_ex_r_being_Real_st_
(_r_>_0_&_(_for_d_being_Real_holds_
(_not_d_>_0_or_ex_h_being_Real_st_
(_abs_h_<_d_&_h_<>_0_&_(h_*_z)_+_x0_in_N_&_not_||.(((h_")_*_((f_/._((h_*_z)_+_x0))_-_(f_/._x0)))_-_dv).||_<_r_)_)_)_)_implies_for_e_being_Real_st_e_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_h_being_Real_st_abs_h_<_d_&_h_<>_0_&_(h_*_z)_+_x0_in_N_holds_
||.(((h_")_*_((f_/._((h_*_z)_+_x0))_-_(f_/._x0)))_-_dv).||_<_e_)_)_)
reconsider c = NAT --> x0 as sequence of S ;
assume A3: 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ; ::_thesis: ( ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex h being Real st
( abs h < d & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) ) ) ) implies for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
now__::_thesis:_for_x_being_set_st_x_in_{x0}_holds_
x_in_rng_c
let x be set ; ::_thesis: ( x in {x0} implies x in rng c )
assume x in {x0} ; ::_thesis: x in rng c
then x = x0 by TARSKI:def_1;
then x = c . 1 by FUNCOP_1:7;
hence x in rng c by NFCONT_1:6; ::_thesis: verum
end;
then A4: {x0} c= rng c by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_rng_c_holds_
x_in_{x0}
let x be set ; ::_thesis: ( x in rng c implies x in {x0} )
assume x in rng c ; ::_thesis: x in {x0}
then ex n being Element of NAT st x = c . n by NFCONT_1:6;
then x = x0 by FUNCOP_1:7;
hence x in {x0} by TARSKI:def_1; ::_thesis: verum
end;
then rng c c= {x0} by TARSKI:def_3;
then A5: rng c = {x0} by A4, XBOOLE_0:def_10;
assume ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex h being Real st
( abs h < d & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) ) ) ) ; ::_thesis: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) )
then consider r being Real such that
A6: r > 0 and
A7: for d being Real st d > 0 holds
ex h being Real st
( abs h < d & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) ;
defpred S1[ Nat, real number ] means ex rr being Real st
( rr = $2 & abs rr < 1 / ($1 + 1) & rr <> 0 & (rr * z) + x0 in N & not ||.(((rr ") * ((f /. ((rr * z) + x0)) - (f /. x0))) - dv).|| < r );
A8: for n being Element of NAT ex h being Real st S1[n,h]
proof
let n be Element of NAT ; ::_thesis: ex h being Real st S1[n,h]
0 <= n by NAT_1:2;
then 0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def_9;
then ex h being Real st
( abs h < 1 / (n + 1) & h <> 0 & (h * z) + x0 in N & not ||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r ) by A7;
hence ex h being Real st S1[n,h] ; ::_thesis: verum
end;
consider h being Real_Sequence such that
A9: for n being Element of NAT holds S1[n,h . n] from FUNCT_2:sch_3(A8);
A10: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((h_._m)_-_0)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < p )
assume A11: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < p
consider n being Element of NAT such that
A12: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by A12, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A11, XREAL_1:76;
then A13: 1 / (n + 1) < p by XCMPLX_1:216;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((h . m) - 0) < p )
assume n <= m ; ::_thesis: abs ((h . m) - 0) < p
then A14: n + 1 <= m + 1 by XREAL_1:6;
A15: S1[m,h . m] by A9;
0 <= n by NAT_1:2;
then 1 / (m + 1) <= 1 / (n + 1) by A14, XREAL_1:118;
then abs ((h . m) - 0) < 1 / (n + 1) by A15, XXREAL_0:2;
hence abs ((h . m) - 0) < p by A13, XXREAL_0:2; ::_thesis: verum
end;
then A16: h is convergent by SEQ_2:def_6;
then A17: lim h = 0 by A10, SEQ_2:def_7;
for n being Element of NAT holds h . n <> 0
proof
let n be Element of NAT ; ::_thesis: h . n <> 0
S1[n,h . n] by A9;
hence h . n <> 0 ; ::_thesis: verum
end;
then h is non-zero by SEQ_1:5;
then reconsider h = h as non-zero 0 -convergent Real_Sequence by A16, A17, FDIFF_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_rng_((h_*_z)_+_c)_holds_
x_in_N
let x be set ; ::_thesis: ( x in rng ((h * z) + c) implies x in N )
assume x in rng ((h * z) + c) ; ::_thesis: x in N
then consider n being Element of NAT such that
A18: x = ((h * z) + c) . n by NFCONT_1:6;
A19: x = ((h * z) . n) + (c . n) by A18, NORMSP_1:def_2
.= ((h . n) * z) + (c . n) by NDIFF_1:def_3
.= ((h . n) * z) + x0 by FUNCOP_1:7 ;
S1[n,h . n] by A9;
hence x in N by A19; ::_thesis: verum
end;
then A20: rng ((h * z) + c) c= N by TARSKI:def_3;
then ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A3, A5;
then consider n being Element of NAT such that
A21: for m being Element of NAT st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r by A6, NORMSP_1:def_7;
x0 in N by NFCONT_1:4;
then A22: rng c c= dom f by A1, A5, ZFMISC_1:31;
A23: S1[n,h . n] by A9;
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - dv).|| = ||.((((h ") . n) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - dv).|| by NDIFF_1:def_2
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) - (f /* c)) . n)) - dv).|| by VALUED_1:10
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) . n) - ((f /* c) . n))) - dv).|| by NORMSP_1:def_3
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) . n) - (f /. (c . n)))) - dv).|| by A22, FUNCT_2:109
.= ||.((((h . n) ") * (((f /* ((h * z) + c)) . n) - (f /. x0))) - dv).|| by FUNCOP_1:7
.= ||.((((h . n) ") * ((f /. (((h * z) + c) . n)) - (f /. x0))) - dv).|| by A1, A20, FUNCT_2:109, XBOOLE_1:1
.= ||.((((h . n) ") * ((f /. (((h * z) . n) + (c . n))) - (f /. x0))) - dv).|| by NORMSP_1:def_2
.= ||.((((h . n) ") * ((f /. (((h * z) . n) + x0)) - (f /. x0))) - dv).|| by FUNCOP_1:7
.= ||.((((h . n) ") * ((f /. (((h . n) * z) + x0)) - (f /. x0))) - dv).|| by NDIFF_1:def_3 ;
hence for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) by A21, A23; ::_thesis: verum
end;
now__::_thesis:_(_(_for_e_being_Real_st_e_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_h_being_Real_st_abs_h_<_d_&_h_<>_0_&_(h_*_z)_+_x0_in_N_holds_
||.(((h_")_*_((f_/._((h_*_z)_+_x0))_-_(f_/._x0)))_-_dv).||_<_e_)_)_)_implies_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_&_dv_=_lim_((h_")_(#)_((f_/*_((h_*_z)_+_c))_-_(f_/*_c)))_)_)
assume A24: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ; ::_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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
now__::_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)))_=_dv_)
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))) = dv )
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))) = dv ) )
assume that
A25: rng c = {x0} and
A26: rng ((h * z) + c) c= N ; ::_thesis: ( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = dv )
A27: ( h is convergent & lim h = 0 ) ;
x0 in N by NFCONT_1:4;
then A28: rng c c= dom f by A1, A25, ZFMISC_1:31;
A29: for n being Element of NAT holds c . n = x0
proof
let n be Element of NAT ; ::_thesis: c . n = x0
c . n in rng c by NFCONT_1:6;
hence c . n = x0 by A25, TARSKI:def_1; ::_thesis: verum
end;
A30: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((((h_")_(#)_((f_/*_((h_*_z)_+_c))_-_(f_/*_c)))_._m)_-_dv).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r )
assume r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r
then consider d being Real such that
A31: d > 0 and
A32: for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r by A24;
consider n being Element of NAT such that
A33: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < d by A27, A31, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r
thus for m being Element of NAT st n <= m holds
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r )
A34: h . m <> 0 by SEQ_1:5;
assume n <= m ; ::_thesis: ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r
then A35: abs ((h . m) - 0) < d by A33;
((h * z) + c) . m in rng ((h * z) + c) by NFCONT_1:6;
then ((h * z) + c) . m in N by A26;
then ((h * z) . m) + (c . m) in N by NORMSP_1:def_2;
then ((h . m) * z) + (c . m) in N by NDIFF_1:def_3;
then A36: ((h . m) * z) + x0 in N by A29;
||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| = ||.((((h ") . m) * (((f /* ((h * z) + c)) - (f /* c)) . m)) - dv).|| by NDIFF_1:def_2
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) - (f /* c)) . m)) - dv).|| by VALUED_1:10
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) . m) - ((f /* c) . m))) - dv).|| by NORMSP_1:def_3
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) . m) - (f /. (c . m)))) - dv).|| by A28, FUNCT_2:109
.= ||.((((h . m) ") * (((f /* ((h * z) + c)) . m) - (f /. x0))) - dv).|| by A29
.= ||.((((h . m) ") * ((f /. (((h * z) + c) . m)) - (f /. x0))) - dv).|| by A1, A26, FUNCT_2:109, XBOOLE_1:1
.= ||.((((h . m) ") * ((f /. (((h * z) . m) + (c . m))) - (f /. x0))) - dv).|| by NORMSP_1:def_2
.= ||.((((h . m) ") * ((f /. (((h * z) . m) + x0)) - (f /. x0))) - dv).|| by A29
.= ||.((((h . m) ") * ((f /. (((h . m) * z) + x0)) - (f /. x0))) - dv).|| by NDIFF_1:def_3 ;
hence ||.((((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r by A32, A35, A34, A36; ::_thesis: verum
end;
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))) = dv
hence lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) = dv by A30, NORMSP_1:def_7; ::_thesis: verum
end;
hence 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ; ::_thesis: verum
end;
hence ( ( 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) by A2; ::_thesis: verum
end;
definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0, z be Point of S;
predf is_Gateaux_differentiable_in x0,z means :Def3: :: NDIFF_2:def 3
ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) );
end;
:: deftheorem Def3 defines is_Gateaux_differentiable_in NDIFF_2:def_3_:_
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) );
theorem Th4: :: NDIFF_2:4
( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )
proof
thus for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) ::_thesis: ( ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )
proof
let X be RealNormSpace; ::_thesis: for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y )
let x, y be Point of X; ::_thesis: ( ||.(x - y).|| > 0 iff x <> y )
( 0 < ||.(x - y).|| implies x - y <> 0. X ) by NORMSP_0:def_6;
hence ( 0 < ||.(x - y).|| implies x <> y ) by RLVECT_1:15; ::_thesis: ( x <> y implies ||.(x - y).|| > 0 )
now__::_thesis:_(_x_<>_y_implies_0_<_||.(x_-_y).||_)
assume x <> y ; ::_thesis: 0 < ||.(x - y).||
then 0 <> ||.(x - y).|| by NORMSP_1:11;
hence 0 < ||.(x - y).|| by NORMSP_1:4; ::_thesis: verum
end;
hence ( x <> y implies ||.(x - y).|| > 0 ) ; ::_thesis: verum
end;
thus for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ::_thesis: ( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )
proof
let X be RealNormSpace; ::_thesis: for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||
let x, y be Point of X; ::_thesis: ||.(x - y).|| = ||.(y - x).||
thus ||.(x - y).|| = ||.(- (x - y)).|| by NORMSP_1:2
.= ||.(y - x).|| by RLVECT_1:33 ; ::_thesis: verum
end;
A1: for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
proof
let X be RealNormSpace; ::_thesis: for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; ::_thesis: for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; ::_thesis: ( e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 implies ||.(x - y).|| < e )
assume e > 0 ; ::_thesis: ( not ||.(x - z).|| < e / 2 or not ||.(z - y).|| < e / 2 or ||.(x - y).|| < e )
assume ( ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 ) ; ::_thesis: ||.(x - y).|| < e
then ||.(x - z).|| + ||.(z - y).|| < (e / 2) + (e / 2) by XREAL_1:8;
then ||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||) < (||.(x - z).|| + ||.(z - y).||) + e by NORMSP_1:10, XREAL_1:8;
then (||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) < (e + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) by XREAL_1:8;
hence ||.(x - y).|| < e ; ::_thesis: verum
end;
A2: for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
proof
let X be RealNormSpace; ::_thesis: for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; ::_thesis: for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; ::_thesis: ( e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 implies ||.(x - y).|| < e )
assume A3: e > 0 ; ::_thesis: ( not ||.(x - z).|| < e / 2 or not ||.(y - z).|| < e / 2 or ||.(x - y).|| < e )
assume that
A4: ||.(x - z).|| < e / 2 and
A5: ||.(y - z).|| < e / 2 ; ::_thesis: ||.(x - y).|| < e
||.(- (y - z)).|| < e / 2 by A5, NORMSP_1:2;
then ||.(z - y).|| < e / 2 by RLVECT_1:33;
hence ||.(x - y).|| < e by A1, A3, A4; ::_thesis: verum
end;
A6: for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
proof
let X be RealNormSpace; ::_thesis: for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
let x be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds
||.x.|| < e ) implies x = 0. X )
assume A7: for e being Real st e > 0 holds
||.x.|| < e ; ::_thesis: x = 0. X
now__::_thesis:_not_x_<>_0._X
assume x <> 0. X ; ::_thesis: contradiction
then 0 <> ||.x.|| by NORMSP_0:def_5;
then 0 < ||.x.|| by NORMSP_1:4;
hence contradiction by A7; ::_thesis: verum
end;
hence x = 0. X ; ::_thesis: verum
end;
for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
proof
let X be RealNormSpace; ::_thesis: for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
let x, y be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds
||.(x - y).|| < e ) implies x = y )
assume for e being Real st e > 0 holds
||.(x - y).|| < e ; ::_thesis: x = y
then x - y = 0. X by A6;
hence x = y by RLVECT_1:21; ::_thesis: verum
end;
hence ( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) ) by A1, A2, A6, NORMSP_1:6; ::_thesis: verum
end;
definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0, z be Point of S;
assume A1: f is_Gateaux_differentiable_in x0,z ;
func Gateaux_diff (f,x0,z) -> Point of T means :Def4: :: NDIFF_2:def 4
ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - it).|| < e ) ) ) );
existence
ex b1 being Point of T ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b1).|| < e ) ) ) )
proof
ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) by A1, Def3;
hence ex b1 being Point of T ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b1).|| < e ) ) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of T st ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b1).|| < e ) ) ) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b2).|| < e ) ) ) ) holds
b1 = b2
proof
let dv1, dv2 be Point of T; ::_thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) ) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) ) ) implies dv1 = dv2 )
assume that
A2: ex N1 being Neighbourhood of x0 st
( N1 c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N1 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) ) ) and
A3: ex N2 being Neighbourhood of x0 st
( N2 c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N2 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) ) ) ; ::_thesis: dv1 = dv2
consider N2 being Neighbourhood of x0 such that
N2 c= dom f and
A4: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N2 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e ) ) by A3;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A5: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N1 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e ) ) by A2;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
||.(dv1_-_dv2).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ||.(dv1 - dv2).|| < e )
assume A6: e > 0 ; ::_thesis: ||.(dv1 - dv2).|| < e
A7: 0 < e / 2 by A6, XREAL_1:215;
then consider d1 being Real such that
A8: d1 > 0 and
A9: for h being Real st abs h < d1 & h <> 0 & (h * z) + x0 in N1 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e / 2 by A5;
consider d2 being Real such that
A10: d2 > 0 and
A11: for h being Real st abs h < d2 & h <> 0 & (h * z) + x0 in N2 holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e / 2 by A4, A7;
ex h being Real st
( h <> 0 & abs h < d1 & abs h < d2 & (h * z) + x0 in N1 & (h * z) + x0 in N2 )
proof
set d3 = min (d1,d2);
consider N0 being Neighbourhood of x0 such that
A12: ( N0 c= N1 & N0 c= N2 ) by NDIFF_1:1;
consider g being Real such that
A13: 0 < g and
A14: { y where y is Point of S : ||.(y - x0).|| < g } c= N0 by NFCONT_1:def_1;
consider n0 being Element of NAT such that
A15: ||.z.|| / g < n0 by SEQ_4:3;
set n1 = n0 + 1;
set h = min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2));
take min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) ; ::_thesis: ( min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) <> 0 & abs (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) < d1 & abs (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) < d2 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 )
A16: min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) <= (min (d1,d2)) / 2 by XXREAL_0:17;
A17: 0 < min (d1,d2) by A8, A10, XXREAL_0:15;
then A18: 0 < (min (d1,d2)) / 2 by XREAL_1:215;
A19: 0 <= n0 by NAT_1:2;
then 0 < 1 * ((1 + (n0 + 1)) ") ;
then A20: 0 < 1 / (1 + (n0 + 1)) by XCMPLX_0:def_9;
hence min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) <> 0 by A18, XXREAL_0:15; ::_thesis: ( abs (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) < d1 & abs (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) < d2 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 )
A21: 0 < min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) by A18, A20, XXREAL_0:15;
n0 <= n0 + 1 by NAT_1:11;
then ||.z.|| / g < n0 + 1 by A15, XXREAL_0:2;
then (||.z.|| / g) * g < (n0 + 1) * g by A13, XREAL_1:68;
then ||.z.|| < (n0 + 1) * g by A13, XCMPLX_1:87;
then A22: ||.z.|| / (n0 + 1) < g by A19, XREAL_1:83;
A23: ||.((((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0) - x0).|| = ||.(((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + (x0 - x0)).|| by RLVECT_1:def_3
.= ||.(((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + (0. S)).|| by RLVECT_1:15
.= ||.((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z).|| by RLVECT_1:4
.= (abs (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)))) * ||.z.|| by NORMSP_1:def_1
.= (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * ||.z.|| by A21, ABSVALUE:def_1 ;
A24: (min (d1,d2)) / 2 < min (d1,d2) by A17, XREAL_1:216;
min (d1,d2) <= d2 by XXREAL_0:17;
then (min (d1,d2)) / 2 < d2 by A24, XXREAL_0:2;
then A25: min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) < d2 by A16, XXREAL_0:2;
min (d1,d2) <= d1 by XXREAL_0:17;
then (min (d1,d2)) / 2 < d1 by A24, XXREAL_0:2;
then min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2)) < d1 by A16, XXREAL_0:2;
hence ( abs (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) < d1 & abs (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) < d2 ) by A21, A25, ABSVALUE:def_1; ::_thesis: ( ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 )
0 <= ||.z.|| by NORMSP_1:4;
then A26: (min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * ||.z.|| <= (1 / ((n0 + 1) + 1)) * ||.z.|| by XREAL_1:64, XXREAL_0:17;
( 0 <= ||.z.|| & n0 + 1 <= 1 + (n0 + 1) ) by NAT_1:12, NORMSP_1:4;
then A27: ||.z.|| / (1 + (n0 + 1)) <= ||.z.|| / (n0 + 1) by A19, XREAL_1:118;
(1 / (1 + (n0 + 1))) * ||.z.|| = ||.z.|| / (1 + (n0 + 1)) by XCMPLX_1:99;
then (1 / (1 + (n0 + 1))) * ||.z.|| < g by A22, A27, XXREAL_0:2;
then ||.((((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0) - x0).|| < g by A23, A26, XXREAL_0:2;
then ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in { y where y is Point of S : ||.(y - x0).|| < g } ;
then ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N0 by A14;
hence ( ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N1 & ((min ((1 / ((n0 + 1) + 1)),((min (d1,d2)) / 2))) * z) + x0 in N2 ) by A12; ::_thesis: verum
end;
then consider h being Real such that
A28: abs h < d1 and
A29: abs h < d2 and
A30: h <> 0 and
A31: (h * z) + x0 in N1 and
A32: (h * z) + x0 in N2 ;
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e / 2 by A9, A28, A30, A31;
then A33: ||.(dv1 - ((h ") * ((f /. ((h * z) + x0)) - (f /. x0)))).|| < e / 2 by Th4;
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e / 2 by A11, A29, A30, A32;
hence ||.(dv1 - dv2).|| < e by A6, A33, Th4; ::_thesis: verum
end;
hence dv1 = dv2 by Th4; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def_4_:_
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0, z being Point of S st f is_Gateaux_differentiable_in x0,z holds
for b6 being Point of T holds
( b6 = Gateaux_diff (f,x0,z) iff ex N being Neighbourhood of x0 st
( N c= dom f & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b6).|| < e ) ) ) ) );
theorem :: NDIFF_2:5
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
let f be PartFunc of S,T; ::_thesis: for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
let x0, z be Point of S; ::_thesis: ( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
A1: now__::_thesis:_(_ex_N_being_Neighbourhood_of_x0_st_
(_N_c=_dom_f_&_ex_dv_being_Point_of_T_st_
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_&_dv_=_lim_((h_")_(#)_((f_/*_((h_*_z)_+_c))_-_(f_/*_c)))_)_)_implies_f_is_Gateaux_differentiable_in_x0,z_)
assume ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ; ::_thesis: f is_Gateaux_differentiable_in x0,z
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ;
consider dv being Point of T such that
A4: 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A3;
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) by A2, A4, Th3;
hence f is_Gateaux_differentiable_in x0,z by A2, Def3; ::_thesis: verum
end;
now__::_thesis:_(_f_is_Gateaux_differentiable_in_x0,z_implies_ex_N_being_Neighbourhood_of_x0_st_
(_N_c=_dom_f_&_ex_dv_being_Point_of_T_st_
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_&_dv_=_lim_((h_")_(#)_((f_/*_((h_*_z)_+_c))_-_(f_/*_c)))_)_)_)
assume f is_Gateaux_differentiable_in x0,z ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) )
then consider N being Neighbourhood of x0 such that
A5: N c= dom f and
A6: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - (Gateaux_diff (f,x0,z))).|| < e ) ) by Def4;
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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A5, A6, Th3;
hence ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) by A5; ::_thesis: verum
end;
hence ( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) by A1; ::_thesis: verum
end;
theorem :: NDIFF_2:6
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
proof
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
for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_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
for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_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 for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) ) )
assume f is_differentiable_in x0 ; ::_thesis: for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_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: 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 Th1;
let z be Point of S; ::_thesis: ( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
A3: 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 A2;
then A4: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - ((diff (f,x0)) . z)).|| < e ) ) by A1, Th3;
hence f is_Gateaux_differentiable_in x0,z by A1, Def3; ::_thesis: ( Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
hence Gateaux_diff (f,x0,z) = (diff (f,x0)) . z by A1, A4, Def4; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
hence ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) by A1, A3; ::_thesis: verum
end;
theorem Th7: :: NDIFF_2:7
for S, T being non trivial RealNormSpace
for R being RestFunc of S,T st R /. (0. S) = 0. T holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for R being RestFunc of S,T st R /. (0. S) = 0. T holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
let R be RestFunc of S,T; ::_thesis: ( R /. (0. S) = 0. T implies for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) ) )
assume A1: R /. (0. S) = 0. T ; ::_thesis: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
let e be Real; ::_thesis: ( e > 0 implies ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) ) )
assume A2: e > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
R is total by NDIFF_1:def_5;
then consider d being Real such that
A3: d > 0 and
A4: for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < e by A2, NDIFF_1:23;
take d ; ::_thesis: ( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
now__::_thesis:_for_h_being_Point_of_S_st_||.h.||_<_d_holds_
||.(R_/._h).||_<=_e_*_||.h.||
let h be Point of S; ::_thesis: ( ||.h.|| < d implies ||.(R /. h).|| <= e * ||.h.|| )
assume A5: ||.h.|| < d ; ::_thesis: ||.(R /. h).|| <= e * ||.h.||
now__::_thesis:_(_(_h_<>_0._S_&_||.(R_/._h).||_<=_e_*_||.h.||_)_or_(_h_=_0._S_&_||.(R_/._h).||_<=_e_*_||.h.||_)_)
percases ( h <> 0. S or h = 0. S ) ;
caseA6: h <> 0. S ; ::_thesis: ||.(R /. h).|| <= e * ||.h.||
then ( 0 <= ||.h.|| & (||.h.|| ") * ||.(R /. h).|| <= e ) by A4, A5, NORMSP_1:4;
then ||.h.|| * ((||.h.|| ") * ||.(R /. h).||) <= ||.h.|| * e by XREAL_1:64;
then A7: (||.h.|| * (||.h.|| ")) * ||.(R /. h).|| <= e * ||.h.|| ;
||.h.|| <> 0 by A6, NORMSP_0:def_5;
then 1 * ||.(R /. h).|| <= e * ||.h.|| by A7, XCMPLX_0:def_7;
hence ||.(R /. h).|| <= e * ||.h.|| ; ::_thesis: verum
end;
caseA8: h = 0. S ; ::_thesis: ||.(R /. h).|| <= e * ||.h.||
0 <= ||.h.|| by NORMSP_1:4;
then 0 * ||.h.|| <= e * ||.h.|| by A2;
hence ||.(R /. h).|| <= e * ||.h.|| by A1, A8, NORMSP_0:def_6; ::_thesis: verum
end;
end;
end;
hence ||.(R /. h).|| <= e * ||.h.|| ; ::_thesis: verum
end;
hence ( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) ) by A3; ::_thesis: verum
end;
theorem :: NDIFF_2:8
for T, S, U being non trivial RealNormSpace
for R being RestFunc of T,U st R /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R * L is RestFunc of S,U
proof
let T, S, U be non trivial RealNormSpace; ::_thesis: for R being RestFunc of T,U st R /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R * L is RestFunc of S,U
let R be RestFunc of T,U; ::_thesis: ( R /. (0. T) = 0. U implies for L being Lipschitzian LinearOperator of S,T holds R * L is RestFunc of S,U )
assume A1: R /. (0. T) = 0. U ; ::_thesis: for L being Lipschitzian LinearOperator of S,T holds R * L is RestFunc of S,U
let L be Lipschitzian LinearOperator of S,T; ::_thesis: R * L is RestFunc of S,U
consider K being Real such that
A2: 0 <= K and
A3: for h being Point of S holds ||.(L . h).|| <= K * ||.h.|| by LOPBAN_1:def_8;
A4: dom L = the carrier of S by FUNCT_2:def_1;
R is total by NDIFF_1:def_5;
then dom R = the carrier of T by PARTFUN1:def_2;
then A5: rng L c= dom R ;
A6: 0 + K < 1 + K by XREAL_1:8;
A7: now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_d1_being_Real_st_
(_d1_>_0_&_(_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_d1_holds_
(||.h.||_")_*_||.((R_*_L)_/._h).||_<_e_)_)
let e be Real; ::_thesis: ( e > 0 implies ex d1 being Real st
( d1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d1 holds
(||.h.|| ") * ||.((R * L) /. h).|| < e ) ) )
assume e > 0 ; ::_thesis: ex d1 being Real st
( d1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d1 holds
(||.h.|| ") * ||.((R * L) /. h).|| < e ) )
then A8: 0 / (1 + K) < e / (1 + K) by A2, XREAL_1:74;
set e1 = e / (1 + K);
consider d being Real such that
A9: 0 < d and
A10: for h being Point of T st ||.h.|| < d holds
||.(R /. h).|| <= (e / (1 + K)) * ||.h.|| by A1, A8, Th7;
set d1 = d / (1 + K);
A11: now__::_thesis:_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_d_/_(1_+_K)_holds_
(||.h.||_")_*_||.((R_*_L)_/._h).||_<_e
let h be Point of S; ::_thesis: ( h <> 0. S & ||.h.|| < d / (1 + K) implies (||.h.|| ") * ||.((R * L) /. h).|| < e )
assume that
A12: h <> 0. S and
A13: ||.h.|| < d / (1 + K) ; ::_thesis: (||.h.|| ") * ||.((R * L) /. h).|| < e
A14: ||.(L . h).|| <= K * ||.h.|| by A3;
A15: ||.h.|| <> 0 by A12, NORMSP_0:def_5;
then A16: ||.h.|| > 0 by NORMSP_1:4;
then K * ||.h.|| < (K + 1) * ||.h.|| by A6, XREAL_1:68;
then A17: ||.(L . h).|| < (K + 1) * ||.h.|| by A14, XXREAL_0:2;
(K + 1) * ||.h.|| < (K + 1) * (d / (1 + K)) by A2, A13, XREAL_1:68;
then ||.(L . h).|| < (K + 1) * (d / (1 + K)) by A17, XXREAL_0:2;
then ||.(L . h).|| < d by A2, XCMPLX_1:87;
then A18: ||.(R /. (L . h)).|| <= (e / (1 + K)) * ||.(L . h).|| by A10;
A19: R /. (L . h) = R /. (L /. h)
.= (R * L) /. h by A4, A5, PARTFUN2:5 ;
(e / (1 + K)) * ||.(L . h).|| < (e / (1 + K)) * ((K + 1) * ||.h.||) by A8, A17, XREAL_1:68;
then ||.(R /. (L . h)).|| < (e / (1 + K)) * ((K + 1) * ||.h.||) by A18, XXREAL_0:2;
then (||.h.|| ") * ||.((R * L) /. h).|| < (||.h.|| ") * (((e / (1 + K)) * (K + 1)) * ||.h.||) by A19, A16, XREAL_1:68;
then (||.h.|| ") * ||.((R * L) /. h).|| < ((||.h.|| * (||.h.|| ")) * (e / (1 + K))) * (K + 1) ;
then (||.h.|| ") * ||.((R * L) /. h).|| < (1 * (e / (1 + K))) * (K + 1) by A15, XCMPLX_0:def_7;
hence (||.h.|| ") * ||.((R * L) /. h).|| < e by A2, XCMPLX_1:87; ::_thesis: verum
end;
0 / (1 + K) < d / (1 + K) by A2, A9, XREAL_1:74;
hence ex d1 being Real st
( d1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d1 holds
(||.h.|| ") * ||.((R * L) /. h).|| < e ) ) by A11; ::_thesis: verum
end;
dom (R * L) = dom L by A5, RELAT_1:27
.= the carrier of S by FUNCT_2:def_1 ;
then R * L is total by PARTFUN1:def_2;
hence R * L is RestFunc of S,U by A7, NDIFF_1:23; ::_thesis: verum
end;
theorem Th9: :: NDIFF_2:9
for S, T, U being non trivial RealNormSpace
for R being RestFunc of S,T
for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U
proof
let S, T, U be non trivial RealNormSpace; ::_thesis: for R being RestFunc of S,T
for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U
let R be RestFunc of S,T; ::_thesis: for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U
let L be Lipschitzian LinearOperator of T,U; ::_thesis: L * R is RestFunc of S,U
consider K being Real such that
A1: 0 <= K and
A2: for z being Point of T holds ||.(L . z).|| <= K * ||.z.|| by LOPBAN_1:def_8;
dom L = the carrier of T by FUNCT_2:def_1;
then A3: rng R c= dom L ;
A4: R is total by NDIFF_1:def_5;
then A5: dom R = the carrier of S by PARTFUN1:def_2;
A6: 0 + K < 1 + K by XREAL_1:8;
A7: now__::_thesis:_for_ee_being_Real_st_ee_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_d_holds_
(||.h.||_")_*_||.((L_*_R)_/._h).||_<_ee_)_)
let ee be Real; ::_thesis: ( ee > 0 implies ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((L * R) /. h).|| < ee ) ) )
assume A8: ee > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((L * R) /. h).|| < ee ) )
set e = ee / 2;
ee / 2 > 0 by A8, XREAL_1:215;
then A9: 0 / (1 + K) < (ee / 2) / (1 + K) by A1, XREAL_1:74;
set e1 = (ee / 2) / (1 + K);
R is total by NDIFF_1:def_5;
then consider d being Real such that
A10: 0 < d and
A11: for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A9, NDIFF_1:23;
A12: ee / 2 < ee by A8, XREAL_1:216;
now__::_thesis:_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_d_holds_
(||.h.||_")_*_||.((L_*_R)_/._h).||_<_ee
let h be Point of S; ::_thesis: ( h <> 0. S & ||.h.|| < d implies (||.h.|| ") * ||.((L * R) /. h).|| < ee )
assume that
A13: h <> 0. S and
A14: ||.h.|| < d ; ::_thesis: (||.h.|| ") * ||.((L * R) /. h).|| < ee
(||.h.|| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A11, A13, A14;
then (K + 1) * ((||.h.|| ") * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K)) by A1, XREAL_1:64;
then A15: (K + 1) * ((||.h.|| ") * ||.(R /. h).||) <= ee / 2 by A1, XCMPLX_1:87;
||.h.|| <> 0 by A13, NORMSP_0:def_5;
then A16: ||.h.|| > 0 by NORMSP_1:4;
0 <= ||.(R /. h).|| by NORMSP_1:4;
then A17: K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).|| by A6, XREAL_1:64;
||.(L . (R /. h)).|| <= K * ||.(R /. h).|| by A2;
then ||.(L . (R /. h)).|| <= (K + 1) * ||.(R /. h).|| by A17, XXREAL_0:2;
then (||.h.|| ") * ||.(L . (R /. h)).|| <= (||.h.|| ") * ((K + 1) * ||.(R /. h).||) by A16, XREAL_1:64;
then A18: (||.h.|| ") * ||.(L . (R /. h)).|| <= ee / 2 by A15, XXREAL_0:2;
L . (R /. h) = L /. (R /. h)
.= (L * R) /. h by A5, A3, PARTFUN2:5 ;
hence (||.h.|| ") * ||.((L * R) /. h).|| < ee by A12, A18, XXREAL_0:2; ::_thesis: verum
end;
hence ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((L * R) /. h).|| < ee ) ) by A10; ::_thesis: verum
end;
dom (L * R) = dom R by A3, RELAT_1:27
.= the carrier of S by A4, PARTFUN1:def_2 ;
then L * R is total by PARTFUN1:def_2;
hence L * R is RestFunc of S,U by A7, NDIFF_1:23; ::_thesis: verum
end;
theorem :: NDIFF_2:10
for S, T, U being non trivial RealNormSpace
for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
proof
let S, T, U be non trivial RealNormSpace; ::_thesis: for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
let R1 be RestFunc of S,T; ::_thesis: ( R1 /. (0. S) = 0. T implies for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U )
assume A1: R1 /. (0. S) = 0. T ; ::_thesis: for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
let R2 be RestFunc of T,U; ::_thesis: ( R2 /. (0. T) = 0. U implies R2 * R1 is RestFunc of S,U )
assume A2: R2 /. (0. T) = 0. U ; ::_thesis: R2 * R1 is RestFunc of S,U
R2 is total by NDIFF_1:def_5;
then dom R2 = the carrier of T by PARTFUN1:def_2;
then A3: rng R1 c= dom R2 ;
A4: R1 is total by NDIFF_1:def_5;
then A5: dom R1 = the carrier of S by PARTFUN1:def_2;
A6: now__::_thesis:_for_e0_being_Real_st_e0_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_d_holds_
(||.h.||_")_*_||.((R2_*_R1)_/._h).||_<_e0_)_)
consider d1 being Real such that
A7: 0 < d1 and
A8: for h being Point of S st ||.h.|| < d1 holds
||.(R1 /. h).|| <= 1 * ||.h.|| by A1, Th7;
let e0 be Real; ::_thesis: ( e0 > 0 implies ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) ) )
assume A9: e0 > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) )
set e = e0 / 2;
A10: e0 / 2 < e0 by A9, XREAL_1:216;
e0 / 2 > 0 by A9, XREAL_1:215;
then consider d2 being Real such that
A11: 0 < d2 and
A12: for z being Point of T st ||.z.|| < d2 holds
||.(R2 /. z).|| <= (e0 / 2) * ||.z.|| by A2, Th7;
set d = min (d1,d2);
A13: min (d1,d2) <= d2 by XXREAL_0:17;
A14: min (d1,d2) <= d1 by XXREAL_0:17;
A15: now__::_thesis:_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_min_(d1,d2)_holds_
(||.h.||_")_*_||.((R2_*_R1)_/._h).||_<_e0
let h be Point of S; ::_thesis: ( h <> 0. S & ||.h.|| < min (d1,d2) implies (||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 )
assume that
A16: h <> 0. S and
A17: ||.h.|| < min (d1,d2) ; ::_thesis: (||.h.|| ") * ||.((R2 * R1) /. h).|| < e0
||.h.|| < d1 by A14, A17, XXREAL_0:2;
then A18: ||.(R1 /. h).|| <= 1 * ||.h.|| by A8;
then ||.(R1 /. h).|| < min (d1,d2) by A17, XXREAL_0:2;
then ||.(R1 /. h).|| < d2 by A13, XXREAL_0:2;
then A19: ||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.(R1 /. h).|| by A12;
(e0 / 2) * ||.(R1 /. h).|| <= (e0 / 2) * ||.h.|| by A9, A18, XREAL_1:64;
then A20: ||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.h.|| by A19, XXREAL_0:2;
A21: ||.h.|| <> 0 by A16, NORMSP_0:def_5;
then ||.h.|| > 0 by NORMSP_1:4;
then (||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= (||.h.|| ") * ((e0 / 2) * ||.h.||) by A20, XREAL_1:64;
then (||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= ((||.h.|| ") * ||.h.||) * (e0 / 2) ;
then A22: (||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= 1 * (e0 / 2) by A21, XCMPLX_0:def_7;
R2 /. (R1 /. h) = (R2 * R1) /. h by A5, A3, PARTFUN2:5;
hence (||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 by A10, A22, XXREAL_0:2; ::_thesis: verum
end;
0 < min (d1,d2) by A11, A7, XXREAL_0:15;
hence ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) ) by A15; ::_thesis: verum
end;
dom (R2 * R1) = dom R1 by A3, RELAT_1:27
.= the carrier of S by A4, PARTFUN1:def_2 ;
then R2 * R1 is total by PARTFUN1:def_2;
hence R2 * R1 is RestFunc of S,U by A6, NDIFF_1:23; ::_thesis: verum
end;
theorem Th11: :: NDIFF_2:11
for S, T, U being non trivial RealNormSpace
for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U
proof
let S, T, U be non trivial RealNormSpace; ::_thesis: for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U
let R1 be RestFunc of S,T; ::_thesis: ( R1 /. (0. S) = 0. T implies for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U )
assume R1 /. (0. S) = 0. T ; ::_thesis: for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U
then consider d0 being Real such that
A1: 0 < d0 and
A2: for h being Point of S st ||.h.|| < d0 holds
||.(R1 /. h).|| <= 1 * ||.h.|| by Th7;
let R2 be RestFunc of T,U; ::_thesis: ( R2 /. (0. T) = 0. U implies for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U )
assume A3: R2 /. (0. T) = 0. U ; ::_thesis: for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U
let L be Lipschitzian LinearOperator of S,T; ::_thesis: R2 * (L + R1) is RestFunc of S,U
consider K being Real such that
A4: 0 <= K and
A5: for h being Point of S holds ||.(L . h).|| <= K * ||.h.|| by LOPBAN_1:def_8;
R2 is total by NDIFF_1:def_5;
then dom R2 = the carrier of T by PARTFUN1:def_2;
then A6: rng (L + R1) c= dom R2 ;
R1 is total by NDIFF_1:def_5;
then A7: L + R1 is total by VFUNCT_1:32;
then A8: dom (L + R1) = the carrier of S by PARTFUN1:def_2;
A9: now__::_thesis:_for_ee_being_Real_st_ee_>_0_holds_
ex_dd1_being_Real_st_
(_dd1_>_0_&_(_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_dd1_holds_
(||.h.||_")_*_||.((R2_*_(L_+_R1))_/._h).||_<_ee_)_)
let ee be Real; ::_thesis: ( ee > 0 implies ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) )
assume A10: ee > 0 ; ::_thesis: ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) )
set e = ee / 2;
A11: ee / 2 < ee by A10, XREAL_1:216;
set e1 = (ee / 2) / (1 + K);
ee / 2 > 0 by A10, XREAL_1:215;
then 0 / (1 + K) < (ee / 2) / (1 + K) by A4, XREAL_1:74;
then consider d being Real such that
A12: 0 < d and
A13: for z being Point of T st ||.z.|| < d holds
||.(R2 /. z).|| <= ((ee / 2) / (1 + K)) * ||.z.|| by A3, Th7;
set d1 = d / (1 + K);
set dd1 = min (d0,(d / (1 + K)));
A14: min (d0,(d / (1 + K))) <= d / (1 + K) by XXREAL_0:17;
A15: min (d0,(d / (1 + K))) <= d0 by XXREAL_0:17;
A16: now__::_thesis:_for_h_being_Point_of_S_st_h_<>_0._S_&_||.h.||_<_min_(d0,(d_/_(1_+_K)))_holds_
(||.h.||_")_*_||.((R2_*_(L_+_R1))_/._h).||_<_ee
let h be Point of S; ::_thesis: ( h <> 0. S & ||.h.|| < min (d0,(d / (1 + K))) implies (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee )
assume that
A17: h <> 0. S and
A18: ||.h.|| < min (d0,(d / (1 + K))) ; ::_thesis: (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee
||.h.|| < d0 by A15, A18, XXREAL_0:2;
then A19: ||.(R1 /. h).|| <= 1 * ||.h.|| by A2;
||.(L . h).|| <= K * ||.h.|| by A5;
then ( ||.((L . h) + (R1 /. h)).|| <= ||.(L . h).|| + ||.(R1 /. h).|| & ||.(L . h).|| + ||.(R1 /. h).|| <= (K * ||.h.||) + (1 * ||.h.||) ) by A19, NORMSP_1:def_1, XREAL_1:7;
then A20: ||.((L . h) + (R1 /. h)).|| <= (K + 1) * ||.h.|| by XXREAL_0:2;
||.h.|| < d / (1 + K) by A14, A18, XXREAL_0:2;
then (K + 1) * ||.h.|| < (K + 1) * (d / (1 + K)) by A4, XREAL_1:68;
then ||.((L . h) + (R1 /. h)).|| < (K + 1) * (d / (1 + K)) by A20, XXREAL_0:2;
then ||.((L . h) + (R1 /. h)).|| < d by A4, XCMPLX_1:87;
then A21: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| by A13;
((ee / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| <= ((ee / 2) / (1 + K)) * ((K + 1) * ||.h.||) by A4, A10, A20, XREAL_1:64;
then A22: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + K)) * ((K + 1) * ||.h.||) by A21, XXREAL_0:2;
A23: R2 /. ((L . h) + (R1 /. h)) = R2 /. ((L /. h) + (R1 /. h))
.= R2 /. ((L + R1) /. h) by A8, VFUNCT_1:def_1
.= (R2 * (L + R1)) /. h by A8, A6, PARTFUN2:5 ;
A24: ||.h.|| <> 0 by A17, NORMSP_0:def_5;
then ||.h.|| > 0 by NORMSP_1:4;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= (||.h.|| ") * ((((ee / 2) / (1 + K)) * (K + 1)) * ||.h.||) by A23, A22, XREAL_1:64;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= ((||.h.|| * (||.h.|| ")) * ((ee / 2) / (1 + K))) * (K + 1) ;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= (1 * ((ee / 2) / (1 + K))) * (K + 1) by A24, XCMPLX_0:def_7;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= ee / 2 by A4, XCMPLX_1:87;
hence (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee by A11, XXREAL_0:2; ::_thesis: verum
end;
0 / (1 + K) < d / (1 + K) by A4, A12, XREAL_1:74;
then 0 < min (d0,(d / (1 + K))) by A1, XXREAL_0:15;
hence ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) by A16; ::_thesis: verum
end;
dom (R2 * (L + R1)) = dom (L + R1) by A6, RELAT_1:27
.= the carrier of S by A7, PARTFUN1:def_2 ;
then R2 * (L + R1) is total by PARTFUN1:def_2;
hence R2 * (L + R1) is RestFunc of S,U by A9, NDIFF_1:23; ::_thesis: verum
end;
theorem Th12: :: NDIFF_2:12
for S, T, U being non trivial RealNormSpace
for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
proof
let S, T, U be non trivial RealNormSpace; ::_thesis: for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
let R1 be RestFunc of S,T; ::_thesis: ( R1 /. (0. S) = 0. T implies for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U )
assume A1: R1 /. (0. S) = 0. T ; ::_thesis: for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
let R2 be RestFunc of T,U; ::_thesis: ( R2 /. (0. T) = 0. U implies for L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U )
assume A2: R2 /. (0. T) = 0. U ; ::_thesis: for L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
let L1 be Lipschitzian LinearOperator of S,T; ::_thesis: for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
let L2 be Lipschitzian LinearOperator of T,U; ::_thesis: (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
A3: L2 * R1 is RestFunc of S,U by Th9;
R2 * (L1 + R1) is RestFunc of S,U by A1, A2, Th11;
hence (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U by A3, NDIFF_1:28; ::_thesis: verum
end;
theorem :: NDIFF_2:13
for S, T being non trivial RealNormSpace
for x0 being Point of S
for U being non trivial RealNormSpace
for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for x0 being Point of S
for U being non trivial RealNormSpace
for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )
let x0 be Point of S; ::_thesis: for U being non trivial RealNormSpace
for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )
let U be non trivial RealNormSpace; ::_thesis: for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )
let f1 be PartFunc of S,T; ::_thesis: ( f1 is_differentiable_in x0 implies for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) ) )
assume A1: f1 is_differentiable_in x0 ; ::_thesis: for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )
consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f1 and
A3: ex R1 being RestFunc of S,T st
( R1 /. (0. S) = 0. T & R1 is_continuous_in 0. S & ( for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = ((diff (f1,x0)) . (x - x0)) + (R1 /. (x - x0)) ) ) by A1, NDIFF_1:47;
let f2 be PartFunc of T,U; ::_thesis: ( f2 is_differentiable_in f1 /. x0 implies ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) ) )
assume f2 is_differentiable_in f1 /. x0 ; ::_thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )
then consider N2 being Neighbourhood of f1 /. x0 such that
A4: N2 c= dom f2 and
A5: ex R2 being RestFunc of T,U st
( R2 /. (0. T) = 0. U & R2 is_continuous_in 0. T & ( for y being Point of T st y in N2 holds
(f2 /. y) - (f2 /. (f1 /. x0)) = ((diff (f2,(f1 /. x0))) . (y - (f1 /. x0))) + (R2 /. (y - (f1 /. x0))) ) ) by NDIFF_1:47;
consider R2 being RestFunc of T,U such that
A6: R2 /. (0. T) = 0. U and
A7: for y being Point of T st y in N2 holds
(f2 /. y) - (f2 /. (f1 /. x0)) = ((diff (f2,(f1 /. x0))) . (y - (f1 /. x0))) + (R2 /. (y - (f1 /. x0))) by A5;
set L2 = modetrans ((diff (f2,(f1 /. x0))),T,U);
set L1 = modetrans ((diff (f1,x0)),S,T);
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 LB1 = diff (f1,x0) as Element of BoundedLinearOperators (S,T) ;
R_NormSpace_of_BoundedLinearOperators (T,U) = NORMSTR(# (BoundedLinearOperators (T,U)),(Zero_ ((BoundedLinearOperators (T,U)),(R_VectorSpace_of_LinearOperators (T,U)))),(Add_ ((BoundedLinearOperators (T,U)),(R_VectorSpace_of_LinearOperators (T,U)))),(Mult_ ((BoundedLinearOperators (T,U)),(R_VectorSpace_of_LinearOperators (T,U)))),(BoundedLinearOperatorsNorm (T,U)) #) by LOPBAN_1:def_14;
then reconsider LB2 = diff (f2,(f1 /. x0)) as Element of BoundedLinearOperators (T,U) ;
consider R1 being RestFunc of S,T such that
A8: R1 /. (0. S) = 0. T and
A9: for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = ((diff (f1,x0)) . (x - x0)) + (R1 /. (x - x0)) by A3;
f1 is_continuous_in x0 by A1, NDIFF_1:44;
then consider N3 being Neighbourhood of x0 such that
A10: f1 .: N3 c= N2 by NFCONT_1:10;
reconsider R0 = ((modetrans ((diff (f2,(f1 /. x0))),T,U)) * R1) + (R2 * ((modetrans ((diff (f1,x0)),S,T)) + R1)) as RestFunc of S,U by A8, A6, Th12;
consider N being Neighbourhood of x0 such that
A11: N c= N1 and
A12: N c= N3 by NDIFF_1:1;
A13: N c= dom (f2 * f1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N or x in dom (f2 * f1) )
assume A14: x in N ; ::_thesis: x in dom (f2 * f1)
then reconsider x9 = x as Point of S ;
A15: x in N1 by A11, A14;
then f1 . x9 in f1 .: N3 by A2, A12, A14, FUNCT_1:def_6;
then f1 . x9 in N2 by A10;
hence x in dom (f2 * f1) by A2, A4, A15, FUNCT_1:11; ::_thesis: verum
end;
A16: ( LB1 = modetrans (LB1,S,T) & LB2 = modetrans (LB2,T,U) ) by LOPBAN_1:def_11;
A17: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N_holds_
((f2_*_f1)_/._x)_-_((f2_*_f1)_/._x0)_=_(((diff_(f2,(f1_/._x0)))_*_(diff_(f1,x0)))_._(x_-_x0))_+_(R0_/._(x_-_x0))
let x be Point of S; ::_thesis: ( x in N implies ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (((diff (f2,(f1 /. x0))) * (diff (f1,x0))) . (x - x0)) + (R0 /. (x - x0)) )
assume A18: x in N ; ::_thesis: ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (((diff (f2,(f1 /. x0))) * (diff (f1,x0))) . (x - x0)) + (R0 /. (x - x0))
A19: (f1 /. x) - (f1 /. x0) = ((diff (f1,x0)) . (x - x0)) + (R1 /. (x - x0)) by A9, A11, A18;
x in N1 by A11, A18;
then f1 . x in f1 .: N3 by A2, A12, A18, FUNCT_1:def_6;
then A20: f1 . x in N2 by A10;
x in N1 by A11, A18;
then A21: f1 /. x in N2 by A2, A20, PARTFUN1:def_6;
dom (modetrans ((diff (f1,x0)),S,T)) = the carrier of S by FUNCT_2:def_1;
then A22: (modetrans ((diff (f2,(f1 /. x0))),T,U)) . ((modetrans ((diff (f1,x0)),S,T)) . (x - x0)) = ((diff (f2,(f1 /. x0))) * (diff (f1,x0))) . (x - x0) by FUNCT_1:13;
A23: x0 in N by NFCONT_1:4;
A24: R1 is total by NDIFF_1:def_5;
then A25: dom R1 = the carrier of S by PARTFUN1:def_2;
dom (modetrans ((diff (f2,(f1 /. x0))),T,U)) = the carrier of T by FUNCT_2:def_1;
then A26: rng R1 c= dom (modetrans ((diff (f2,(f1 /. x0))),T,U)) ;
then A27: dom ((modetrans ((diff (f2,(f1 /. x0))),T,U)) * R1) = dom R1 by RELAT_1:27
.= the carrier of S by A24, PARTFUN1:def_2 ;
A28: (modetrans ((diff (f1,x0)),S,T)) + R1 is total by A24, VFUNCT_1:32;
then A29: dom ((modetrans ((diff (f1,x0)),S,T)) + R1) = the carrier of S by PARTFUN1:def_2;
R2 is total by NDIFF_1:def_5;
then dom R2 = the carrier of T by PARTFUN1:def_2;
then A30: rng ((modetrans ((diff (f1,x0)),S,T)) + R1) c= dom R2 ;
then dom (R2 * ((modetrans ((diff (f1,x0)),S,T)) + R1)) = dom ((modetrans ((diff (f1,x0)),S,T)) + R1) by RELAT_1:27
.= the carrier of S by A28, PARTFUN1:def_2 ;
then A31: dom (((modetrans ((diff (f2,(f1 /. x0))),T,U)) * R1) + (R2 * ((modetrans ((diff (f1,x0)),S,T)) + R1))) = the carrier of S /\ the carrier of S by A27, VFUNCT_1:def_1
.= the carrier of S ;
A32: (modetrans ((diff (f2,(f1 /. x0))),T,U)) . (R1 /. (x - x0)) = (modetrans ((diff (f2,(f1 /. x0))),T,U)) /. (R1 /. (x - x0))
.= ((modetrans ((diff (f2,(f1 /. x0))),T,U)) * R1) /. (x - x0) by A25, A26, PARTFUN2:5 ;
A33: R2 /. (((modetrans ((diff (f1,x0)),S,T)) . (x - x0)) + (R1 /. (x - x0))) = R2 /. (((modetrans ((diff (f1,x0)),S,T)) /. (x - x0)) + (R1 /. (x - x0)))
.= R2 /. (((modetrans ((diff (f1,x0)),S,T)) + R1) /. (x - x0)) by A29, VFUNCT_1:def_1
.= (R2 * ((modetrans ((diff (f1,x0)),S,T)) + R1)) /. (x - x0) by A29, A30, PARTFUN2:5 ;
thus ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (f2 /. (f1 /. x)) - ((f2 * f1) /. x0) by A13, A18, PARTFUN2:3
.= (f2 /. (f1 /. x)) - (f2 /. (f1 /. x0)) by A13, A23, PARTFUN2:3
.= ((diff (f2,(f1 /. x0))) . ((f1 /. x) - (f1 /. x0))) + (R2 /. ((f1 /. x) - (f1 /. x0))) by A7, A21
.= (((modetrans ((diff (f2,(f1 /. x0))),T,U)) . ((modetrans ((diff (f1,x0)),S,T)) . (x - x0))) + ((modetrans ((diff (f2,(f1 /. x0))),T,U)) . (R1 /. (x - x0)))) + ((R2 * ((modetrans ((diff (f1,x0)),S,T)) + R1)) /. (x - x0)) by A16, A19, A33, VECTSP_1:def_20
.= ((modetrans ((diff (f2,(f1 /. x0))),T,U)) . ((modetrans ((diff (f1,x0)),S,T)) . (x - x0))) + ((((modetrans ((diff (f2,(f1 /. x0))),T,U)) * R1) /. (x - x0)) + ((R2 * ((modetrans ((diff (f1,x0)),S,T)) + R1)) /. (x - x0))) by A32, RLVECT_1:def_3
.= (((diff (f2,(f1 /. x0))) * (diff (f1,x0))) . (x - x0)) + (R0 /. (x - x0)) by A31, A22, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence f2 * f1 is_differentiable_in x0 by A13, NDIFF_1:def_6; ::_thesis: diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0))
hence diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) by A13, A17, NDIFF_1:def_7; ::_thesis: verum
end;