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