:: NDIFF_1 semantic presentation begin theorem Th1: :: NDIFF_1:1 for S being RealNormSpace for x0 being Point of S for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st ( N c= N1 & N c= N2 ) proof let S be RealNormSpace; ::_thesis: for x0 being Point of S for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st ( N c= N1 & N c= N2 ) let x0 be Point of S; ::_thesis: for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st ( N c= N1 & N c= N2 ) let N1, N2 be Neighbourhood of x0; ::_thesis: ex N being Neighbourhood of x0 st ( N c= N1 & N c= N2 ) consider g1 being Real such that A1: 0 < g1 and A2: { y where y is Point of S : ||.(y - x0).|| < g1 } c= N1 by NFCONT_1:def_1; consider g2 being Real such that A3: 0 < g2 and A4: { y where y is Point of S : ||.(y - x0).|| < g2 } c= N2 by NFCONT_1:def_1; set g = min (g1,g2); take { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; ::_thesis: ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K6( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N2 ) A5: min (g1,g2) <= g2 by XXREAL_0:17; A6: { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= { y where y is Point of S : ||.(y - x0).|| < g2 } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } or z in { y where y is Point of S : ||.(y - x0).|| < g2 } ) assume z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; ::_thesis: z in { y where y is Point of S : ||.(y - x0).|| < g2 } then consider y being Point of S such that A7: z = y and A8: ||.(y - x0).|| < min (g1,g2) ; ||.(y - x0).|| < g2 by A5, A8, XXREAL_0:2; hence z in { y where y is Point of S : ||.(y - x0).|| < g2 } by A7; ::_thesis: verum end; A9: min (g1,g2) <= g1 by XXREAL_0:17; A10: { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= { y where y is Point of S : ||.(y - x0).|| < g1 } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } or z in { y where y is Point of S : ||.(y - x0).|| < g1 } ) assume z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; ::_thesis: z in { y where y is Point of S : ||.(y - x0).|| < g1 } then consider y being Point of S such that A11: z = y and A12: ||.(y - x0).|| < min (g1,g2) ; ||.(y - x0).|| < g1 by A9, A12, XXREAL_0:2; hence z in { y where y is Point of S : ||.(y - x0).|| < g1 } by A11; ::_thesis: verum end; 0 < min (g1,g2) by A1, A3, XXREAL_0:15; hence ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K6( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N2 ) by A2, A4, A10, A6, NFCONT_1:3, XBOOLE_1:1; ::_thesis: verum end; theorem Th2: :: NDIFF_1:2 for S being RealNormSpace for X being Subset of S st X is open holds for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X proof let S be RealNormSpace; ::_thesis: for X being Subset of S st X is open holds for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X let X be Subset of S; ::_thesis: ( X is open implies for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X ) assume X is open ; ::_thesis: for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X then A1: X ` is closed by NFCONT_1:def_4; let r be Point of S; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X ) assume that A2: r in X and A3: for N being Neighbourhood of r holds not N c= X ; ::_thesis: contradiction defpred S1[ Element of NAT , Point of S] means ( $2 in { y where y is Point of S : ||.(y - r).|| < 1 / ($1 + 1) } & $2 in X ` ); A4: now__::_thesis:_for_g_being_Real_st_0_<_g_holds_ ex_s_being_Point_of_S_st_ (_s_in__{__y_where_y_is_Point_of_S_:_||.(y_-_r).||_<_g__}__&_s_in_X_`_) let g be Real; ::_thesis: ( 0 < g implies ex s being Point of S st ( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` ) ) assume A5: 0 < g ; ::_thesis: ex s being Point of S st ( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` ) set N = { y where y is Point of S : ||.(y - r).|| < g } ; { y where y is Point of S : ||.(y - r).|| < g } is Neighbourhood of r by A5, NFCONT_1:3; then not { y where y is Point of S : ||.(y - r).|| < g } c= X by A3; then consider x being set such that A6: x in { y where y is Point of S : ||.(y - r).|| < g } and A7: not x in X by TARSKI:def_3; consider s being Point of S such that A8: x = s and A9: ||.(s - r).|| < g by A6; take s = s; ::_thesis: ( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` ) thus s in { y where y is Point of S : ||.(y - r).|| < g } by A9; ::_thesis: s in X ` thus s in X ` by A7, A8, XBOOLE_0:def_5; ::_thesis: verum end; A10: for n being Element of NAT ex s being Point of S st S1[n,s] proof let n be Element of NAT ; ::_thesis: ex s being Point of S st S1[n,s] 0 <= n by NAT_1:2; then 0 < 1 * ((n + 1) ") ; then 0 < 1 / (n + 1) by XCMPLX_0:def_9; hence ex s being Point of S st S1[n,s] by A4; ::_thesis: verum end; consider s1 being sequence of S such that A11: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A10); A12: rng s1 c= X ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s1 or x in X ` ) assume x in rng s1 ; ::_thesis: x in X ` then consider y being set such that A13: y in dom s1 and A14: s1 . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A13; s1 . y in X ` by A11; hence x in X ` by A14; ::_thesis: verum end; A15: 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_ ||.((s1_._m)_-_r).||_<_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 ||.((s1 . m) - r).|| < p ) assume A16: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((s1 . m) - r).|| < p consider n being Element of NAT such that A17: p " < n by SEQ_4:3; (p ") + 0 < n + 1 by A17, XREAL_1:8; then 1 / (n + 1) < 1 / (p ") by A16, XREAL_1:76; then A18: 1 / (n + 1) < p by XCMPLX_1:216; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.((s1 . m) - r).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((s1 . m) - r).|| < p ) assume n <= m ; ::_thesis: ||.((s1 . m) - r).|| < p then A19: n + 1 <= m + 1 by XREAL_1:6; s1 . m in { y where y is Point of S : ||.(y - r).|| < 1 / (m + 1) } by A11; then A20: ex y being Point of S st ( s1 . m = y & ||.(y - r).|| < 1 / (m + 1) ) ; 0 <= n by NAT_1:2; then 1 / (m + 1) <= 1 / (n + 1) by A19, XREAL_1:118; then ||.((s1 . m) - r).|| < 1 / (n + 1) by A20, XXREAL_0:2; hence ||.((s1 . m) - r).|| < p by A18, XXREAL_0:2; ::_thesis: verum end; then A21: s1 is convergent by NORMSP_1:def_6; then lim s1 = r by A15, NORMSP_1:def_7; then r in X ` by A21, A12, A1, NFCONT_1:def_3; hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: NDIFF_1:3 for S being RealNormSpace for X being Subset of S st X is open holds for r being Point of S st r in X holds ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) proof let S be RealNormSpace; ::_thesis: for X being Subset of S st X is open holds for r being Point of S st r in X holds ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) let X be Subset of S; ::_thesis: ( X is open implies for r being Point of S st r in X holds ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) ) assume A1: X is open ; ::_thesis: for r being Point of S st r in X holds ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) let r be Point of S; ::_thesis: ( r in X implies ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) ) assume r in X ; ::_thesis: ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) then consider N being Neighbourhood of r such that A2: N c= X by A1, Th2; consider g being Real such that A3: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= N ) by NFCONT_1:def_1; take g ; ::_thesis: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) thus ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) by A2, A3, XBOOLE_1:1; ::_thesis: verum end; theorem Th4: :: NDIFF_1:4 for S being RealNormSpace for X being Subset of S st ( for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X ) holds X is open proof let S be RealNormSpace; ::_thesis: for X being Subset of S st ( for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X ) holds X is open let X be Subset of S; ::_thesis: ( ( for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X ) implies X is open ) assume that A1: for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X and A2: not X is open ; ::_thesis: contradiction not X ` is closed by A2, NFCONT_1:def_4; then consider s1 being sequence of S such that A3: rng s1 c= X ` and A4: s1 is convergent and A5: not lim s1 in X ` by NFCONT_1:def_3; consider N being Neighbourhood of lim s1 such that A6: N c= X by A1, A5, SUBSET_1:29; consider g being Real such that A7: 0 < g and A8: { y where y is Point of S : ||.(y - (lim s1)).|| < g } c= N by NFCONT_1:def_1; consider n being Element of NAT such that A9: for m being Element of NAT st n <= m holds ||.((s1 . m) - (lim s1)).|| < g by A4, A7, NORMSP_1:def_7; n in NAT ; then n in dom s1 by FUNCT_2:def_1; then A10: s1 . n in rng s1 by FUNCT_1:def_3; ||.((s1 . n) - (lim s1)).|| < g by A9; then s1 . n in { y where y is Point of S : ||.(y - (lim s1)).|| < g } ; then s1 . n in N by A8; hence contradiction by A3, A6, A10, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: NDIFF_1:5 for S being RealNormSpace for X being Subset of S holds ( ( for r being Point of S st r in X holds ex N being Neighbourhood of r st N c= X ) iff X is open ) by Th2, Th4; definition let X be set ; let S be ZeroStr ; let f be Function of X,S; redefine attr f is non-zero means :Def1: :: NDIFF_1:def 1 rng f c= NonZero S; compatibility ( f is non-zero iff rng f c= NonZero S ) proof thus ( f is non-zero implies rng f c= NonZero S ) ::_thesis: ( rng f c= NonZero S implies f is non-zero ) proof assume f is non-zero ; ::_thesis: rng f c= NonZero S then not 0. S in rng f by STRUCT_0:def_15; hence rng f c= NonZero S by ZFMISC_1:34; ::_thesis: verum end; assume A1: rng f c= NonZero S ; ::_thesis: f is non-zero assume 0. S in rng f ; :: according to STRUCT_0:def_15 ::_thesis: contradiction then not 0. S in {(0. S)} by A1, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; end; :: deftheorem Def1 defines non-zero NDIFF_1:def_1_:_ for X being set for S being ZeroStr for f being Function of X,S holds ( f is non-zero iff rng f c= NonZero S ); theorem Th6: :: NDIFF_1:6 for S being RealNormSpace for seq being sequence of S holds ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0. S ) proof let S be RealNormSpace; ::_thesis: for seq being sequence of S holds ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0. S ) let seq be sequence of S; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0. S ) thus ( seq is non-zero implies for x being set st x in NAT holds seq . x <> 0. S ) ::_thesis: ( ( for x being set st x in NAT holds seq . x <> 0. S ) implies seq is non-zero ) proof assume seq is non-zero ; ::_thesis: for x being set st x in NAT holds seq . x <> 0. S then A1: rng seq c= NonZero S by Def1; let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0. S ) assume x in NAT ; ::_thesis: seq . x <> 0. S then x in dom seq by FUNCT_2:def_1; then seq . x in rng seq by FUNCT_1:def_3; then not seq . x in {(0. S)} by A1, XBOOLE_0:def_5; hence seq . x <> 0. S by TARSKI:def_1; ::_thesis: verum end; assume A2: for x being set st x in NAT holds seq . x <> 0. S ; ::_thesis: seq is non-zero now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_ y_in_NonZero_S let y be set ; ::_thesis: ( y in rng seq implies y in NonZero S ) assume A3: y in rng seq ; ::_thesis: y in NonZero S then ex x being set st ( x in dom seq & seq . x = y ) by FUNCT_1:def_3; then y <> 0. S by A2; then not y in {(0. S)} by TARSKI:def_1; hence y in NonZero S by A3, XBOOLE_0:def_5; ::_thesis: verum end; then rng seq c= NonZero S by TARSKI:def_3; hence seq is non-zero by Def1; ::_thesis: verum end; theorem Th7: :: NDIFF_1:7 for S being RealNormSpace for seq being sequence of S holds ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. S ) proof let S be RealNormSpace; ::_thesis: for seq being sequence of S holds ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. S ) let seq be sequence of S; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. S ) thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0. S ) by Th6; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. S ) implies seq is non-zero ) assume for n being Element of NAT holds seq . n <> 0. S ; ::_thesis: seq is non-zero then for x being set st x in NAT holds seq . x <> 0. S ; hence seq is non-zero by Th6; ::_thesis: verum end; definition let RNS be RealLinearSpace; let S be sequence of RNS; let a be Real_Sequence; funca (#) S -> sequence of RNS means :Def2: :: NDIFF_1:def 2 for n being Element of NAT holds it . n = (a . n) * (S . n); existence ex b1 being sequence of RNS st for n being Element of NAT holds b1 . n = (a . n) * (S . n) proof deffunc H1( Element of NAT ) -> Element of the carrier of RNS = (a . $1) * (S . $1); thus ex S being sequence of RNS st for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (a . n) * (S . n) ) & ( for n being Element of NAT holds b2 . n = (a . n) * (S . n) ) holds b1 = b2 proof let S1, S2 be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (a . n) * (S . n) ) & ( for n being Element of NAT holds S2 . n = (a . n) * (S . n) ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (a . n) * (S . n) and A2: for n being Element of NAT holds S2 . n = (a . n) * (S . n) ; ::_thesis: S1 = S2 for n being Element of NAT holds S1 . n = S2 . n proof let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (a . n) * (S . n) by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines (#) NDIFF_1:def_2_:_ for RNS being RealLinearSpace for S being sequence of RNS for a being Real_Sequence for b4 being sequence of RNS holds ( b4 = a (#) S iff for n being Element of NAT holds b4 . n = (a . n) * (S . n) ); definition let RNS be RealLinearSpace; let z be Point of RNS; let a be Real_Sequence; funca * z -> sequence of RNS means :Def3: :: NDIFF_1:def 3 for n being Element of NAT holds it . n = (a . n) * z; existence ex b1 being sequence of RNS st for n being Element of NAT holds b1 . n = (a . n) * z proof deffunc H1( Element of NAT ) -> Element of the carrier of RNS = (a . $1) * z; thus ex S being sequence of RNS st for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (a . n) * z ) & ( for n being Element of NAT holds b2 . n = (a . n) * z ) holds b1 = b2 proof let S1, S2 be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (a . n) * z ) & ( for n being Element of NAT holds S2 . n = (a . n) * z ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (a . n) * z and A2: for n being Element of NAT holds S2 . n = (a . n) * z ; ::_thesis: S1 = S2 for n being Element of NAT holds S1 . n = S2 . n proof let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (a . n) * z by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines * NDIFF_1:def_3_:_ for RNS being RealLinearSpace for z being Point of RNS for a being Real_Sequence for b4 being sequence of RNS holds ( b4 = a * z iff for n being Element of NAT holds b4 . n = (a . n) * z ); theorem :: NDIFF_1:8 for S being RealNormSpace for seq being sequence of S for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq) proof let S be RealNormSpace; ::_thesis: for seq being sequence of S for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq) let seq be sequence of S; ::_thesis: for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq) let rseq1, rseq2 be Real_Sequence; ::_thesis: (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((rseq1_+_rseq2)_(#)_seq)_._n_=_((rseq1_(#)_seq)_+_(rseq2_(#)_seq))_._n let n be Element of NAT ; ::_thesis: ((rseq1 + rseq2) (#) seq) . n = ((rseq1 (#) seq) + (rseq2 (#) seq)) . n thus ((rseq1 + rseq2) (#) seq) . n = ((rseq1 + rseq2) . n) * (seq . n) by Def2 .= ((rseq1 . n) + (rseq2 . n)) * (seq . n) by SEQ_1:7 .= ((rseq1 . n) * (seq . n)) + ((rseq2 . n) * (seq . n)) by RLVECT_1:def_6 .= ((rseq1 (#) seq) . n) + ((rseq2 . n) * (seq . n)) by Def2 .= ((rseq1 (#) seq) . n) + ((rseq2 (#) seq) . n) by Def2 .= ((rseq1 (#) seq) + (rseq2 (#) seq)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th9: :: NDIFF_1:9 for S being RealNormSpace for rseq being Real_Sequence for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2) proof let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2) let rseq be Real_Sequence; ::_thesis: for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2) let seq1, seq2 be sequence of S; ::_thesis: rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(rseq_(#)_(seq1_+_seq2))_._n_=_((rseq_(#)_seq1)_+_(rseq_(#)_seq2))_._n let n be Element of NAT ; ::_thesis: (rseq (#) (seq1 + seq2)) . n = ((rseq (#) seq1) + (rseq (#) seq2)) . n thus (rseq (#) (seq1 + seq2)) . n = (rseq . n) * ((seq1 + seq2) . n) by Def2 .= (rseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def_2 .= ((rseq . n) * (seq1 . n)) + ((rseq . n) * (seq2 . n)) by RLVECT_1:def_5 .= ((rseq (#) seq1) . n) + ((rseq . n) * (seq2 . n)) by Def2 .= ((rseq (#) seq1) . n) + ((rseq (#) seq2) . n) by Def2 .= ((rseq (#) seq1) + (rseq (#) seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th10: :: NDIFF_1:10 for r being Real for S being RealNormSpace for seq being sequence of S for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq) proof let r be Real; ::_thesis: for S being RealNormSpace for seq being sequence of S for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq) let S be RealNormSpace; ::_thesis: for seq being sequence of S for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq) let seq be sequence of S; ::_thesis: for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq) let rseq be Real_Sequence; ::_thesis: r * (rseq (#) seq) = rseq (#) (r * seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_*_(rseq_(#)_seq))_._n_=_(rseq_(#)_(r_*_seq))_._n let n be Element of NAT ; ::_thesis: (r * (rseq (#) seq)) . n = (rseq (#) (r * seq)) . n thus (r * (rseq (#) seq)) . n = r * ((rseq (#) seq) . n) by NORMSP_1:def_5 .= r * ((rseq . n) * (seq . n)) by Def2 .= (r * (rseq . n)) * (seq . n) by RLVECT_1:def_7 .= (rseq . n) * (r * (seq . n)) by RLVECT_1:def_7 .= (rseq . n) * ((r * seq) . n) by NORMSP_1:def_5 .= (rseq (#) (r * seq)) . n by Def2 ; ::_thesis: verum end; hence r * (rseq (#) seq) = rseq (#) (r * seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: NDIFF_1:11 for S being RealNormSpace for seq being sequence of S for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq) proof let S be RealNormSpace; ::_thesis: for seq being sequence of S for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq) let seq be sequence of S; ::_thesis: for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq) let rseq1, rseq2 be Real_Sequence; ::_thesis: (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((rseq1_-_rseq2)_(#)_seq)_._n_=_((rseq1_(#)_seq)_-_(rseq2_(#)_seq))_._n let n be Element of NAT ; ::_thesis: ((rseq1 - rseq2) (#) seq) . n = ((rseq1 (#) seq) - (rseq2 (#) seq)) . n thus ((rseq1 - rseq2) (#) seq) . n = ((rseq1 + (- rseq2)) . n) * (seq . n) by Def2 .= ((rseq1 . n) + ((- rseq2) . n)) * (seq . n) by SEQ_1:7 .= ((rseq1 . n) + (- (rseq2 . n))) * (seq . n) by SEQ_1:10 .= ((rseq1 . n) - (rseq2 . n)) * (seq . n) .= ((rseq1 . n) * (seq . n)) - ((rseq2 . n) * (seq . n)) by RLVECT_1:35 .= ((rseq1 (#) seq) . n) - ((rseq2 . n) * (seq . n)) by Def2 .= ((rseq1 (#) seq) . n) - ((rseq2 (#) seq) . n) by Def2 .= ((rseq1 (#) seq) - (rseq2 (#) seq)) . n by NORMSP_1:def_3 ; ::_thesis: verum end; hence (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th12: :: NDIFF_1:12 for S being RealNormSpace for rseq being Real_Sequence for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2) proof let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2) let rseq be Real_Sequence; ::_thesis: for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2) let seq1, seq2 be sequence of S; ::_thesis: rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(rseq_(#)_(seq1_-_seq2))_._n_=_((rseq_(#)_seq1)_-_(rseq_(#)_seq2))_._n let n be Element of NAT ; ::_thesis: (rseq (#) (seq1 - seq2)) . n = ((rseq (#) seq1) - (rseq (#) seq2)) . n thus (rseq (#) (seq1 - seq2)) . n = (rseq . n) * ((seq1 - seq2) . n) by Def2 .= (rseq . n) * ((seq1 . n) - (seq2 . n)) by NORMSP_1:def_3 .= ((rseq . n) * (seq1 . n)) - ((rseq . n) * (seq2 . n)) by RLVECT_1:34 .= ((rseq (#) seq1) . n) - ((rseq . n) * (seq2 . n)) by Def2 .= ((rseq (#) seq1) . n) - ((rseq (#) seq2) . n) by Def2 .= ((rseq (#) seq1) - (rseq (#) seq2)) . n by NORMSP_1:def_3 ; ::_thesis: verum end; hence rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th13: :: NDIFF_1:13 for S being RealNormSpace for rseq being Real_Sequence for seq being sequence of S st rseq is convergent & seq is convergent holds rseq (#) seq is convergent proof let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence for seq being sequence of S st rseq is convergent & seq is convergent holds rseq (#) seq is convergent let rseq be Real_Sequence; ::_thesis: for seq being sequence of S st rseq is convergent & seq is convergent holds rseq (#) seq is convergent let seq be sequence of S; ::_thesis: ( rseq is convergent & seq is convergent implies rseq (#) seq is convergent ) assume that A1: rseq is convergent and A2: seq is convergent ; ::_thesis: rseq (#) seq is convergent consider g1 being real number such that A3: 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 ((rseq . m) - g1) < p by A1, SEQ_2:def_6; consider g2 being Point of S such that A4: 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 ||.((seq . m) - g2).|| < p by A2, NORMSP_1:def_6; reconsider g1 = g1 as Real by XREAL_0:def_1; take g = g1 * g2; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.(((rseq (#) seq) . b3) - g).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((rseq (#) seq) . b2) - g).|| ) ) rseq is bounded by A1, SEQ_2:13; then consider r being real number such that A5: 0 < r and A6: for n being Element of NAT holds abs (rseq . n) < r by SEQ_2:3; reconsider r = r as Real by XREAL_0:def_1; A7: 0 + 0 < ||.g2.|| + r by A5, NORMSP_1:4, XREAL_1:8; assume A8: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.(((rseq (#) seq) . b2) - g).|| ) then consider n1 being Element of NAT such that A9: for m being Element of NAT st n1 <= m holds abs ((rseq . m) - g1) < p / (||.g2.|| + r) by A3, A7, XREAL_1:139; consider n2 being Element of NAT such that A10: for m being Element of NAT st n2 <= m holds ||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A4, A7, A8, XREAL_1:139; take n = n1 + n2; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.(((rseq (#) seq) . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((rseq (#) seq) . m) - g).|| ) assume A11: n <= m ; ::_thesis: not p <= ||.(((rseq (#) seq) . m) - g).|| n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A11, XXREAL_0:2; then A12: abs ((rseq . m) - g1) <= p / (||.g2.|| + r) by A9; ( 0 <= ||.g2.|| & ||.(((rseq . m) - g1) * g2).|| = ||.g2.|| * (abs ((rseq . m) - g1)) ) by NORMSP_1:4, NORMSP_1:def_1; then A13: ||.(((rseq . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + r)) by A12, XREAL_1:64; ||.(((rseq (#) seq) . m) - g).|| = ||.(((rseq . m) * (seq . m)) - (g1 * g2)).|| by Def2 .= ||.((((rseq . m) * (seq . m)) - (0. S)) - (g1 * g2)).|| by RLVECT_1:13 .= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * g2) - ((rseq . m) * g2))) - (g1 * g2)).|| by RLVECT_1:15 .= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:29 .= ||.((((rseq . m) * ((seq . m) - g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:34 .= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) * g2) - (g1 * g2))).|| by RLVECT_1:def_3 .= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) - g1) * g2)).|| by RLVECT_1:35 ; then A14: ||.(((rseq (#) seq) . m) - g).|| <= ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| by NORMSP_1:def_1; n2 <= n by NAT_1:12; then n2 <= m by A11, XXREAL_0:2; then A15: ||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A10; A16: ( 0 <= abs (rseq . m) & 0 <= ||.((seq . m) - g2).|| ) by COMPLEX1:46, NORMSP_1:4; abs (rseq . m) < r by A6; then (abs (rseq . m)) * ||.((seq . m) - g2).|| < r * (p / (||.g2.|| + r)) by A16, A15, XREAL_1:96; then A17: ||.((rseq . m) * ((seq . m) - g2)).|| < r * (p / (||.g2.|| + r)) by NORMSP_1:def_1; (r * (p / (||.g2.|| + r))) + (||.g2.|| * (p / (||.g2.|| + r))) = (p / (||.g2.|| + r)) * (||.g2.|| + r) .= p by A7, XCMPLX_1:87 ; then ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| < p by A17, A13, XREAL_1:8; hence not p <= ||.(((rseq (#) seq) . m) - g).|| by A14, XXREAL_0:2; ::_thesis: verum end; theorem Th14: :: NDIFF_1:14 for S being RealNormSpace for rseq being Real_Sequence for seq being sequence of S st rseq is convergent & seq is convergent holds lim (rseq (#) seq) = (lim rseq) * (lim seq) proof let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence for seq being sequence of S st rseq is convergent & seq is convergent holds lim (rseq (#) seq) = (lim rseq) * (lim seq) let rseq be Real_Sequence; ::_thesis: for seq being sequence of S st rseq is convergent & seq is convergent holds lim (rseq (#) seq) = (lim rseq) * (lim seq) let seq be sequence of S; ::_thesis: ( rseq is convergent & seq is convergent implies lim (rseq (#) seq) = (lim rseq) * (lim seq) ) assume that A1: rseq is convergent and A2: seq is convergent ; ::_thesis: lim (rseq (#) seq) = (lim rseq) * (lim seq) set g2 = lim seq; reconsider g1 = lim rseq as Real ; set g = g1 * (lim seq); rseq is bounded by A1, SEQ_2:13; then consider r being real number such that A3: 0 < r and A4: for n being Element of NAT holds abs (rseq . n) < r by SEQ_2:3; reconsider r = r as Real by XREAL_0:def_1; A5: 0 + 0 < ||.(lim seq).|| + r by A3, NORMSP_1:4, XREAL_1:8; A6: 0 <= ||.(lim seq).|| by NORMSP_1:4; A7: 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 ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p proof 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 ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p then A8: 0 < p / (||.(lim seq).|| + r) by A5, XREAL_1:139; then consider n1 being Element of NAT such that A9: for m being Element of NAT st n1 <= m holds abs ((rseq . m) - g1) < p / (||.(lim seq).|| + r) by A1, SEQ_2:def_7; consider n2 being Element of NAT such that A10: for m being Element of NAT st n2 <= m holds ||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A2, A8, NORMSP_1:def_7; take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p ) assume A11: n <= m ; ::_thesis: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A11, XXREAL_0:2; then A12: abs ((rseq . m) - g1) <= p / (||.(lim seq).|| + r) by A9; ||.(((rseq . m) - g1) * (lim seq)).|| = ||.(lim seq).|| * (abs ((rseq . m) - g1)) by NORMSP_1:def_1; then A13: ||.(((rseq . m) - g1) * (lim seq)).|| <= ||.(lim seq).|| * (p / (||.(lim seq).|| + r)) by A6, A12, XREAL_1:64; A14: ( 0 <= abs (rseq . m) & 0 <= ||.((seq . m) - (lim seq)).|| ) by COMPLEX1:46, NORMSP_1:4; n2 <= n by NAT_1:12; then n2 <= m by A11, XXREAL_0:2; then A15: ||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A10; ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| = ||.(((rseq . m) * (seq . m)) - (g1 * (lim seq))).|| by Def2 .= ||.((((rseq . m) * (seq . m)) - (0. S)) - (g1 * (lim seq))).|| by RLVECT_1:13 .= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * (lim seq)) - ((rseq . m) * (lim seq)))) - (g1 * (lim seq))).|| by RLVECT_1:15 .= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:29 .= ||.((((rseq . m) * ((seq . m) - (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:34 .= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) * (lim seq)) - (g1 * (lim seq)))).|| by RLVECT_1:def_3 .= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) - g1) * (lim seq))).|| by RLVECT_1:35 ; then A16: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| <= ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| by NORMSP_1:def_1; abs (rseq . m) < r by A4; then (abs (rseq . m)) * ||.((seq . m) - (lim seq)).|| < r * (p / (||.(lim seq).|| + r)) by A14, A15, XREAL_1:96; then A17: ||.((rseq . m) * ((seq . m) - (lim seq))).|| < r * (p / (||.(lim seq).|| + r)) by NORMSP_1:def_1; (r * (p / (||.(lim seq).|| + r))) + (||.(lim seq).|| * (p / (||.(lim seq).|| + r))) = (p / (||.(lim seq).|| + r)) * (||.(lim seq).|| + r) .= p by A5, XCMPLX_1:87 ; then ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| < p by A17, A13, XREAL_1:8; hence ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p by A16, XXREAL_0:2; ::_thesis: verum end; rseq (#) seq is convergent by A1, A2, Th13; hence lim (rseq (#) seq) = (lim rseq) * (lim seq) by A7, NORMSP_1:def_7; ::_thesis: verum end; theorem Th15: :: NDIFF_1:15 for k being Element of NAT for S being RealNormSpace for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) proof let k be Element of NAT ; ::_thesis: for S being RealNormSpace for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) let S be RealNormSpace; ::_thesis: for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) let seq, seq1 be sequence of S; ::_thesis: (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_+_seq1)_^\_k)_._n_=_((seq_^\_k)_+_(seq1_^\_k))_._n let n be Element of NAT ; ::_thesis: ((seq + seq1) ^\ k) . n = ((seq ^\ k) + (seq1 ^\ k)) . n thus ((seq + seq1) ^\ k) . n = (seq + seq1) . (n + k) by NAT_1:def_3 .= (seq . (n + k)) + (seq1 . (n + k)) by NORMSP_1:def_2 .= ((seq ^\ k) . n) + (seq1 . (n + k)) by NAT_1:def_3 .= ((seq ^\ k) . n) + ((seq1 ^\ k) . n) by NAT_1:def_3 .= ((seq ^\ k) + (seq1 ^\ k)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem Th16: :: NDIFF_1:16 for k being Element of NAT for S being RealNormSpace for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) proof let k be Element of NAT ; ::_thesis: for S being RealNormSpace for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) let S be RealNormSpace; ::_thesis: for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) let seq, seq1 be sequence of S; ::_thesis: (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_-_seq1)_^\_k)_._n_=_((seq_^\_k)_-_(seq1_^\_k))_._n let n be Element of NAT ; ::_thesis: ((seq - seq1) ^\ k) . n = ((seq ^\ k) - (seq1 ^\ k)) . n thus ((seq - seq1) ^\ k) . n = (seq - seq1) . (n + k) by NAT_1:def_3 .= (seq . (n + k)) - (seq1 . (n + k)) by NORMSP_1:def_3 .= ((seq ^\ k) . n) - (seq1 . (n + k)) by NAT_1:def_3 .= ((seq ^\ k) . n) - ((seq1 ^\ k) . n) by NAT_1:def_3 .= ((seq ^\ k) - (seq1 ^\ k)) . n by NORMSP_1:def_3 ; ::_thesis: verum end; hence (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem Th17: :: NDIFF_1:17 for k being Element of NAT for S being RealNormSpace for seq being sequence of S st seq is non-zero holds seq ^\ k is non-zero proof let k be Element of NAT ; ::_thesis: for S being RealNormSpace for seq being sequence of S st seq is non-zero holds seq ^\ k is non-zero let S be RealNormSpace; ::_thesis: for seq being sequence of S st seq is non-zero holds seq ^\ k is non-zero let seq be sequence of S; ::_thesis: ( seq is non-zero implies seq ^\ k is non-zero ) assume A1: seq is non-zero ; ::_thesis: seq ^\ k is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_k)_._n_<>_0._S let n be Element of NAT ; ::_thesis: (seq ^\ k) . n <> 0. S (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3; hence (seq ^\ k) . n <> 0. S by A1, Th7; ::_thesis: verum end; hence seq ^\ k is non-zero by Th7; ::_thesis: verum end; definition let S be RealNormSpace; let x be Point of S; let IT be sequence of S; attrIT is x -convergent means :Def4: :: NDIFF_1:def 4 ( IT is convergent & lim IT = x ); end; :: deftheorem Def4 defines -convergent NDIFF_1:def_4_:_ for S being RealNormSpace for x being Point of S for IT being sequence of S holds ( IT is x -convergent iff ( IT is convergent & lim IT = x ) ); theorem Th18: :: NDIFF_1:18 for X being RealNormSpace for seq being sequence of X st seq is constant holds ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) ) proof let X be RealNormSpace; ::_thesis: for seq being sequence of X st seq is constant holds ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) ) let seq be sequence of X; ::_thesis: ( seq is constant implies ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) ) ) assume A1: seq is constant ; ::_thesis: ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) ) then consider r being Point of X such that A2: for n being Nat holds seq . n = r by VALUED_0:def_18; thus A3: seq is convergent by A1, LOPBAN_3:12; ::_thesis: for k being Element of NAT holds lim seq = seq . k now__::_thesis:_for_k_being_Element_of_NAT_holds_lim_seq_=_seq_._k let k be Element of NAT ; ::_thesis: lim seq = seq . k 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_ ||.((seq_._m)_-_(seq_._k)).||_<_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 ||.((seq . m) - (seq . k)).|| < p ) assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . k)).|| < p take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds ||.((seq . m) - (seq . k)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (seq . k)).|| < p ) assume n <= m ; ::_thesis: ||.((seq . m) - (seq . k)).|| < p ||.((seq . m) - (seq . k)).|| = ||.(r - (seq . k)).|| by A2 .= ||.(r - r).|| by A2 .= ||.(0. X).|| by RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.((seq . m) - (seq . k)).|| < p by A4; ::_thesis: verum end; hence lim seq = seq . k by A3, NORMSP_1:def_7; ::_thesis: verum end; hence for k being Element of NAT holds lim seq = seq . k ; ::_thesis: verum end; theorem Th19: :: NDIFF_1:19 for S being RealNormSpace for seq being sequence of S for x0 being Point of S for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds seq is convergent proof let S be RealNormSpace; ::_thesis: for seq being sequence of S for x0 being Point of S for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds seq is convergent let seq be sequence of S; ::_thesis: for x0 being Point of S for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds seq is convergent let x0 be Point of S; ::_thesis: for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds seq is convergent let r be Real; ::_thesis: ( 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) implies seq is convergent ) assume that A1: 0 < r and A2: for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ; ::_thesis: seq is convergent take g = 0. S; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= ||.((seq . b3) - g).|| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| ) ) assume A3: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| ) ex pp being Real st ( pp > 0 & pp * ||.x0.|| < p ) proof take pp = p / (||.x0.|| + 1); ::_thesis: ( pp > 0 & pp * ||.x0.|| < p ) A4: ( ||.x0.|| + 0 < ||.x0.|| + 1 & 0 <= ||.x0.|| ) by NORMSP_1:4, XREAL_1:8; A5: ||.x0.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8; then 0 < p / (||.x0.|| + 1) by A3, XREAL_1:139; then pp * ||.x0.|| < pp * (||.x0.|| + 1) by A4, XREAL_1:97; hence ( pp > 0 & pp * ||.x0.|| < p ) by A3, A5, XCMPLX_1:87; ::_thesis: verum end; then consider pp being Real such that A6: pp > 0 and A7: pp * ||.x0.|| < p ; consider k1 being Element of NAT such that A8: pp " < k1 by SEQ_4:3; (pp ") + 0 < k1 + r by A1, A8, XREAL_1:8; then 1 / (k1 + r) < 1 / (pp ") by A6, XREAL_1:76; then A9: 1 / (k1 + r) < 1 * ((pp ") ") by XCMPLX_0:def_9; take n = k1; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= ||.((seq . b1) - g).|| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq . m) - g).|| ) assume n <= m ; ::_thesis: not p <= ||.((seq . m) - g).|| then A10: n + r <= m + r by XREAL_1:6; A11: 0 <= ||.x0.|| by NORMSP_1:4; 0 < pp " by A6; then 1 / (m + r) <= 1 / (n + r) by A1, A8, A10, XREAL_1:118; then 1 / (m + r) < pp by A9, XXREAL_0:2; then A12: (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by A11, XREAL_1:64; A13: 0 <= m by NAT_1:2; ||.((seq . m) - g).|| = ||.(((1 / (m + r)) * x0) - (0. S)).|| by A2 .= ||.((1 / (m + r)) * x0).|| by RLVECT_1:13 .= (abs (1 / (m + r))) * ||.x0.|| by NORMSP_1:def_1 .= (1 / (m + r)) * ||.x0.|| by A1, A13, ABSVALUE:def_1 ; hence not p <= ||.((seq . m) - g).|| by A7, A12, XXREAL_0:2; ::_thesis: verum end; theorem Th20: :: NDIFF_1:20 for S being RealNormSpace for seq being sequence of S for x0 being Point of S for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds lim seq = 0. S proof let S be RealNormSpace; ::_thesis: for seq being sequence of S for x0 being Point of S for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds lim seq = 0. S let seq be sequence of S; ::_thesis: for x0 being Point of S for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds lim seq = 0. S let x0 be Point of S; ::_thesis: for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds lim seq = 0. S let r be Real; ::_thesis: ( 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) implies lim seq = 0. S ) assume that A1: 0 < r and A2: for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ; ::_thesis: lim seq = 0. S A3: 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_ ||.((seq_._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 ||.((seq . m) - (0. S)).|| < p ) A4: 0 <= ||.x0.|| by NORMSP_1:4; assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((seq . m) - (0. S)).|| < p ex pp being Real st ( pp > 0 & pp * ||.x0.|| < p ) proof take pp = p / (||.x0.|| + 1); ::_thesis: ( pp > 0 & pp * ||.x0.|| < p ) A6: ( ||.x0.|| + 0 < ||.x0.|| + 1 & 0 <= ||.x0.|| ) by NORMSP_1:4, XREAL_1:8; A7: ||.x0.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8; then 0 < p / (||.x0.|| + 1) by A5, XREAL_1:139; then pp * ||.x0.|| < pp * (||.x0.|| + 1) by A6, XREAL_1:97; hence ( pp > 0 & pp * ||.x0.|| < p ) by A5, A7, XCMPLX_1:87; ::_thesis: verum end; then consider pp being Real such that A8: pp > 0 and A9: pp * ||.x0.|| < p ; consider k1 being Element of NAT such that A10: pp " < k1 by SEQ_4:3; (pp ") + 0 < k1 + r by A1, A10, XREAL_1:8; then 1 / (k1 + r) < 1 / (pp ") by A8, XREAL_1:76; then A11: 1 / (k1 + r) < 1 * ((pp ") ") by XCMPLX_0:def_9; take n = k1; ::_thesis: for m being Element of NAT st n <= m holds ||.((seq . m) - (0. S)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (0. S)).|| < p ) assume n <= m ; ::_thesis: ||.((seq . m) - (0. S)).|| < p then A12: n + r <= m + r by XREAL_1:6; 0 < pp " by A8; then 1 / (m + r) <= 1 / (n + r) by A1, A10, A12, XREAL_1:118; then 1 / (m + r) < pp by A11, XXREAL_0:2; then A13: (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by A4, XREAL_1:64; A14: 0 <= m by NAT_1:2; ||.((seq . m) - (0. S)).|| = ||.(((1 / (m + r)) * x0) - (0. S)).|| by A2 .= ||.((1 / (m + r)) * x0).|| by RLVECT_1:13 .= (abs (1 / (m + r))) * ||.x0.|| by NORMSP_1:def_1 .= (1 / (m + r)) * ||.x0.|| by A1, A14, ABSVALUE:def_1 ; hence ||.((seq . m) - (0. S)).|| < p by A9, A13, XXREAL_0:2; ::_thesis: verum end; seq is convergent by A1, A2, Th19; hence lim seq = 0. S by A3, NORMSP_1:def_7; ::_thesis: verum end; registration let S be non trivial RealNormSpace; clusterV1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total non-zero 0. S -convergent for Element of K6(K7(NAT, the carrier of S)); existence ex b1 being sequence of S st ( b1 is non-zero & b1 is 0. S -convergent ) proof consider x0 being Point of S such that A1: x0 <> 0. S by STRUCT_0:def_18; deffunc H1( Element of NAT ) -> Element of the carrier of S = (1 / (S + 1)) * x0; consider s1 being sequence of S such that A2: for n being Element of NAT holds s1 . n = H1(n) from FUNCT_2:sch_4(); take s1 ; ::_thesis: ( s1 is non-zero & s1 is 0. S -convergent ) now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0._S let n be Element of NAT ; ::_thesis: s1 . n <> 0. S (n + 1) " <> 0 by NAT_1:5, XCMPLX_1:202; then A3: 1 / (n + 1) <> 0 by XCMPLX_1:215; thus s1 . n <> 0. S ::_thesis: verum proof assume s1 . n = 0. S ; ::_thesis: contradiction then (1 / (n + 1)) * x0 = 0. S by A2; hence contradiction by A1, A3, RLVECT_1:11; ::_thesis: verum end; end; hence s1 is non-zero by Th7; ::_thesis: s1 is 0. S -convergent A4: lim s1 = 0. S by A2, Th20; s1 is convergent by A2, Th19; then s1 is 0. S -convergent by Def4, A4; hence s1 is 0. S -convergent ; ::_thesis: verum end; end; theorem :: NDIFF_1:21 for S being RealNormSpace for a being non-zero 0 -convergent Real_Sequence for z being Point of S st z <> 0. S holds ( a * z is non-zero & a * z is 0. S -convergent ) proof let S be RealNormSpace; ::_thesis: for a being non-zero 0 -convergent Real_Sequence for z being Point of S st z <> 0. S holds ( a * z is non-zero & a * z is 0. S -convergent ) let a be non-zero 0 -convergent Real_Sequence; ::_thesis: for z being Point of S st z <> 0. S holds ( a * z is non-zero & a * z is 0. S -convergent ) let z be Point of S; ::_thesis: ( z <> 0. S implies ( a * z is non-zero & a * z is 0. S -convergent ) ) assume A1: z <> 0. S ; ::_thesis: ( a * z is non-zero & a * z is 0. S -convergent ) now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(a_*_z)_._n_=_0._S let n be Element of NAT ; ::_thesis: not (a * z) . n = 0. S A2: a . n <> 0 by SEQ_1:5; assume (a * z) . n = 0. S ; ::_thesis: contradiction then (a . n) * z = 0. S by Def3; hence contradiction by A1, A2, RLVECT_1:11; ::_thesis: verum end; hence a * z is non-zero by Th7; ::_thesis: a * z is 0. S -convergent A3: 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_ ||.(((a_*_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 ||.(((a * z) . m) - (0. S)).|| < p ) assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((a * 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 ) A5: ( ||.z.|| + 0 < ||.z.|| + 1 & 0 <= ||.z.|| ) by NORMSP_1:4, XREAL_1:8; A6: ||.z.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8; then 0 < p / (||.z.|| + 1) by A4, XREAL_1:139; then pp * ||.z.|| < pp * (||.z.|| + 1) by A5, XREAL_1:97; hence ( pp > 0 & pp * ||.z.|| < p ) by A4, A6, XCMPLX_1:87; ::_thesis: verum end; then consider pp being Real such that A7: pp > 0 and A8: pp * ||.z.|| < p ; ( a is convergent & lim a = 0 ) ; then consider n being Element of NAT such that A9: for m being Element of NAT st n <= m holds abs ((a . m) - 0) < pp by A7, SEQ_2:def_7; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.(((a * z) . m) - (0. S)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((a * z) . m) - (0. S)).|| < p ) assume n <= m ; ::_thesis: ||.(((a * z) . m) - (0. S)).|| < p then A10: abs ((a . m) - 0) < pp by A9; A11: ||.(((a * z) . m) - (0. S)).|| = ||.(((a . m) * z) - (0. S)).|| by Def3 .= ||.((a . m) * z).|| by RLVECT_1:13 .= (abs (a . m)) * ||.z.|| by NORMSP_1:def_1 ; 0 <= ||.z.|| by NORMSP_1:4; then (abs (a . m)) * ||.z.|| <= pp * ||.z.|| by A10, XREAL_1:64; hence ||.(((a * z) . m) - (0. S)).|| < p by A8, A11, XXREAL_0:2; ::_thesis: verum end; hence a * z is convergent by NORMSP_1:def_6; :: according to NDIFF_1:def_4 ::_thesis: lim (a * z) = 0. S hence lim (a * z) = 0. S by A3, NORMSP_1:def_7; ::_thesis: verum end; theorem :: NDIFF_1:22 for S being RealNormSpace for Y being Subset of S holds ( ( for r being Point of S holds ( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S ) proof let S be RealNormSpace; ::_thesis: for Y being Subset of S holds ( ( for r being Point of S holds ( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S ) let Y be Subset of S; ::_thesis: ( ( for r being Point of S holds ( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S ) thus ( ( for r being Point of S holds ( r in Y iff r in the carrier of S ) ) implies Y = the carrier of S ) ::_thesis: ( Y = the carrier of S implies for r being Point of S holds ( r in Y iff r in the carrier of S ) ) proof assume for r being Point of S holds ( r in Y iff r in the carrier of S ) ; ::_thesis: Y = the carrier of S then for y being set holds ( y in Y iff y in the carrier of S ) ; hence Y = the carrier of S by TARSKI:1; ::_thesis: verum end; assume A1: Y = the carrier of S ; ::_thesis: for r being Point of S holds ( r in Y iff r in the carrier of S ) let r be Point of S; ::_thesis: ( r in Y iff r in the carrier of S ) thus ( r in Y implies r in the carrier of S ) ; ::_thesis: ( r in the carrier of S implies r in Y ) thus ( r in the carrier of S implies r in Y ) by A1; ::_thesis: verum end; registration let S be non trivial RealNormSpace; clusterV1() V16() V19( NAT ) V20( the carrier of S) Function-like constant total quasi_total for Element of K6(K7(NAT, the carrier of S)); existence ex b1 being sequence of S st b1 is constant proof reconsider s1 = NAT --> (0. S) as sequence of S ; take s1 ; ::_thesis: s1 is constant thus s1 is constant ; ::_thesis: verum end; end; definition let S, T be non trivial RealNormSpace; let IT be PartFunc of S,T; attrIT is RestFunc-like means :Def5: :: NDIFF_1:def 5 ( IT is total & ( for h being non-zero 0. S -convergent sequence of S holds ( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ); end; :: deftheorem Def5 defines RestFunc-like NDIFF_1:def_5_:_ for S, T being non trivial RealNormSpace for IT being PartFunc of S,T holds ( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0. b1 -convergent sequence of S holds ( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) ); registration let S, T be non trivial RealNormSpace; clusterV16() V19( the carrier of S) V20( the carrier of T) Function-like RestFunc-like for Element of K6(K7( the carrier of S, the carrier of T)); existence ex b1 being PartFunc of S,T st b1 is RestFunc-like proof reconsider f = the carrier of S --> (0. T) as PartFunc of S,T ; take f ; ::_thesis: f is RestFunc-like thus f is total ; :: according to NDIFF_1:def_5 ::_thesis: for h being non-zero 0. S -convergent sequence of S holds ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) A1: dom f = the carrier of S by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_(f_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(f_/*_h))_=_0._T_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(f_/*_h))_._n_=_0._T let n be Nat; ::_thesis: ((||.h.|| ") (#) (f /* h)) . n = 0. T A2: f /. (h . n) = f . (h . n) by A1, PARTFUN1:def_6 .= 0. T by FUNCOP_1:7 ; A3: rng h c= dom f by A1; A4: n in NAT by ORDINAL1:def_12; hence ((||.h.|| ") (#) (f /* h)) . n = ((||.h.|| ") . n) * ((f /* h) . n) by Def2 .= ((||.h.|| ") . n) * (f /. (h . n)) by A3, A4, FUNCT_2:109 .= 0. T by A2, RLVECT_1:10 ; ::_thesis: verum end; then ( (||.h.|| ") (#) (f /* h) is constant & ((||.h.|| ") (#) (f /* h)) . 0 = 0. T ) by VALUED_0:def_18; hence ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) by Th18; ::_thesis: verum end; hence for h being non-zero 0. S -convergent sequence of S holds ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) ; ::_thesis: verum end; end; definition let S, T be non trivial RealNormSpace; mode RestFunc of S,T is RestFunc-like PartFunc of S,T; end; theorem :: NDIFF_1:23 for S, T being non trivial RealNormSpace for R being PartFunc of S,T st R is total holds ( R is RestFunc-like iff for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for R being PartFunc of S,T st R is total holds ( R is RestFunc-like iff for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) let R be PartFunc of S,T; ::_thesis: ( R is total implies ( R is RestFunc-like iff for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) ) assume A1: R is total ; ::_thesis: ( R is RestFunc-like iff for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) A2: now__::_thesis:_(_R_is_RestFunc-like_&_ex_r_being_Real_st_ (_r_>_0_&_(_for_d_being_Real_holds_ (_not_d_>_0_or_ex_z_being_Point_of_S_st_ (_z_<>_0._S_&_||.z.||_<_d_&_not_(||.z.||_")_*_||.(R_/._z).||_<_r_)_)_)_)_implies_for_r_being_Real_st_r_>_0_holds_ ex_d_being_Real_st_ (_d_>_0_&_(_for_z_being_Point_of_S_st_z_<>_0._S_&_||.z.||_<_d_holds_ (||.z.||_")_*_||.(R_/._z).||_<_r_)_)_) assume A3: R is RestFunc-like ; ::_thesis: ( ex r being Real st ( r > 0 & ( for d being Real holds ( not d > 0 or ex z being Point of S st ( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ) ) ) implies for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) assume ex r being Real st ( r > 0 & ( for d being Real holds ( not d > 0 or ex z being Point of S st ( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ) ) ) ; ::_thesis: for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) then consider r being Real such that A4: r > 0 and A5: for d being Real st d > 0 holds ex z being Point of S st ( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ; defpred S1[ Element of NAT , Point of S] means ( $2 <> 0. S & ||.$2.|| < 1 / ($1 + 1) & not (||.$2.|| ") * ||.(R /. $2).|| < r ); A6: for n being Element of NAT ex z being Point of S st S1[n,z] proof let n be Element of NAT ; ::_thesis: ex z being Point of S st S1[n,z] 0 <= n by NAT_1:2; then 0 < 1 * ((n + 1) ") ; then 0 < 1 / (n + 1) by XCMPLX_0:def_9; hence ex z being Point of S st S1[n,z] by A5; ::_thesis: verum end; consider s being sequence of S such that A7: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch_3(A6); A8: 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_ ||.((s_._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 ||.((s . m) - (0. S)).|| < p ) assume A9: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((s . m) - (0. S)).|| < p consider n being Element of NAT such that A10: p " < n by SEQ_4:3; (p ") + 0 < n + 1 by A10, XREAL_1:8; then 1 / (n + 1) < 1 / (p ") by A9, XREAL_1:76; then A11: 1 / (n + 1) < p by XCMPLX_1:216; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.((s . m) - (0. S)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((s . m) - (0. S)).|| < p ) assume n <= m ; ::_thesis: ||.((s . m) - (0. S)).|| < p then A12: n + 1 <= m + 1 by XREAL_1:6; ||.(s . m).|| < 1 / (m + 1) by A7; then A13: ||.((s . m) - (0. S)).|| < 1 / (m + 1) by RLVECT_1:13; 0 <= n by NAT_1:2; then 1 / (m + 1) <= 1 / (n + 1) by A12, XREAL_1:118; then ||.((s . m) - (0. S)).|| < 1 / (n + 1) by A13, XXREAL_0:2; hence ||.((s . m) - (0. S)).|| < p by A11, XXREAL_0:2; ::_thesis: verum end; then A14: s is convergent by NORMSP_1:def_6; then A15: lim s = 0. S by A8, NORMSP_1:def_7; s is non-zero by A7, Th7; then reconsider s = s as non-zero 0. S -convergent sequence of S by A14, A15, Def4; ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T ) by A3, Def5; then consider n being Element of NAT such that A16: for m being Element of NAT st n <= m holds ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A4, NORMSP_1:def_7; A17: ||.((((||.s.|| ") (#) (R /* s)) . n) - (0. T)).|| < r by A16; s . n <> 0. S by A7; then ||.(s . n).|| <> 0 by NORMSP_0:def_5; then A18: ||.(s . n).|| > 0 by NORMSP_1:4; A19: ||.((||.(s . n).|| ") * (R /. (s . n))).|| = (abs (||.(s . n).|| ")) * ||.(R /. (s . n)).|| by NORMSP_1:def_1 .= (||.(s . n).|| ") * ||.(R /. (s . n)).|| by A18, ABSVALUE:def_1 ; dom R = the carrier of S by A1, PARTFUN1:def_2; then A20: rng s c= dom R ; ||.((((||.s.|| ") (#) (R /* s)) . n) - (0. T)).|| = ||.(((||.s.|| ") (#) (R /* s)) . n).|| by RLVECT_1:13 .= ||.(((||.s.|| ") . n) * ((R /* s) . n)).|| by Def2 .= ||.(((||.s.|| . n) ") * ((R /* s) . n)).|| by VALUED_1:10 .= ||.((||.(s . n).|| ") * ((R /* s) . n)).|| by NORMSP_0:def_4 .= ||.((||.(s . n).|| ") * (R /. (s . n))).|| by A20, FUNCT_2:109 ; hence for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) by A7, A17, A19; ::_thesis: verum end; now__::_thesis:_(_(_for_r_being_Real_st_r_>_0_holds_ ex_d_being_Real_st_ (_d_>_0_&_(_for_z_being_Point_of_S_st_z_<>_0._S_&_||.z.||_<_d_holds_ (||.z.||_")_*_||.(R_/._z).||_<_r_)_)_)_implies_R_is_RestFunc-like_) assume A21: for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ; ::_thesis: R is RestFunc-like now__::_thesis:_for_s_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.s.||_")_(#)_(R_/*_s)_is_convergent_&_lim_((||.s.||_")_(#)_(R_/*_s))_=_0._T_) let s be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T ) A22: ( s is convergent & lim s = 0. S ) by Def4; A23: 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_ ||.((((||.s.||_")_(#)_(R_/*_s))_._m)_-_(0._T)).||_<_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 ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r ) assume r > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r then consider d being Real such that A24: d > 0 and A25: for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r by A21; consider n being Element of NAT such that A26: for m being Element of NAT st n <= m holds ||.((s . m) - (0. S)).|| < d by A22, A24, NORMSP_1:def_7; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r thus for m being Element of NAT st n <= m holds ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r ::_thesis: verum proof dom R = the carrier of S by A1, PARTFUN1:def_2; then A27: rng s c= dom R ; let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r ) assume n <= m ; ::_thesis: ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r then ||.((s . m) - (0. S)).|| < d by A26; then A28: ||.(s . m).|| < d by RLVECT_1:13; A29: s . m <> 0. S by Th7; s . m <> 0. S by Th7; then ||.(s . m).|| <> 0 by NORMSP_0:def_5; then ||.(s . m).|| > 0 by NORMSP_1:4; then (||.(s . m).|| ") * ||.(R /. (s . m)).|| = (abs (||.(s . m).|| ")) * ||.(R /. (s . m)).|| by ABSVALUE:def_1 .= ||.((||.(s . m).|| ") * (R /. (s . m))).|| by NORMSP_1:def_1 .= ||.((||.(s . m).|| ") * ((R /* s) . m)).|| by A27, FUNCT_2:109 .= ||.(((||.s.|| . m) ") * ((R /* s) . m)).|| by NORMSP_0:def_4 .= ||.(((||.s.|| ") . m) * ((R /* s) . m)).|| by VALUED_1:10 .= ||.(((||.s.|| ") (#) (R /* s)) . m).|| by Def2 .= ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| by RLVECT_1:13 ; hence ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A25, A28, A29; ::_thesis: verum end; end; hence (||.s.|| ") (#) (R /* s) is convergent by NORMSP_1:def_6; ::_thesis: lim ((||.s.|| ") (#) (R /* s)) = 0. T hence lim ((||.s.|| ") (#) (R /* s)) = 0. T by A23, NORMSP_1:def_7; ::_thesis: verum end; hence R is RestFunc-like by A1, Def5; ::_thesis: verum end; hence ( R is RestFunc-like iff for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r ) ) ) by A2; ::_thesis: verum end; theorem Th24: :: NDIFF_1:24 for S, T being non trivial RealNormSpace for R being RestFunc of S,T for s being non-zero 0. b1 -convergent sequence of S holds ( R /* s is convergent & lim (R /* s) = 0. T ) proof let S, T be non trivial RealNormSpace; ::_thesis: for R being RestFunc of S,T for s being non-zero 0. S -convergent sequence of S holds ( R /* s is convergent & lim (R /* s) = 0. T ) let R be RestFunc of S,T; ::_thesis: for s being non-zero 0. S -convergent sequence of S holds ( R /* s is convergent & lim (R /* s) = 0. T ) let s be non-zero 0. S -convergent sequence of S; ::_thesis: ( R /* s is convergent & lim (R /* s) = 0. T ) A1: (||.s.|| ") (#) (R /* s) is convergent by Def5; now__::_thesis:_for_n_being_Element_of_NAT_holds_(||.s.||_(#)_((||.s.||_")_(#)_(R_/*_s)))_._n_=_(R_/*_s)_._n let n be Element of NAT ; ::_thesis: (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (R /* s) . n s . n <> 0. S by Th7; then A2: ||.(s . n).|| <> 0 by NORMSP_0:def_5; thus (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (||.s.|| . n) * (((||.s.|| ") (#) (R /* s)) . n) by Def2 .= (||.s.|| . n) * (((||.s.|| ") . n) * ((R /* s) . n)) by Def2 .= ||.(s . n).|| * (((||.s.|| ") . n) * ((R /* s) . n)) by NORMSP_0:def_4 .= ||.(s . n).|| * (((||.s.|| . n) ") * ((R /* s) . n)) by VALUED_1:10 .= ||.(s . n).|| * ((||.(s . n).|| ") * ((R /* s) . n)) by NORMSP_0:def_4 .= (||.(s . n).|| * (||.(s . n).|| ")) * ((R /* s) . n) by RLVECT_1:def_7 .= 1 * ((R /* s) . n) by A2, XCMPLX_0:def_7 .= (R /* s) . n by RLVECT_1:def_8 ; ::_thesis: verum end; then A3: ||.s.|| (#) ((||.s.|| ") (#) (R /* s)) = R /* s by FUNCT_2:63; A4: s is convergent by Def4; then A5: ||.s.|| is convergent by LOPBAN_1:41; lim s = 0. S by Def4; then lim ||.s.|| = ||.(0. S).|| by A4, LOPBAN_1:41; then A6: lim ||.s.|| = 0 by NORMSP_1:1; lim ((||.s.|| ") (#) (R /* s)) = 0. T by Def5; then lim (R /* s) = 0 * (0. T) by A4, A3, A1, A6, Th14, LOPBAN_1:41; hence ( R /* s is convergent & lim (R /* s) = 0. T ) by A3, A1, A5, Th13, RLVECT_1:10; ::_thesis: verum end; theorem Th25: :: NDIFF_1:25 for S, T being non trivial RealNormSpace for h1, h2 being PartFunc of S,T for seq being sequence of S st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for h1, h2 being PartFunc of S,T for seq being sequence of S st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) let h1, h2 be PartFunc of S,T; ::_thesis: for seq being sequence of S st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) let seq be sequence of S; ::_thesis: ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) ) assume ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) then h1 + h2 is total by VFUNCT_1:32; then dom (h1 + h2) = the carrier of S by PARTFUN1:def_2; then (dom h1) /\ (dom h2) = the carrier of S by VFUNCT_1:def_1; then A1: rng seq c= (dom h1) /\ (dom h2) ; hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NFCONT_1:12; ::_thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, NFCONT_1:12; ::_thesis: verum end; theorem Th26: :: NDIFF_1:26 for S, T being non trivial RealNormSpace for h being PartFunc of S,T for seq being sequence of S for r being Real st h is total holds (r (#) h) /* seq = r * (h /* seq) proof let S, T be non trivial RealNormSpace; ::_thesis: for h being PartFunc of S,T for seq being sequence of S for r being Real st h is total holds (r (#) h) /* seq = r * (h /* seq) let h be PartFunc of S,T; ::_thesis: for seq being sequence of S for r being Real st h is total holds (r (#) h) /* seq = r * (h /* seq) let seq be sequence of S; ::_thesis: for r being Real st h is total holds (r (#) h) /* seq = r * (h /* seq) let r be Real; ::_thesis: ( h is total implies (r (#) h) /* seq = r * (h /* seq) ) assume h is total ; ::_thesis: (r (#) h) /* seq = r * (h /* seq) then dom h = the carrier of S by PARTFUN1:def_2; then rng seq c= dom h ; hence (r (#) h) /* seq = r * (h /* seq) by NFCONT_1:13; ::_thesis: verum end; theorem Th27: :: NDIFF_1:27 for T, S being non trivial RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) proof let T, S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) let f be PartFunc of S,T; ::_thesis: for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) let x0 be Point of S; ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) by NFCONT_1:def_5; ::_thesis: ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 ) assume that A1: x0 in dom f and A2: for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ; ::_thesis: f is_continuous_in x0 thus x0 in dom f by A1; :: according to NFCONT_1:def_5 ::_thesis: for b1 being Element of K6(K7(NAT, the carrier of S)) holds ( not rng b1 c= dom f or not b1 is convergent or not lim b1 = x0 or ( f /* b1 is convergent & f /. x0 = lim (f /* b1) ) ) let s2 be sequence of S; ::_thesis: ( not rng s2 c= dom f or not s2 is convergent or not lim s2 = x0 or ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ) assume that A3: rng s2 c= dom f and A4: ( s2 is convergent & lim s2 = x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) now__::_thesis:_(_f_/*_s2_is_convergent_&_f_/._x0_=_lim_(f_/*_s2)_) percases ( ex n being Element of NAT st for m being Element of NAT st n <= m holds s2 . m = x0 or for n being Element of NAT ex m being Element of NAT st ( n <= m & s2 . m <> x0 ) ) ; suppose ex n being Element of NAT st for m being Element of NAT st n <= m holds s2 . m = x0 ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) then consider N being Element of NAT such that A5: for m being Element of NAT st N <= m holds s2 . m = x0 ; A6: for n being Element of NAT holds (s2 ^\ N) . n = x0 proof let n be Element of NAT ; ::_thesis: (s2 ^\ N) . n = x0 s2 . (n + N) = x0 by A5, NAT_1:12; hence (s2 ^\ N) . n = x0 by NAT_1:def_3; ::_thesis: verum end; A7: rng (s2 ^\ N) c= rng s2 by VALUED_0:21; A8: now__::_thesis:_for_p_being_Real_st_p_>_0_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((f_/*_(s2_^\_N))_._m)_-_(f_/._x0)).||_<_p let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p ) assume A9: p > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p ) assume n <= m ; ::_thesis: ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A3, A7, FUNCT_2:109, XBOOLE_1:1 .= ||.((f /. x0) - (f /. x0)).|| by A6 .= ||.(0. T).|| by RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A9; ::_thesis: verum end; then A10: f /* (s2 ^\ N) is convergent by NORMSP_1:def_6; A11: f /* (s2 ^\ N) = (f /* s2) ^\ N by A3, VALUED_0:27; then A12: f /* s2 is convergent by A10, LOPBAN_3:10; f /. x0 = lim ((f /* s2) ^\ N) by A8, A10, A11, NORMSP_1:def_7; hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A12, LOPBAN_3:9; ::_thesis: verum end; supposeA13: for n being Element of NAT ex m being Element of NAT st ( n <= m & s2 . m <> x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) defpred S1[ Element of NAT , set , set ] means for n, m being Element of NAT st $2 = n & $3 = m holds ( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds m <= k ) ); defpred S2[ Nat] means s2 . $1 <> x0; ex m1 being Element of NAT st ( 0 <= m1 & s2 . m1 <> x0 ) by A13; then A14: ex m being Nat st S2[m] ; consider M being Nat such that A15: ( S2[M] & ( for n being Nat st S2[n] holds M <= n ) ) from NAT_1:sch_5(A14); reconsider M9 = M as Element of NAT by ORDINAL1:def_12; A16: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_ (_n_<_m_&_s2_._m_<>_x0_) let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n < m & s2 . m <> x0 ) consider m being Element of NAT such that A17: ( n + 1 <= m & s2 . m <> x0 ) by A13; take m = m; ::_thesis: ( n < m & s2 . m <> x0 ) thus ( n < m & s2 . m <> x0 ) by A17, NAT_1:13; ::_thesis: verum end; A18: for n, x being Element of NAT ex y being Element of NAT st S1[n,x,y] proof let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S1[n,x,y] defpred S3[ Nat] means ( x < $1 & s2 . $1 <> x0 ); ex m being Element of NAT st S3[m] by A16; then A19: ex m being Nat st S3[m] ; consider l being Nat such that A20: ( S3[l] & ( for k being Nat st S3[k] holds l <= k ) ) from NAT_1:sch_5(A19); reconsider l = l as Element of NAT by ORDINAL1:def_12; take l ; ::_thesis: S1[n,x,l] thus S1[n,x,l] by A20; ::_thesis: verum end; consider F being Function of NAT,NAT such that A21: ( F . 0 = M9 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A18); A22: rng F c= REAL by XBOOLE_1:1; A23: rng F c= NAT ; A24: dom F = NAT by FUNCT_2:def_1; then reconsider F = F as Real_Sequence by A22, RELSET_1:4; A25: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_Element_of_NAT let n be Element of NAT ; ::_thesis: F . n is Element of NAT F . n in rng F by A24, FUNCT_1:def_3; hence F . n is Element of NAT by A23; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_<_F_._(n_+_1) let n be Element of NAT ; ::_thesis: F . n < F . (n + 1) ( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A25; hence F . n < F . (n + 1) by A21; ::_thesis: verum end; then reconsider F = F as V37() sequence of NAT by SEQM_3:def_6; A26: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A4, LOPBAN_3:7, LOPBAN_3:8; A27: for n being Element of NAT st s2 . n <> x0 holds ex m being Element of NAT st F . m = n proof defpred S3[ Nat] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) ); assume ex n being Element of NAT st S3[n] ; ::_thesis: contradiction then A28: ex n being Nat st S3[n] ; consider M1 being Nat such that A29: ( S3[M1] & ( for n being Nat st S3[n] holds M1 <= n ) ) from NAT_1:sch_5(A28); defpred S4[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 ); A30: ex n being Nat st S4[n] proof take M ; ::_thesis: S4[M] ( M <= M1 & M <> M1 ) by A15, A21, A29; hence M < M1 by XXREAL_0:1; ::_thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M ) thus s2 . M <> x0 by A15; ::_thesis: ex m being Element of NAT st F . m = M take 0 ; ::_thesis: F . 0 = M thus F . 0 = M by A21; ::_thesis: verum end; A31: for n being Nat st S4[n] holds n <= M1 ; consider MX being Nat such that A32: ( S4[MX] & ( for n being Nat st S4[n] holds n <= MX ) ) from NAT_1:sch_6(A31, A30); A33: for k being Element of NAT st MX < k & k < M1 holds s2 . k = x0 proof given k being Element of NAT such that A34: MX < k and A35: ( k < M1 & s2 . k <> x0 ) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ; suppose ex m being Element of NAT st F . m = k ; ::_thesis: contradiction hence contradiction by A32, A34, A35; ::_thesis: verum end; suppose for m being Element of NAT holds F . m <> k ; ::_thesis: contradiction hence contradiction by A29, A35; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; consider m being Element of NAT such that A36: F . m = MX by A32; A37: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A21, A36; M1 in NAT by ORDINAL1:def_12; then A38: F . (m + 1) <= M1 by A21, A29, A32, A36; now__::_thesis:_not_F_._(m_+_1)_<>_M1 assume F . (m + 1) <> M1 ; ::_thesis: contradiction then F . (m + 1) < M1 by A38, XXREAL_0:1; hence contradiction by A33, A37; ::_thesis: verum end; hence contradiction by A29; ::_thesis: verum end; A39: for n being Element of NAT holds (s2 * F) . n <> x0 proof defpred S3[ Element of NAT ] means (s2 * F) . $1 <> x0; A40: for k being Element of NAT st S3[k] holds S3[k + 1] proof let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] ) assume (s2 * F) . k <> x0 ; ::_thesis: S3[k + 1] S1[k,F . k,F . (k + 1)] by A21; then s2 . (F . (k + 1)) <> x0 ; hence S3[k + 1] by FUNCT_2:15; ::_thesis: verum end; A41: S3[ 0 ] by A15, A21, FUNCT_2:15; thus for n being Element of NAT holds S3[n] from NAT_1:sch_1(A41, A40); ::_thesis: verum end; A42: rng (s2 * F) c= rng s2 by VALUED_0:21; then rng (s2 * F) c= dom f by A3, XBOOLE_1:1; then A43: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A2, A39, A26; A44: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ ||.(((f_/*_s2)_._m)_-_(f_/._x0)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.(((f /* s2) . m) - (f /. x0)).|| < p ) assume A45: 0 < p ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.(((f /* s2) . m) - (f /. x0)).|| < p then consider n being Element of NAT such that A46: for m being Element of NAT st n <= m holds ||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A43, NORMSP_1:def_7; take k = F . n; ::_thesis: for m being Element of NAT st k <= m holds ||.(((f /* s2) . m) - (f /. x0)).|| < p let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((f /* s2) . m) - (f /. x0)).|| < p ) assume A47: k <= m ; ::_thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p now__::_thesis:_||.(((f_/*_s2)_._m)_-_(f_/._x0)).||_<_p percases ( s2 . m = x0 or s2 . m <> x0 ) ; supposeA48: s2 . m = x0 ; ::_thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p ||.(((f /* s2) . m) - (f /. x0)).|| = ||.((f /. (s2 . m)) - (f /. x0)).|| by A3, FUNCT_2:109 .= ||.(0. T).|| by A48, RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A45; ::_thesis: verum end; suppose s2 . m <> x0 ; ::_thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p then consider l being Element of NAT such that A49: m = F . l by A27; n <= l by A47, A49, SEQM_3:1; then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A46; then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A3, A42, FUNCT_2:109, XBOOLE_1:1; then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A49, FUNCT_2:15; hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A3, FUNCT_2:109; ::_thesis: verum end; end; end; hence ||.(((f /* s2) . m) - (f /. x0)).|| < p ; ::_thesis: verum end; hence f /* s2 is convergent by NORMSP_1:def_6; ::_thesis: f /. x0 = lim (f /* s2) hence f /. x0 = lim (f /* s2) by A44, NORMSP_1:def_7; ::_thesis: verum end; end; end; hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ; ::_thesis: verum end; theorem Th28: :: NDIFF_1:28 for T, S being non trivial RealNormSpace for R1, R2 being RestFunc of S,T holds ( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T ) proof let T, S be non trivial RealNormSpace; ::_thesis: for R1, R2 being RestFunc of S,T holds ( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T ) let R1, R2 be RestFunc of S,T; ::_thesis: ( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T ) A1: ( R1 is total & R2 is total ) by Def5; A2: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_((R1_+_R2)_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_((R1_+_R2)_/*_h))_=_0._T_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) ((R1 + R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T ) A3: ( (||.h.|| ") (#) (R1 /* h) is convergent & (||.h.|| ") (#) (R2 /* h) is convergent ) by Def5; A4: (||.h.|| ") (#) ((R1 + R2) /* h) = (||.h.|| ") (#) ((R1 /* h) + (R2 /* h)) by A1, Th25 .= ((||.h.|| ") (#) (R1 /* h)) + ((||.h.|| ") (#) (R2 /* h)) by Th9 ; hence (||.h.|| ") (#) ((R1 + R2) /* h) is convergent by A3, NORMSP_1:19; ::_thesis: lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T ( lim ((||.h.|| ") (#) (R1 /* h)) = 0. T & lim ((||.h.|| ") (#) (R2 /* h)) = 0. T ) by Def5; hence lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = (0. T) + (0. T) by A3, A4, NORMSP_1:25 .= 0. T by RLVECT_1:4 ; ::_thesis: verum end; A5: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_((R1_-_R2)_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_((R1_-_R2)_/*_h))_=_0._T_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) ((R1 - R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T ) A6: ( (||.h.|| ") (#) (R1 /* h) is convergent & (||.h.|| ") (#) (R2 /* h) is convergent ) by Def5; A7: (||.h.|| ") (#) ((R1 - R2) /* h) = (||.h.|| ") (#) ((R1 /* h) - (R2 /* h)) by A1, Th25 .= ((||.h.|| ") (#) (R1 /* h)) - ((||.h.|| ") (#) (R2 /* h)) by Th12 ; hence (||.h.|| ") (#) ((R1 - R2) /* h) is convergent by A6, NORMSP_1:20; ::_thesis: lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T ( lim ((||.h.|| ") (#) (R1 /* h)) = 0. T & lim ((||.h.|| ") (#) (R2 /* h)) = 0. T ) by Def5; hence lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = (0. T) - (0. T) by A6, A7, NORMSP_1:26 .= 0. T by RLVECT_1:13 ; ::_thesis: verum end; R1 + R2 is total by A1, VFUNCT_1:32; hence R1 + R2 is RestFunc of S,T by A2, Def5; ::_thesis: R1 - R2 is RestFunc of S,T R1 - R2 is total by A1, VFUNCT_1:32; hence R1 - R2 is RestFunc of S,T by A5, Def5; ::_thesis: verum end; theorem Th29: :: NDIFF_1:29 for T, S being non trivial RealNormSpace for r being Real for R being RestFunc of S,T holds r (#) R is RestFunc of S,T proof let T, S be non trivial RealNormSpace; ::_thesis: for r being Real for R being RestFunc of S,T holds r (#) R is RestFunc of S,T let r be Real; ::_thesis: for R being RestFunc of S,T holds r (#) R is RestFunc of S,T let R be RestFunc of S,T; ::_thesis: r (#) R is RestFunc of S,T A1: R is total by Def5; A2: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_((r_(#)_R)_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_((r_(#)_R)_/*_h))_=_0._T_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) ((r (#) R) /* h) is convergent & lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T ) A3: (||.h.|| ") (#) (R /* h) is convergent by Def5; A4: (||.h.|| ") (#) ((r (#) R) /* h) = (||.h.|| ") (#) (r * (R /* h)) by A1, Th26 .= r * ((||.h.|| ") (#) (R /* h)) by Th10 ; hence (||.h.|| ") (#) ((r (#) R) /* h) is convergent by A3, NORMSP_1:22; ::_thesis: lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T lim ((||.h.|| ") (#) (R /* h)) = 0. T by Def5; hence lim ((||.h.|| ") (#) ((r (#) R) /* h)) = r * (0. T) by A3, A4, NORMSP_1:28 .= 0. T by RLVECT_1:10 ; ::_thesis: verum end; r (#) R is total by A1, VFUNCT_1:34; hence r (#) R is RestFunc of S,T by A2, Def5; ::_thesis: verum end; definition let S, T be non trivial RealNormSpace; let f be PartFunc of S,T; let x0 be Point of S; predf is_differentiable_in x0 means :Def6: :: NDIFF_1:def 6 ex N being Neighbourhood of x0 st ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ); end; :: deftheorem Def6 defines is_differentiable_in NDIFF_1:def_6_:_ for S, T being non trivial RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ); definition let S, T be non trivial RealNormSpace; let f be PartFunc of S,T; let x0 be Point of S; assume A1: f is_differentiable_in x0 ; func diff (f,x0) -> Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def7: :: NDIFF_1:def 7 ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (it . (x - x0)) + (R /. (x - x0)) ); existence ex b1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (b1 . (x - x0)) + (R /. (x - x0)) ) proof consider N being Neighbourhood of x0 such that A2: N c= dom f and A3: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6; consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that A4: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3; take L ; ::_thesis: ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) thus ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A2, A4; ::_thesis: verum end; uniqueness for b1, b2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (b1 . (x - x0)) + (R /. (x - x0)) ) & ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (b2 . (x - x0)) + (R /. (x - x0)) ) holds b1 = b2 proof let LB, LB1 be Point of (R_NormSpace_of_BoundedLinearOperators (S,T)); ::_thesis: ( ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) ) & ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) ) implies LB = LB1 ) A5: 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 = LB as Element of BoundedLinearOperators (S,T) ; reconsider L1 = LB1 as Element of BoundedLinearOperators (S,T) by A5; assume that A6: ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) ) and A7: ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) ) ; ::_thesis: LB = LB1 consider N being Neighbourhood of x0 such that N c= dom f and A8: ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) by A6; consider R being RestFunc of S,T such that A9: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) by A8; consider N1 being Neighbourhood of x0 such that N1 c= dom f and A10: ex R being RestFunc of S,T st for x being Point of S st x in N1 holds (f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) by A7; consider R1 being RestFunc of S,T such that A11: for x being Point of S st x in N1 holds (f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R1 /. (x - x0)) by A10; A12: for z being Point of S holds (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z proof let z be Point of S; ::_thesis: (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z now__::_thesis:_(_(_z_=_0._S_&_(modetrans_(L,S,T))_._z_=_(modetrans_(L1,S,T))_._z_)_or_(_z_<>_0._S_&_(modetrans_(L,S,T))_._z_=_(modetrans_(L1,S,T))_._z_)_) percases ( z = 0. S or z <> 0. S ) ; caseA13: z = 0. S ; ::_thesis: (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z hence (modetrans (L,S,T)) . z = (modetrans (L,S,T)) . (0 * z) by RLVECT_1:10 .= 0 * ((modetrans (L,S,T)) . z) by LOPBAN_1:def_5 .= 0. T by RLVECT_1:10 .= 0 * ((modetrans (L1,S,T)) . z) by RLVECT_1:10 .= (modetrans (L1,S,T)) . (0 * z) by LOPBAN_1:def_5 .= (modetrans (L1,S,T)) . z by A13, RLVECT_1:10 ; ::_thesis: verum end; caseA14: z <> 0. S ; ::_thesis: (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z consider N0 being Neighbourhood of x0 such that A15: ( N0 c= N & N0 c= N1 ) by Th1; consider g being Real such that A16: 0 < g and A17: { 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 A18: ||.z.|| / g < n0 by SEQ_4:3; set n1 = n0 + 1; A19: 0 <= n0 by NAT_1:2; n0 <= n0 + 1 by NAT_1:11; then ||.z.|| / g < n0 + 1 by A18, XXREAL_0:2; then (||.z.|| / g) * g < (n0 + 1) * g by A16, XREAL_1:68; then ||.z.|| < (n0 + 1) * g by A16, XCMPLX_1:87; then A20: ||.z.|| / (n0 + 1) < g by A19, XREAL_1:83; ex r being Real_Sequence st ( ( for n being Element of NAT holds ( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ) & r is convergent & lim r = 0 ) proof deffunc H1( Element of NAT ) -> Element of REAL = 1 / ($1 + (n0 + 1)); consider r being Real_Sequence such that A21: for n being Element of NAT holds r . n = H1(n) from SEQ_1:sch_1(); take r ; ::_thesis: ( ( for n being Element of NAT holds ( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ) & r is convergent & lim r = 0 ) thus for n being Element of NAT holds ( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ::_thesis: ( r is convergent & lim r = 0 ) proof let n be Element of NAT ; ::_thesis: ( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) thus r . n = 1 / (n + (n0 + 1)) by A21; ::_thesis: ( r . n > 0 & ((r . n) * z) + x0 in N0 ) ( n0 + 1 <= n + (n0 + 1) & 0 <= ||.z.|| ) by NAT_1:12, NORMSP_1:4; then A22: ||.z.|| / (n + (n0 + 1)) <= ||.z.|| / (n0 + 1) by A19, XREAL_1:118; 0 <= n by NAT_1:2; then 0 < 1 * ((n + (n0 + 1)) ") by A19; then A23: 0 < 1 / (n + (n0 + 1)) by XCMPLX_0:def_9; hence r . n > 0 by A21; ::_thesis: ((r . n) * z) + x0 in N0 ||.((((r . n) * z) + x0) - x0).|| = ||.(((r . n) * z) + (x0 - x0)).|| by RLVECT_1:def_3 .= ||.(((r . n) * z) + (0. S)).|| by RLVECT_1:15 .= ||.((r . n) * z).|| by RLVECT_1:4 .= ||.((1 / (n + (n0 + 1))) * z).|| by A21 .= (abs (1 / (n + (n0 + 1)))) * ||.z.|| by NORMSP_1:def_1 .= (1 / (n + (n0 + 1))) * ||.z.|| by A23, ABSVALUE:def_1 .= ||.z.|| / (n + (n0 + 1)) by XCMPLX_1:99 ; then ||.((((r . n) * z) + x0) - x0).|| < g by A20, A22, XXREAL_0:2; then ((r . n) * z) + x0 in { y where y is Point of S : ||.(y - x0).|| < g } ; hence ((r . n) * z) + x0 in N0 by A17; ::_thesis: verum end; thus r is convergent by A21, NAT_1:2, SEQ_4:28; ::_thesis: lim r = 0 thus lim r = 0 by A21, NAT_1:2, SEQ_4:29; ::_thesis: verum end; then consider r being Real_Sequence such that A24: for n being Element of NAT holds ( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) and r is convergent and lim r = 0 ; deffunc H1( Element of NAT ) -> Element of the carrier of S = (r . $1) * z; consider s being sequence of S such that A25: for n being Element of NAT holds s . n = H1(n) from FUNCT_2:sch_4(); now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s_._n_=_0._S let n be Element of NAT ; ::_thesis: not s . n = 0. S assume s . n = 0. S ; ::_thesis: contradiction then (r . n) * z = 0. S by A25; then ( r . n = 0 or z = 0. S ) by RLVECT_1:11; hence contradiction by A14, A24; ::_thesis: verum end; then A26: s is non-zero by Th7; now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_=_(1_/_(n_+_(n0_+_1)))_*_z let n be Element of NAT ; ::_thesis: s . n = (1 / (n + (n0 + 1))) * z thus s . n = (r . n) * z by A25 .= (1 / (n + (n0 + 1))) * z by A24 ; ::_thesis: verum end; then ( s is convergent & lim s = 0. S ) by A19, Th19, Th20; then reconsider s = s as non-zero 0. S -convergent sequence of S by A26, Def4; A27: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N_&_x_in_N1_holds_ (L_._(x_-_x0))_+_(R_/._(x_-_x0))_=_(L1_._(x_-_x0))_+_(R1_/._(x_-_x0)) let x be Point of S; ::_thesis: ( x in N & x in N1 implies (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) ) assume that A28: x in N and A29: x in N1 ; ::_thesis: (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A9, A28; hence (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A11, A29; ::_thesis: verum end; now__::_thesis:_for_n_being_Nat_holds_(L_._z)_-_(L1_._z)_=_(||.z.||_*_(((||.s.||_")_(#)_(R1_/*_s))_-_((||.s.||_")_(#)_(R_/*_s))))_._n R1 is total by Def5; then dom R1 = the carrier of S by PARTFUN1:def_2; then A30: rng s c= dom R1 ; R is total by Def5; then dom R = the carrier of S by PARTFUN1:def_2; then A31: rng s c= dom R ; let n be Nat; ::_thesis: (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . n set x = ((r . n) * z) + x0; A32: (((r . n) * z) + x0) - x0 = ((r . n) * z) + (x0 - x0) by RLVECT_1:def_3 .= ((r . n) * z) + (0. S) by RLVECT_1:15 .= (r . n) * z by RLVECT_1:4 ; A33: n in NAT by ORDINAL1:def_12; then A34: r . n <> 0 by A24; s . n <> 0. S by A33, Th7; then A35: ||.(s . n).|| <> 0 by NORMSP_0:def_5; A36: r . n > 0 by A24, A33; ||.(s . n).|| = ||.((r . n) * z).|| by A25, A33 .= (abs (r . n)) * ||.z.|| by NORMSP_1:def_1 .= (r . n) * ||.z.|| by A36, ABSVALUE:def_1 ; then ((r . n) ") * ||.(s . n).|| = (((r . n) ") * (r . n)) * ||.z.|| .= ((r . n) / (r . n)) * ||.z.|| by XCMPLX_0:def_9 .= 1 * ||.z.|| by A34, XCMPLX_1:60 .= ||.z.|| ; then ||.z.|| * (||.(s . n).|| ") = ((r . n) ") * (||.(s . n).|| * (||.(s . n).|| ")) .= ((r . n) ") * (||.(s . n).|| / ||.(s . n).||) by XCMPLX_0:def_9 .= ((r . n) ") * 1 by A35, XCMPLX_1:60 .= (r . n) " ; then A37: ||.z.|| * ((||.s.|| . n) ") = (r . n) " by A33, NORMSP_0:def_4; ((r . n) * z) + x0 in N0 by A24, A33; then (L . ((r . n) * z)) + (R /. ((r . n) * z)) = (L1 . ((r . n) * z)) + (R1 /. ((r . n) * z)) by A27, A15, A32; then A38: (((r . n) ") * (L . ((r . n) * z))) + (((r . n) ") * (R /. ((r . n) * z))) = ((r . n) ") * ((L1 . ((r . n) * z)) + (R1 /. ((r . n) * z))) by RLVECT_1:def_5; A39: ((r . n) ") * (L1 . ((r . n) * z)) = ((r . n) ") * ((modetrans (L1,S,T)) . ((r . n) * z)) by LOPBAN_1:def_11 .= ((r . n) ") * ((r . n) * ((modetrans (L1,S,T)) . z)) by LOPBAN_1:def_5 .= ((r . n) ") * ((r . n) * (L1 . z)) by LOPBAN_1:def_11 .= (((r . n) ") * (r . n)) * (L1 . z) by RLVECT_1:def_7 .= ((r . n) / (r . n)) * (L1 . z) by XCMPLX_0:def_9 .= 1 * (L1 . z) by A34, XCMPLX_1:60 .= L1 . z by RLVECT_1:def_8 ; ((r . n) ") * (L . ((r . n) * z)) = ((r . n) ") * ((modetrans (L,S,T)) . ((r . n) * z)) by LOPBAN_1:def_11 .= ((r . n) ") * ((r . n) * ((modetrans (L,S,T)) . z)) by LOPBAN_1:def_5 .= ((r . n) ") * ((r . n) * (L . z)) by LOPBAN_1:def_11 .= (((r . n) ") * (r . n)) * (L . z) by RLVECT_1:def_7 .= ((r . n) / (r . n)) * (L . z) by XCMPLX_0:def_9 .= 1 * (L . z) by A34, XCMPLX_1:60 .= L . z by RLVECT_1:def_8 ; then A40: (L . z) + (((r . n) ") * (R /. ((r . n) * z))) = (L1 . z) + (((r . n) ") * (R1 /. ((r . n) * z))) by A38, A39, RLVECT_1:def_5; A41: ((r . n) ") * (R1 /. ((r . n) * z)) = ((r . n) ") * (R1 /. (s . n)) by A25, A33 .= (||.z.|| * ((||.s.|| ") . n)) * (R1 /. (s . n)) by A37, VALUED_1:10 .= ||.z.|| * (((||.s.|| ") . n) * (R1 /. (s . n))) by RLVECT_1:def_7 .= ||.z.|| * (((||.s.|| ") . n) * ((R1 /* s) . n)) by A33, A30, FUNCT_2:109 .= ||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n) by A33, Def2 ; ((r . n) ") * (R /. ((r . n) * z)) = ((r . n) ") * (R /. (s . n)) by A25, A33 .= (||.z.|| * ((||.s.|| ") . n)) * (R /. (s . n)) by A37, VALUED_1:10 .= ||.z.|| * (((||.s.|| ") . n) * (R /. (s . n))) by RLVECT_1:def_7 .= ||.z.|| * (((||.s.|| ") . n) * ((R /* s) . n)) by A33, A31, FUNCT_2:109 .= ||.z.|| * (((||.s.|| ") (#) (R /* s)) . n) by A33, Def2 ; then (L . z) + ((||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by A40, A41, RLVECT_1:def_3; then (L . z) + (0. T) = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:15; then L . z = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:def_4; then (L . z) - (L1 . z) = (- (L1 . z)) + ((L1 . z) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)))) by RLVECT_1:def_3; then (L . z) - (L1 . z) = ((- (L1 . z)) + (L1 . z)) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) by RLVECT_1:def_3; then (L . z) - (L1 . z) = (0. T) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) by RLVECT_1:5; then (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:4; then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| ") (#) (R1 /* s)) . n) - (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:34; then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) . n) by A33, NORMSP_1:def_3; hence (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . n by A33, NORMSP_1:def_5; ::_thesis: verum end; then ( ||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) is constant & (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . 1 = (L . z) - (L1 . z) ) by VALUED_0:def_18; then A42: lim (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) = (L . z) - (L1 . z) by Th18; A43: ( (||.s.|| ") (#) (R /* s) is convergent & (||.s.|| ") (#) (R1 /* s) is convergent ) by Def5; ( lim ((||.s.|| ") (#) (R /* s)) = 0. T & lim ((||.s.|| ") (#) (R1 /* s)) = 0. T ) by Def5; then A44: lim (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) = (0. T) - (0. T) by A43, NORMSP_1:26 .= 0. T by RLVECT_1:13 ; A45: lim (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) = ||.z.|| * (lim (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) by A43, NORMSP_1:20, NORMSP_1:28 .= 0. T by A44, RLVECT_1:10 ; thus (modetrans (L,S,T)) . z = L . z by LOPBAN_1:def_11 .= L1 . z by A42, A45, RLVECT_1:21 .= (modetrans (L1,S,T)) . z by LOPBAN_1:def_11 ; ::_thesis: verum end; end; end; hence (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z ; ::_thesis: verum end; thus LB = modetrans (L,S,T) by LOPBAN_1:def_11 .= modetrans (L1,S,T) by A12, FUNCT_2:63 .= LB1 by LOPBAN_1:def_11 ; ::_thesis: verum end; end; :: deftheorem Def7 defines diff NDIFF_1:def_7_:_ for S, T 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 b5 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) holds ( b5 = diff (f,x0) iff ex N being Neighbourhood of x0 st ( N c= dom f & ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (b5 . (x - x0)) + (R /. (x - x0)) ) ); definition let X be set ; let S, T be non trivial RealNormSpace; let f be PartFunc of S,T; predf is_differentiable_on X means :Def8: :: NDIFF_1:def 8 ( X c= dom f & ( for x being Point of S st x in X holds f | X is_differentiable_in x ) ); end; :: deftheorem Def8 defines is_differentiable_on NDIFF_1:def_8_:_ for X being set for S, T being non trivial RealNormSpace for f being PartFunc of S,T holds ( f is_differentiable_on X iff ( X c= dom f & ( for x being Point of S st x in X holds f | X is_differentiable_in x ) ) ); theorem Th30: :: NDIFF_1:30 for X being set for S, T being non trivial RealNormSpace for f being PartFunc of S,T st f is_differentiable_on X holds X is Subset of S proof let X be set ; ::_thesis: for S, T being non trivial RealNormSpace for f being PartFunc of S,T st f is_differentiable_on X holds X is Subset of S let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_differentiable_on X holds X is Subset of S let f be PartFunc of S,T; ::_thesis: ( f is_differentiable_on X implies X is Subset of S ) assume f is_differentiable_on X ; ::_thesis: X is Subset of S then X c= dom f by Def8; hence X is Subset of S by XBOOLE_1:1; ::_thesis: verum end; theorem Th31: :: NDIFF_1:31 for S, T being non trivial RealNormSpace for f being PartFunc of S,T for Z being Subset of S st Z is open holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) ) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T for Z being Subset of S st Z is open holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) ) ) let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) ) ) let Z be Subset of S; ::_thesis: ( Z is open implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) ) ) ) assume A1: Z is open ; ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) ) ) thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) implies f is_differentiable_on Z ) proof assume A2: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds f is_differentiable_in x ) ) hence A3: Z c= dom f by Def8; ::_thesis: for x being Point of S st x in Z holds f is_differentiable_in x let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A4: x0 in Z ; ::_thesis: f is_differentiable_in x0 then f | Z is_differentiable_in x0 by A2, Def8; then consider N being Neighbourhood of x0 such that A5: N c= dom (f | Z) and A6: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6; consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that A7: for x being Point of S st x in N holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6; take N ; :: according to NDIFF_1:def_6 ::_thesis: ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A8: dom (f | Z) = (dom f) /\ Z by RELAT_1:61; then dom (f | Z) c= dom f by XBOOLE_1:17; hence N c= dom f by A5, XBOOLE_1:1; ::_thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) take L ; ::_thesis: ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) take R ; ::_thesis: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) assume A9: x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A7; then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5, A8, A9, PARTFUN2:16; hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, PARTFUN2:17; ::_thesis: verum end; assume that A10: Z c= dom f and A11: for x being Point of S st x in Z holds f is_differentiable_in x ; ::_thesis: f is_differentiable_on Z thus Z c= dom f by A10; :: according to NDIFF_1:def_8 ::_thesis: for x being Point of S st x in Z holds f | Z is_differentiable_in x let x0 be Point of S; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 ) assume A12: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0 then consider N1 being Neighbourhood of x0 such that A13: N1 c= Z by A1, Th2; f is_differentiable_in x0 by A11, A12; then consider N being Neighbourhood of x0 such that A14: N c= dom f and A15: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6; consider N2 being Neighbourhood of x0 such that A16: N2 c= N1 and A17: N2 c= N by Th1; A18: N2 c= Z by A13, A16, XBOOLE_1:1; take N2 ; :: according to NDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) N2 c= dom f by A14, A17, XBOOLE_1:1; then A19: N2 c= (dom f) /\ Z by A18, XBOOLE_1:19; hence N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) A20: x0 in N2 by NFCONT_1:4; consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that A21: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A15; take L ; ::_thesis: ex R being RestFunc of S,T st for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) take R ; ::_thesis: for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) let x be Point of S; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) assume A22: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A17, A21; then ((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A22, PARTFUN2:16; hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A20, PARTFUN2:16; ::_thesis: verum end; theorem :: NDIFF_1:32 for S, T being non trivial RealNormSpace for f being PartFunc of S,T for Y being Subset of S st f is_differentiable_on Y holds Y is open proof let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T for Y being Subset of S st f is_differentiable_on Y holds Y is open let f be PartFunc of S,T; ::_thesis: for Y being Subset of S st f is_differentiable_on Y holds Y is open let Y be Subset of S; ::_thesis: ( f is_differentiable_on Y implies Y is open ) assume A1: f is_differentiable_on Y ; ::_thesis: Y is open now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Y_holds_ ex_N_being_Neighbourhood_of_x0_st_N_c=_Y let x0 be Point of S; ::_thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y ) assume x0 in Y ; ::_thesis: ex N being Neighbourhood of x0 st N c= Y then f | Y is_differentiable_in x0 by A1, Def8; then consider N being Neighbourhood of x0 such that A2: N c= dom (f | Y) and ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds ((f | Y) /. x) - ((f | Y) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6; take N = N; ::_thesis: N c= Y dom (f | Y) = (dom f) /\ Y by RELAT_1:61; then dom (f | Y) c= Y by XBOOLE_1:17; hence N c= Y by A2, XBOOLE_1:1; ::_thesis: verum end; hence Y is open by Th4; ::_thesis: verum end; definition let S, T be non trivial RealNormSpace; let f be PartFunc of S,T; let X be set ; assume A1: f is_differentiable_on X ; funcf `| X -> PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def9: :: NDIFF_1:def 9 ( dom it = X & ( for x being Point of S st x in X holds it /. x = diff (f,x) ) ); existence ex b1 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st ( dom b1 = X & ( for x being Point of S st x in X holds b1 /. x = diff (f,x) ) ) proof deffunc H1( Point of S) -> Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) = diff (f,$1); defpred S1[ Point of S] means $1 in X; consider F being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) such that A2: ( ( for x being Point of S holds ( x in dom F iff S1[x] ) ) & ( for x being Point of S st x in dom F holds F . x = H1(x) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = X & ( for x being Point of S st x in X holds F /. x = diff (f,x) ) ) now__::_thesis:_for_y_being_set_st_y_in_X_holds_ y_in_dom_F A3: X is Subset of S by A1, Th30; let y be set ; ::_thesis: ( y in X implies y in dom F ) assume y in X ; ::_thesis: y in dom F hence y in dom F by A2, A3; ::_thesis: verum end; then A4: X c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in X by A2; then dom F c= X by TARSKI:def_3; hence dom F = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Point of S st x in X holds F /. x = diff (f,x) now__::_thesis:_for_x_being_Point_of_S_st_x_in_X_holds_ F_/._x_=_diff_(f,x) let x be Point of S; ::_thesis: ( x in X implies F /. x = diff (f,x) ) assume x in X ; ::_thesis: F /. x = diff (f,x) then A5: x in dom F by A2; then F . x = diff (f,x) by A2; hence F /. x = diff (f,x) by A5, PARTFUN1:def_6; ::_thesis: verum end; hence for x being Point of S st x in X holds F /. x = diff (f,x) ; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st dom b1 = X & ( for x being Point of S st x in X holds b1 /. x = diff (f,x) ) & dom b2 = X & ( for x being Point of S st x in X holds b2 /. x = diff (f,x) ) holds b1 = b2 proof let F, G be PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)); ::_thesis: ( dom F = X & ( for x being Point of S st x in X holds F /. x = diff (f,x) ) & dom G = X & ( for x being Point of S st x in X holds G /. x = diff (f,x) ) implies F = G ) assume that A6: dom F = X and A7: for x being Point of S st x in X holds F /. x = diff (f,x) and A8: dom G = X and A9: for x being Point of S st x in X holds G /. x = diff (f,x) ; ::_thesis: F = G now__::_thesis:_for_x_being_Point_of_S_st_x_in_dom_F_holds_ F_/._x_=_G_/._x let x be Point of S; ::_thesis: ( x in dom F implies F /. x = G /. x ) assume A10: x in dom F ; ::_thesis: F /. x = G /. x then F /. x = diff (f,x) by A6, A7; hence F /. x = G /. x by A6, A9, A10; ::_thesis: verum end; hence F = G by A6, A8, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem Def9 defines `| NDIFF_1:def_9_:_ for S, T being non trivial RealNormSpace for f being PartFunc of S,T for X being set st f is_differentiable_on X holds for b5 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) holds ( b5 = f `| X iff ( dom b5 = X & ( for x being Point of S st x in X holds b5 /. x = diff (f,x) ) ) ); theorem :: NDIFF_1:33 for S, T being non trivial RealNormSpace for f being PartFunc of S,T for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & ex r being Point of T st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) ) assume that A1: Z is open and A2: Z c= dom f ; ::_thesis: ( for r being Point of T holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) ) reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ; set L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)); given r being Point of T such that A3: rng f = {r} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (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 L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) as Element of BoundedLinearOperators (S,T) ; A4: dom R = the carrier of S by FUNCOP_1:13; A5: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._T_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T ) A6: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._T let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. T A7: R /. (h . n) = R . (h . n) by A4, PARTFUN1:def_6 .= 0. T by FUNCOP_1:7 ; A8: rng h c= dom R by A4; A9: n in NAT by ORDINAL1:def_12; hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2 .= ((||.h.|| ") . n) * (R /. (h . n)) by A9, A8, FUNCT_2:109 .= 0. T by A7, RLVECT_1:10 ; ::_thesis: verum end; then A10: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18; hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. T ((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A6; hence lim ((||.h.|| ") (#) (R /* h)) = 0. T by A10, Th18; ::_thesis: verum end; A11: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_dom_f_holds_ f_/._x0_=_r let x0 be Point of S; ::_thesis: ( x0 in dom f implies f /. x0 = r ) assume A12: x0 in dom f ; ::_thesis: f /. x0 = r then f . x0 in {r} by A3, FUNCT_1:def_3; then f /. x0 in {r} by A12, PARTFUN1:def_6; hence f /. x0 = r by TARSKI:def_1; ::_thesis: verum end; reconsider R = R as RestFunc of S,T by A5, Def5; A13: the carrier of S --> (0. T) = L by LOPBAN_1:31; A14: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A15: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A16: N c= Z by A1, Th2; A17: N c= dom f by A2, A16, XBOOLE_1:1; for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A18: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6 .= 0. T by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = r - (f /. x0) by A11, A17 .= r - r by A2, A11, A15 .= 0. T by RLVECT_1:15 .= (0. T) + (0. T) by RLVECT_1:4 .= (L . (x - x0)) + (R /. (x - x0)) by A13, A18, FUNCOP_1:7 ; ::_thesis: verum end; hence f is_differentiable_in x0 by A17, Def6; ::_thesis: verum end; hence A19: f is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) assume A20: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) then A21: f is_differentiable_in x0 by A14; then ex N being Neighbourhood of x0 st ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by Def6; then consider N being Neighbourhood of x0 such that A22: N c= dom f ; A23: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A24: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6 .= 0. T by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = r - (f /. x0) by A11, A22 .= r - r by A2, A11, A20 .= 0. T by RLVECT_1:15 .= (0. T) + (0. T) by RLVECT_1:4 .= (L . (x - x0)) + (R /. (x - x0)) by A13, A24, FUNCOP_1:7 ; ::_thesis: verum end; thus (f `| Z) /. x0 = diff (f,x0) by A19, A20, Def9 .= 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) by A21, A22, A23, Def7 ; ::_thesis: verum end; registration let S be non trivial RealNormSpace; let h be non-zero 0. S -convergent sequence of S; let n be Element of NAT ; clusterh ^\ n -> non-zero 0. S -convergent for sequence of S; coherence for b1 being sequence of S st b1 = h ^\ n holds ( b1 is 0. S -convergent & b1 is non-zero ) proof A1: h ^\ n is non-zero by Th17; A2: h is convergent by Def4; lim h = 0. S by Def4; then A3: lim (h ^\ n) = 0. S by A2, LOPBAN_3:9; h ^\ n is convergent by A2, LOPBAN_3:9; hence for b1 being sequence of S st b1 = h ^\ n holds ( b1 is 0. S -convergent & b1 is non-zero ) by A1, A3, Def4; ::_thesis: verum end; end; theorem Th34: :: NDIFF_1:34 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 f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0. b1 -convergent sequence of S for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) 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 f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0. S -convergent sequence of S for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) let f be PartFunc of S,T; ::_thesis: for x0 being Point of S for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0. S -convergent sequence of S for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) let x0 be Point of S; ::_thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0. S -convergent sequence of S for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) let N be Neighbourhood of x0; ::_thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0. S -convergent sequence of S for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) ) assume that A1: f is_differentiable_in x0 and A2: N c= dom f ; ::_thesis: for h being non-zero 0. S -convergent sequence of S for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) let h be non-zero 0. S -convergent sequence of S; ::_thesis: for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) let c be constant sequence of S; ::_thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) ) assume that A3: rng c = {x0} and A4: rng (h + c) c= N ; ::_thesis: ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) consider N1 being Neighbourhood of x0 such that N1 c= dom f and A5: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N1 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6; consider N2 being Neighbourhood of x0 such that A6: N2 c= N and A7: N2 c= N1 by Th1; consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that A8: for x being Point of S st x in N1 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5; consider g being Real such that A9: 0 < g and A10: { y where y is Point of S : ||.(y - x0).|| < g } c= N2 by NFCONT_1:def_1; A11: x0 in N2 by NFCONT_1:4; ex n being Element of NAT st ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) proof c . 0 in rng c by NFCONT_1:6; then c . 0 = x0 by A3, TARSKI:def_1; then A12: lim c = x0 by Th18; A13: ( c is convergent & h is convergent ) by Def4, Th18; then A14: h + c is convergent by NORMSP_1:19; lim h = 0. S by Def4; then lim (h + c) = (0. S) + x0 by A12, A13, NORMSP_1:25 .= x0 by RLVECT_1:4 ; then consider n being Element of NAT such that A15: for m being Element of NAT st n <= m holds ||.(((h + c) . m) - x0).|| < g by A9, A14, NORMSP_1:def_7; take n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) A16: rng (c ^\ n) = {x0} by A3, VALUED_0:26; thus rng (c ^\ n) c= N2 ::_thesis: rng ((h + c) ^\ n) c= N2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in N2 ) assume y in rng (c ^\ n) ; ::_thesis: y in N2 hence y in N2 by A11, A16, TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in N2 ) assume y in rng ((h + c) ^\ n) ; ::_thesis: y in N2 then consider m being Element of NAT such that A17: y = ((h + c) ^\ n) . m by NFCONT_1:6; reconsider y1 = y as Point of S by A17; 0 <= m by NAT_1:2; then n + 0 <= n + m by XREAL_1:7; then ||.(((h + c) . (n + m)) - x0).|| < g by A15; then ||.((((h + c) ^\ n) . m) - x0).|| < g by NAT_1:def_3; then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A17; hence y in N2 by A10; ::_thesis: verum end; then consider n being Element of NAT such that rng (c ^\ n) c= N2 and A18: rng ((h + c) ^\ n) c= N2 ; A19: lim (h ^\ n) = 0. S by Def4; A20: for k being Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) proof let k be Element of NAT ; ::_thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) ((h + c) ^\ n) . k in rng ((h + c) ^\ n) by NFCONT_1:6; then A21: ((h + c) ^\ n) . k in N2 by A18; ( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by NFCONT_1:6, VALUED_0:26; then A22: (c ^\ n) . k = x0 by A3, TARSKI:def_1; (((h + c) ^\ n) . k) - ((c ^\ n) . k) = ((h + c) . (k + n)) - ((c ^\ n) . k) by NAT_1:def_3 .= ((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k) by NORMSP_1:def_2 .= (((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k) by NAT_1:def_3 .= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by NAT_1:def_3 .= ((h ^\ n) . k) + (((c ^\ n) . k) - ((c ^\ n) . k)) by RLVECT_1:def_3 .= ((h ^\ n) . k) + (0. S) by RLVECT_1:15 .= (h ^\ n) . k by RLVECT_1:4 ; hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A8, A7, A21, A22; ::_thesis: verum end; 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 = L as Element of BoundedLinearOperators (S,T) ; reconsider LP = modetrans (L,S,T) as PartFunc of S,T ; A23: lim (R /* (h ^\ n)) = 0. T by Th24; A24: rng ((h + c) ^\ n) c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in dom f ) assume y in rng ((h + c) ^\ n) ; ::_thesis: y in dom f then y in N2 by A18; then y in N by A6; hence y in dom f by A2; ::_thesis: verum end; R is total by Def5; then dom R = the carrier of S by PARTFUN1:def_2; then A25: rng (h ^\ n) c= dom R ; A26: rng (c ^\ n) c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom f ) assume A27: y in rng (c ^\ n) ; ::_thesis: y in dom f rng (c ^\ n) = rng c by VALUED_0:26; then y = x0 by A3, A27, TARSKI:def_1; then y in N by NFCONT_1:4; hence y in dom f by A2; ::_thesis: verum end; A28: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def_1; then A29: rng (h ^\ n) c= dom (modetrans (L,S,T)) ; now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_/*_((h_+_c)_^\_n))_-_(f_/*_(c_^\_n)))_._k_=_((LP_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k let k be Element of NAT ; ::_thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by NORMSP_1:def_3 .= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A24, FUNCT_2:109 .= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A26, FUNCT_2:109 .= (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A20 .= ((modetrans (L,S,T)) . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by LOPBAN_1:def_11 .= (LP /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A28, PARTFUN1:def_6 .= ((LP /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by A29, FUNCT_2:109 .= ((LP /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A25, FUNCT_2:109 .= ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def_2 ; ::_thesis: verum end; then A30: (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (LP /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63; A31: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def_1; LP is_Lipschitzian_on the carrier of S proof thus the carrier of S c= dom LP by FUNCT_2:def_1; :: according to NFCONT_1:def_9 ::_thesis: ex b1 being Element of REAL st ( not b1 <= 0 & ( for b2, b3 being Element of the carrier of S holds ( not b2 in the carrier of S or not b3 in the carrier of S or ||.((LP /. b2) - (LP /. b3)).|| <= b1 * ||.(b2 - b3).|| ) ) ) set LL = modetrans (L,S,T); consider K being Real such that A32: 0 <= K and A33: for x being VECTOR of S holds ||.((modetrans (L,S,T)) . x).|| <= K * ||.x.|| by LOPBAN_1:def_8; take K + 1 ; ::_thesis: ( not K + 1 <= 0 & ( for b1, b2 being Element of the carrier of S holds ( not b1 in the carrier of S or not b2 in the carrier of S or ||.((LP /. b1) - (LP /. b2)).|| <= (K + 1) * ||.(b1 - b2).|| ) ) ) A34: 0 + K < 1 + K by XREAL_1:8; now__::_thesis:_for_x1,_x2_being_Point_of_S_st_x1_in_the_carrier_of_S_&_x2_in_the_carrier_of_S_holds_ ||.((LP_/._x1)_-_(LP_/._x2)).||_<=_(K_+_1)_*_||.(x1_-_x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in the carrier of S & x2 in the carrier of S implies ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| ) assume that x1 in the carrier of S and x2 in the carrier of S ; ::_thesis: ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| A35: ||.((modetrans (L,S,T)) . (x1 - x2)).|| <= K * ||.(x1 - x2).|| by A33; 0 <= ||.(x1 - x2).|| by NORMSP_1:4; then A36: K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A34, XREAL_1:64; ||.((LP /. x1) - (LP /. x2)).|| = ||.(((modetrans (L,S,T)) . x1) - (LP /. x2)).|| by A31, PARTFUN1:def_6 .= ||.(((modetrans (L,S,T)) . x1) + (- ((modetrans (L,S,T)) . x2))).|| by A31, PARTFUN1:def_6 .= ||.(((modetrans (L,S,T)) . x1) + ((- 1) * ((modetrans (L,S,T)) . x2))).|| by RLVECT_1:16 .= ||.(((modetrans (L,S,T)) . x1) + ((modetrans (L,S,T)) . ((- 1) * x2))).|| by LOPBAN_1:def_5 .= ||.((modetrans (L,S,T)) . (x1 + ((- 1) * x2))).|| by VECTSP_1:def_20 .= ||.((modetrans (L,S,T)) . (x1 - x2)).|| by RLVECT_1:16 ; hence ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| by A35, A36, XXREAL_0:2; ::_thesis: verum end; hence ( not K + 1 <= 0 & ( for b1, b2 being Element of the carrier of S holds ( not b1 in the carrier of S or not b2 in the carrier of S or ||.((LP /. b1) - (LP /. b2)).|| <= (K + 1) * ||.(b1 - b2).|| ) ) ) by A32; ::_thesis: verum end; then A37: LP is_continuous_on the carrier of S by NFCONT_1:45; A38: rng c c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in dom f ) assume y in rng c ; ::_thesis: y in dom f then y = x0 by A3, TARSKI:def_1; then y in N by NFCONT_1:4; hence y in dom f by A2; ::_thesis: verum end; A39: ( h ^\ n is convergent & rng (h ^\ n) c= the carrier of S ) by Def4; then A40: LP /* (h ^\ n) is convergent by A37, A19, NFCONT_1:18; A41: R /* (h ^\ n) is convergent by Th24; then A42: (LP /* (h ^\ n)) + (R /* (h ^\ n)) is convergent by A40, NORMSP_1:19; LP /. (0. S) = (modetrans (L,S,T)) . (0. S) by A31, PARTFUN1:def_6 .= (modetrans (L,S,T)) . (0 * (0. S)) by RLVECT_1:10 .= 0 * ((modetrans (L,S,T)) . (0. S)) by LOPBAN_1:def_5 .= 0. T by RLVECT_1:10 ; then lim (LP /* (h ^\ n)) = 0. T by A37, A39, A19, NFCONT_1:18; then lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = (0. T) + (0. T) by A41, A23, A40, NORMSP_1:25; then A43: lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = 0. T by RLVECT_1:4; rng (h + c) c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom f ) assume y in rng (h + c) ; ::_thesis: y in dom f then y in N by A4; hence y in dom f by A2; ::_thesis: verum end; then (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = ((f /* (h + c)) ^\ n) - (f /* (c ^\ n)) by VALUED_0:27 .= ((f /* (h + c)) ^\ n) - ((f /* c) ^\ n) by A38, VALUED_0:27 .= ((f /* (h + c)) - (f /* c)) ^\ n by Th16 ; hence ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) by A30, A42, A43, LOPBAN_3:10, LOPBAN_3:11; ::_thesis: verum end; theorem Th35: :: NDIFF_1:35 for T, S being non trivial RealNormSpace for f1, f2 being PartFunc of S,T for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) proof let T, S be non trivial RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) let f1, f2 be PartFunc of S,T; ::_thesis: for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) let x0 be Point of S; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) ) assume that A1: f1 is_differentiable_in x0 and A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) consider N1 being Neighbourhood of x0 such that A3: N1 c= dom f1 and A4: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N1 holds (f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6; consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that A5: for x being Point of S st x in N1 holds (f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4; consider N2 being Neighbourhood of x0 such that A6: N2 c= dom f2 and A7: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N2 holds (f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def6; consider L2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R2 being RestFunc of S,T such that A8: for x being Point of S st x in N2 holds (f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7; reconsider R = R1 + R2 as RestFunc of S,T by Th28; set L = L1 + L2; consider N being Neighbourhood of x0 such that A9: N c= N1 and A10: N c= N2 by Th1; A11: N c= dom f2 by A6, A10, XBOOLE_1:1; N c= dom f1 by A3, A9, XBOOLE_1:1; then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27; then A12: N c= dom (f1 + f2) by VFUNCT_1:def_1; A13: ( R1 is total & R2 is total ) by Def5; A14: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N_holds_ ((f1_+_f2)_/._x)_-_((f1_+_f2)_/._x0)_=_((L1_+_L2)_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Point of S; ::_thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((L1 + L2) . (x - x0)) + (R /. (x - x0)) ) A15: x0 in N by NFCONT_1:4; assume A16: x in N ; ::_thesis: ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((L1 + L2) . (x - x0)) + (R /. (x - x0)) hence ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0) by A12, VFUNCT_1:def_1 .= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A12, A15, VFUNCT_1:def_1 .= (((f1 /. x) + (f2 /. x)) - (f1 /. x0)) - (f2 /. x0) by RLVECT_1:27 .= (((f1 /. x) + (- (f1 /. x0))) + (f2 /. x)) - (f2 /. x0) by RLVECT_1:def_3 .= ((f1 /. x) - (f1 /. x0)) + ((f2 /. x) - (f2 /. x0)) by RLVECT_1:def_3 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A9, A16 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A10, A16 .= (((R1 /. (x - x0)) + (L1 . (x - x0))) + (L2 . (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3 .= (((L1 . (x - x0)) + (L2 . (x - x0))) + (R1 /. (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3 .= ((L1 . (x - x0)) + (L2 . (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by RLVECT_1:def_3 .= ((L1 + L2) . (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by LOPBAN_1:35 .= ((L1 + L2) . (x - x0)) + (R /. (x - x0)) by A13, VFUNCT_1:37 ; ::_thesis: verum end; hence f1 + f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) hence diff ((f1 + f2),x0) = L1 + L2 by A12, A14, Def7 .= (diff (f1,x0)) + L2 by A1, A3, A5, Def7 .= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def7 ; ::_thesis: verum end; theorem Th36: :: NDIFF_1:36 for T, S being non trivial RealNormSpace for f1, f2 being PartFunc of S,T for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) proof let T, S be non trivial RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) let f1, f2 be PartFunc of S,T; ::_thesis: for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) let x0 be Point of S; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) ) assume that A1: f1 is_differentiable_in x0 and A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) consider N1 being Neighbourhood of x0 such that A3: N1 c= dom f1 and A4: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N1 holds (f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6; consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that A5: for x being Point of S st x in N1 holds (f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4; consider N2 being Neighbourhood of x0 such that A6: N2 c= dom f2 and A7: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N2 holds (f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def6; consider L2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R2 being RestFunc of S,T such that A8: for x being Point of S st x in N2 holds (f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7; reconsider R = R1 - R2 as RestFunc of S,T by Th28; set L = L1 - L2; consider N being Neighbourhood of x0 such that A9: N c= N1 and A10: N c= N2 by Th1; A11: N c= dom f2 by A6, A10, XBOOLE_1:1; N c= dom f1 by A3, A9, XBOOLE_1:1; then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27; then A12: N c= dom (f1 - f2) by VFUNCT_1:def_2; A13: ( R1 is total & R2 is total ) by Def5; A14: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N_holds_ ((f1_-_f2)_/._x)_-_((f1_-_f2)_/._x0)_=_((L1_-_L2)_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Point of S; ::_thesis: ( x in N implies ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0)) ) A15: x0 in N by NFCONT_1:4; assume A16: x in N ; ::_thesis: ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0)) hence ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0) by A12, VFUNCT_1:def_2 .= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A12, A15, VFUNCT_1:def_2 .= (((f1 /. x) - (f2 /. x)) - (f1 /. x0)) + (f2 /. x0) by RLVECT_1:29 .= ((f1 /. x) - ((f1 /. x0) + (f2 /. x))) + (f2 /. x0) by RLVECT_1:27 .= (((f1 /. x) - (f1 /. x0)) - (f2 /. x)) + (f2 /. x0) by RLVECT_1:27 .= ((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0)) by RLVECT_1:29 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0)) by A5, A9, A16 .= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A10, A16 .= (((L1 . (x - x0)) + (R1 /. (x - x0))) - (L2 . (x - x0))) - (R2 /. (x - x0)) by RLVECT_1:27 .= ((L1 . (x - x0)) + ((R1 /. (x - x0)) + (- (L2 . (x - x0))))) - (R2 /. (x - x0)) by RLVECT_1:def_3 .= ((L1 . (x - x0)) - ((L2 . (x - x0)) - (R1 /. (x - x0)))) - (R2 /. (x - x0)) by RLVECT_1:33 .= (((L1 . (x - x0)) - (L2 . (x - x0))) + (R1 /. (x - x0))) - (R2 /. (x - x0)) by RLVECT_1:29 .= ((L1 . (x - x0)) - (L2 . (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by RLVECT_1:def_3 .= ((L1 - L2) . (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by LOPBAN_1:40 .= ((L1 - L2) . (x - x0)) + (R /. (x - x0)) by A13, VFUNCT_1:37 ; ::_thesis: verum end; hence f1 - f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) hence diff ((f1 - f2),x0) = L1 - L2 by A12, A14, Def7 .= (diff (f1,x0)) - L2 by A1, A3, A5, Def7 .= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def7 ; ::_thesis: verum end; theorem Th37: :: NDIFF_1:37 for T, S being non trivial RealNormSpace for r being Real for f being PartFunc of S,T for x0 being Point of S st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) proof let T, S be non trivial RealNormSpace; ::_thesis: for r being Real for f being PartFunc of S,T for x0 being Point of S st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) let r be Real; ::_thesis: for f being PartFunc of S,T for x0 being Point of S st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) let x0 be Point of S; ::_thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) ) assume A1: f is_differentiable_in x0 ; ::_thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) then consider N1 being Neighbourhood of x0 such that A2: N1 c= dom f and A3: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N1 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6; consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that A4: for x being Point of S st x in N1 holds (f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A3; reconsider R = r (#) R1 as RestFunc of S,T by Th29; set L = r * L1; A5: N1 c= dom (r (#) f) by A2, VFUNCT_1:def_4; A6: R1 is total by Def5; A7: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N1_holds_ ((r_(#)_f)_/._x)_-_((r_(#)_f)_/._x0)_=_((r_*_L1)_._(x_-_x0))_+_(R_/._(x_-_x0)) let x be Point of S; ::_thesis: ( x in N1 implies ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0)) ) A8: x0 in N1 by NFCONT_1:4; assume A9: x in N1 ; ::_thesis: ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0)) hence ((r (#) f) /. x) - ((r (#) f) /. x0) = (r * (f /. x)) - ((r (#) f) /. x0) by A5, VFUNCT_1:def_4 .= (r * (f /. x)) - (r * (f /. x0)) by A5, A8, VFUNCT_1:def_4 .= r * ((f /. x) - (f /. x0)) by RLVECT_1:34 .= r * ((L1 . (x - x0)) + (R1 /. (x - x0))) by A4, A9 .= (r * (L1 . (x - x0))) + (r * (R1 /. (x - x0))) by RLVECT_1:def_5 .= ((r * L1) . (x - x0)) + (r * (R1 /. (x - x0))) by LOPBAN_1:36 .= ((r * L1) . (x - x0)) + (R /. (x - x0)) by A6, VFUNCT_1:39 ; ::_thesis: verum end; hence r (#) f is_differentiable_in x0 by A5, Def6; ::_thesis: diff ((r (#) f),x0) = r * (diff (f,x0)) hence diff ((r (#) f),x0) = r * L1 by A5, A7, Def7 .= r * (diff (f,x0)) by A1, A2, A4, Def7 ; ::_thesis: verum end; theorem :: NDIFF_1:38 for S being non trivial RealNormSpace for f being PartFunc of S,S for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = id the carrier of S ) ) proof let S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,S for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = id the carrier of S ) ) set L = id the carrier of S; ( R_NormSpace_of_BoundedLinearOperators (S,S) = NORMSTR(# (BoundedLinearOperators (S,S)),(Zero_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Add_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Mult_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(BoundedLinearOperatorsNorm (S,S)) #) & id the carrier of S is Lipschitzian LinearOperator of S,S ) by LOPBAN_1:def_14, LOPBAN_2:3; then reconsider L = id the carrier of S as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) by LOPBAN_1:def_9; let f be PartFunc of S,S; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = id the carrier of S ) ) let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = id the carrier of S ) ) ) assume A1: Z is open ; ::_thesis: ( not Z c= dom f or not f | Z = id Z or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = id the carrier of S ) ) ) reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ; A2: dom R = the carrier of S by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._S_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. S ) A3: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._S let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. S A4: R /. (h . n) = R . (h . n) by A2, PARTFUN1:def_6 .= 0. S by FUNCOP_1:7 ; A5: rng h c= dom R by A2; A6: n in NAT by ORDINAL1:def_12; hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2 .= ((||.h.|| ") . n) * (R /. (h . n)) by A6, A5, FUNCT_2:109 .= 0. S by A4, RLVECT_1:10 ; ::_thesis: verum end; then A7: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18; hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. S ((||.h.|| ") (#) (R /* h)) . 0 = 0. S by A3; hence lim ((||.h.|| ") (#) (R /* h)) = 0. S by A7, Th18; ::_thesis: verum end; then reconsider R = R as RestFunc of S,S by Def5; assume that A8: Z c= dom f and A9: f | Z = id Z ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = id the carrier of S ) ) A10: now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_ f_/._x_=_x let x be Point of S; ::_thesis: ( x in Z implies f /. x = x ) assume A11: x in Z ; ::_thesis: f /. x = x then (f | Z) . x = x by A9, FUNCT_1:18; then f . x = x by A11, FUNCT_1:49; hence f /. x = x by A8, A11, PARTFUN1:def_6; ::_thesis: verum end; A12: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A13: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A14: N c= Z by A1, Th2; A15: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A16: R /. (x - x0) = R . (x - x0) by A2, PARTFUN1:def_6 .= 0. S by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A14 .= x - x0 by A10, A13 .= L . (x - x0) by FUNCT_1:17 .= (L . (x - x0)) + (R /. (x - x0)) by A16, RLVECT_1:4 ; ::_thesis: verum end; N c= dom f by A8, A14, XBOOLE_1:1; hence f is_differentiable_in x0 by A15, Def6; ::_thesis: verum end; hence A17: f is_differentiable_on Z by A1, A8, Th31; ::_thesis: for x being Point of S st x in Z holds (f `| Z) /. x = id the carrier of S let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = id the carrier of S ) assume A18: x0 in Z ; ::_thesis: (f `| Z) /. x0 = id the carrier of S then consider N1 being Neighbourhood of x0 such that A19: N1 c= Z by A1, Th2; A20: f is_differentiable_in x0 by A12, A18; then ex N being Neighbourhood of x0 st ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) ex R being RestFunc of S,S st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by Def6; then consider N being Neighbourhood of x0 such that A21: N c= dom f ; consider N2 being Neighbourhood of x0 such that A22: N2 c= N1 and A23: N2 c= N by Th1; A24: N2 c= dom f by A21, A23, XBOOLE_1:1; A25: for x being Point of S st x in N2 holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N2 implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A26: R /. (x - x0) = R . (x - x0) by A2, PARTFUN1:def_6 .= 0. S by FUNCOP_1:7 ; assume x in N2 ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then x in N1 by A22; hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A19 .= x - x0 by A10, A18 .= L . (x - x0) by FUNCT_1:17 .= (L . (x - x0)) + (R /. (x - x0)) by A26, RLVECT_1:4 ; ::_thesis: verum end; thus (f `| Z) /. x0 = diff (f,x0) by A17, A18, Def9 .= id the carrier of S by A20, A24, A25, Def7 ; ::_thesis: verum end; theorem :: NDIFF_1:39 for S, T being non trivial RealNormSpace for Z being Subset of S st Z is open holds for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for Z being Subset of S st Z is open holds for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) let Z be Subset of S; ::_thesis: ( Z is open implies for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) ) assume A1: Z is open ; ::_thesis: for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) let f1, f2 be PartFunc of S,T; ::_thesis: ( Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) ) assume that A2: Z c= dom (f1 + f2) and A3: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_ f1_+_f2_is_differentiable_in_x0 let x0 be Point of S; ::_thesis: ( x0 in Z implies f1 + f2 is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: f1 + f2 is_differentiable_in x0 then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, A3, Th31; hence f1 + f2 is_differentiable_in x0 by Th35; ::_thesis: verum end; hence A4: f1 + f2 is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_ ((f1_+_f2)_`|_Z)_/._x_=_(diff_(f1,x))_+_(diff_(f2,x)) let x be Point of S; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) assume A5: x in Z ; ::_thesis: ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) then A6: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A1, A3, Th31; thus ((f1 + f2) `| Z) /. x = diff ((f1 + f2),x) by A4, A5, Def9 .= (diff (f1,x)) + (diff (f2,x)) by A6, Th35 ; ::_thesis: verum end; hence for x being Point of S st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ; ::_thesis: verum end; theorem :: NDIFF_1:40 for S, T being non trivial RealNormSpace for Z being Subset of S st Z is open holds for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for Z being Subset of S st Z is open holds for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) let Z be Subset of S; ::_thesis: ( Z is open implies for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) ) assume A1: Z is open ; ::_thesis: for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) let f1, f2 be PartFunc of S,T; ::_thesis: ( Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) ) assume that A2: Z c= dom (f1 - f2) and A3: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_ f1_-_f2_is_differentiable_in_x0 let x0 be Point of S; ::_thesis: ( x0 in Z implies f1 - f2 is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: f1 - f2 is_differentiable_in x0 then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, A3, Th31; hence f1 - f2 is_differentiable_in x0 by Th36; ::_thesis: verum end; hence A4: f1 - f2 is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_ ((f1_-_f2)_`|_Z)_/._x_=_(diff_(f1,x))_-_(diff_(f2,x)) let x be Point of S; ::_thesis: ( x in Z implies ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) assume A5: x in Z ; ::_thesis: ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) then A6: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A1, A3, Th31; thus ((f1 - f2) `| Z) /. x = diff ((f1 - f2),x) by A4, A5, Def9 .= (diff (f1,x)) - (diff (f2,x)) by A6, Th36 ; ::_thesis: verum end; hence for x being Point of S st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ; ::_thesis: verum end; theorem :: NDIFF_1:41 for S, T being non trivial RealNormSpace for Z being Subset of S st Z is open holds for r being Real for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for Z being Subset of S st Z is open holds for r being Real for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) let Z be Subset of S; ::_thesis: ( Z is open implies for r being Real for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) ) assume A1: Z is open ; ::_thesis: for r being Real for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) let r be Real; ::_thesis: for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) let f be PartFunc of S,T; ::_thesis: ( Z c= dom (r (#) f) & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) ) assume that A2: Z c= dom (r (#) f) and A3: f is_differentiable_on Z ; ::_thesis: ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_ r_(#)_f_is_differentiable_in_x0 let x0 be Point of S; ::_thesis: ( x0 in Z implies r (#) f is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: r (#) f is_differentiable_in x0 then f is_differentiable_in x0 by A1, A3, Th31; hence r (#) f is_differentiable_in x0 by Th37; ::_thesis: verum end; hence A4: r (#) f is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_ ((r_(#)_f)_`|_Z)_/._x_=_r_*_(diff_(f,x)) let x be Point of S; ::_thesis: ( x in Z implies ((r (#) f) `| Z) /. x = r * (diff (f,x)) ) assume A5: x in Z ; ::_thesis: ((r (#) f) `| Z) /. x = r * (diff (f,x)) then A6: f is_differentiable_in x by A1, A3, Th31; thus ((r (#) f) `| Z) /. x = diff ((r (#) f),x) by A4, A5, Def9 .= r * (diff (f,x)) by A6, Th37 ; ::_thesis: verum end; hence for x being Point of S st x in Z holds ((r (#) f) `| Z) /. x = r * (diff (f,x)) ; ::_thesis: verum end; theorem :: NDIFF_1:42 for S, T being non trivial RealNormSpace for f being PartFunc of S,T for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) proof let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) ) assume A1: Z is open ; ::_thesis: ( not Z c= dom f or not f | Z is constant or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) ) reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ; set L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)); assume that A2: Z c= dom f and A3: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (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 L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) as Element of BoundedLinearOperators (S,T) ; A4: dom R = the carrier of S by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._T_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T ) A5: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._T let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. T A6: R /. (h . n) = R . (h . n) by A4, PARTFUN1:def_6 .= 0. T by FUNCOP_1:7 ; A7: rng h c= dom R by A4; A8: n in NAT by ORDINAL1:def_12; hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2 .= ((||.h.|| ") . n) * (R /. (h . n)) by A8, A7, FUNCT_2:109 .= 0. T by A6, RLVECT_1:10 ; ::_thesis: verum end; then A9: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18; hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. T ((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A5; hence lim ((||.h.|| ") (#) (R /* h)) = 0. T by A9, Th18; ::_thesis: verum end; then reconsider R = R as RestFunc of S,T by Def5; consider r being Point of T such that A10: for x being Point of S st x in Z /\ (dom f) holds f . x = r by A3, PARTFUN2:57; A11: now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_/\_(dom_f)_holds_ f_/._x_=_r let x be Point of S; ::_thesis: ( x in Z /\ (dom f) implies f /. x = r ) assume A12: x in Z /\ (dom f) ; ::_thesis: f /. x = r Z /\ (dom f) c= dom f by XBOOLE_1:17; hence f /. x = f . x by A12, PARTFUN1:def_6 .= r by A10, A12 ; ::_thesis: verum end; A13: the carrier of S --> (0. T) = L by LOPBAN_1:31; A14: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A15: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A16: N c= Z by A1, Th2; A17: N c= dom f by A2, A16, XBOOLE_1:1; A18: x0 in Z /\ (dom f) by A2, A15, XBOOLE_0:def_4; for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A19: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6 .= 0. T by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then x in Z /\ (dom f) by A16, A17, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = r - (f /. x0) by A11 .= r - r by A11, A18 .= 0. T by RLVECT_1:15 .= (0. T) + (0. T) by RLVECT_1:4 .= (L . (x - x0)) + (R /. (x - x0)) by A13, A19, FUNCOP_1:7 ; ::_thesis: verum end; hence f is_differentiable_in x0 by A17, Def6; ::_thesis: verum end; hence A20: f is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds (f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) assume A21: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) then consider N being Neighbourhood of x0 such that A22: N c= Z by A1, Th2; A23: N c= dom f by A2, A22, XBOOLE_1:1; A24: x0 in Z /\ (dom f) by A2, A21, XBOOLE_0:def_4; A25: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A26: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6 .= 0. T by FUNCOP_1:7 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) then x in Z /\ (dom f) by A22, A23, XBOOLE_0:def_4; hence (f /. x) - (f /. x0) = r - (f /. x0) by A11 .= r - r by A11, A24 .= 0. T by RLVECT_1:15 .= (0. T) + (0. T) by RLVECT_1:4 .= (L . (x - x0)) + (R /. (x - x0)) by A13, A26, FUNCOP_1:7 ; ::_thesis: verum end; A27: f is_differentiable_in x0 by A14, A21; thus (f `| Z) /. x0 = diff (f,x0) by A20, A21, Def9 .= 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) by A27, A23, A25, Def7 ; ::_thesis: verum end; theorem :: NDIFF_1:43 for S being non trivial RealNormSpace for f being PartFunc of S,S for r being Real for p being Point of S for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds f /. x = (r * x) + p ) holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) proof let S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,S for r being Real for p being Point of S for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds f /. x = (r * x) + p ) holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) let f be PartFunc of S,S; ::_thesis: for r being Real for p being Point of S for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds f /. x = (r * x) + p ) holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) let r be Real; ::_thesis: for p being Point of S for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds f /. x = (r * x) + p ) holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) let p be Point of S; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds f /. x = (r * x) + p ) holds ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & ( for x being Point of S st x in Z holds f /. x = (r * x) + p ) implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) ) assume A1: Z is open ; ::_thesis: ( not Z c= dom f or ex x being Point of S st ( x in Z & not f /. x = (r * x) + p ) or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) ) A2: R_NormSpace_of_BoundedLinearOperators (S,S) = NORMSTR(# (BoundedLinearOperators (S,S)),(Zero_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Add_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Mult_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(BoundedLinearOperatorsNorm (S,S)) #) by LOPBAN_1:def_14; then reconsider II = FuncUnit S as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) ; set L = r * II; reconsider L = r * II as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) ; reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ; assume that A3: Z c= dom f and A4: for x being Point of S st x in Z holds f /. x = (r * x) + p ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) ) ) A5: L = r * (FuncUnit S) by A2, LOPBAN_2:def_3; A6: dom R = the carrier of S by FUNCOP_1:13; now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_ (_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._S_) let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. S ) A7: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._S let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. S A8: R /. (h . n) = R . (h . n) by A6, PARTFUN1:def_6 .= 0. S by FUNCOP_1:7 ; A9: rng h c= dom R by A6; A10: n in NAT by ORDINAL1:def_12; hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2 .= ((||.h.|| ") . n) * (R /. (h . n)) by A10, A9, FUNCT_2:109 .= 0. S by A8, RLVECT_1:10 ; ::_thesis: verum end; then A11: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18; hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. S ((||.h.|| ") (#) (R /* h)) . 0 = 0. S by A7; hence lim ((||.h.|| ") (#) (R /* h)) = 0. S by A11, Th18; ::_thesis: verum end; then reconsider R = R as RestFunc of S,S by Def5; A12: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_ f_is_differentiable_in_x0 let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 ) assume A13: x0 in Z ; ::_thesis: f is_differentiable_in x0 then consider N being Neighbourhood of x0 such that A14: N c= Z by A1, Th2; A15: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A16: R /. (x - x0) = R . (x - x0) by A6, PARTFUN1:def_6 .= 0. S by FUNCOP_1:7 ; x - x0 = (id the carrier of S) . (x - x0) by FUNCT_1:17; then A17: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def_5 .= L . (x - x0) by LOPBAN_1:36 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A4, A14 .= ((r * x) + p) - ((r * x0) + p) by A4, A13 .= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def_3 .= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:27 .= (r * x) + ((p + (- (r * x0))) - p) .= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def_3 .= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:15 .= (r * x) - (r * x0) by RLVECT_1:4 .= r * (x - x0) by RLVECT_1:34 .= (L . (x - x0)) + (R /. (x - x0)) by A16, A17, RLVECT_1:4 ; ::_thesis: verum end; N c= dom f by A3, A14, XBOOLE_1:1; hence f is_differentiable_in x0 by A15, Def6; ::_thesis: verum end; hence A18: f is_differentiable_on Z by A1, A3, Th31; ::_thesis: for x being Point of S st x in Z holds (f `| Z) /. x = r * (FuncUnit S) let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = r * (FuncUnit S) ) assume A19: x0 in Z ; ::_thesis: (f `| Z) /. x0 = r * (FuncUnit S) then consider N being Neighbourhood of x0 such that A20: N c= Z by A1, Th2; A21: for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) A22: R /. (x - x0) = R . (x - x0) by A6, PARTFUN1:def_6 .= 0. S by FUNCOP_1:7 ; x - x0 = (id the carrier of S) . (x - x0) by FUNCT_1:17; then A23: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def_5 .= L . (x - x0) by LOPBAN_1:36 ; assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) hence (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A4, A20 .= ((r * x) + p) - ((r * x0) + p) by A4, A19 .= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def_3 .= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:27 .= (r * x) + ((p + (- (r * x0))) - p) .= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def_3 .= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:15 .= (r * x) - (r * x0) by RLVECT_1:4 .= r * (x - x0) by RLVECT_1:34 .= (L . (x - x0)) + (R /. (x - x0)) by A22, A23, RLVECT_1:4 ; ::_thesis: verum end; A24: N c= dom f by A3, A20, XBOOLE_1:1; A25: f is_differentiable_in x0 by A12, A19; thus (f `| Z) /. x0 = diff (f,x0) by A18, A19, Def9 .= r * (FuncUnit S) by A5, A25, A24, A21, Def7 ; ::_thesis: verum end; theorem Th44: :: NDIFF_1:44 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 f is_continuous_in x0 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 f is_continuous_in x0 let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st f is_differentiable_in x0 holds f is_continuous_in x0 let x0 be Point of S; ::_thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 ) assume A1: f is_differentiable_in x0 ; ::_thesis: f is_continuous_in x0 then consider N being Neighbourhood of x0 such that A2: N c= dom f and ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6; A3: now__::_thesis:_for_s1_being_sequence_of_S_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_=_x0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_x0_)_holds_ (_f_/*_s1_is_convergent_&_f_/._x0_=_lim_(f_/*_s1)_) consider g being Real such that A4: 0 < g and A5: { y where y is Point of S : ||.(y - x0).|| < g } c= N by NFCONT_1:def_1; reconsider s2 = NAT --> x0 as sequence of S ; let s1 be sequence of S; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) assume that A6: rng s1 c= dom f and A7: s1 is convergent and A8: lim s1 = x0 and A9: for n being Element of NAT holds s1 . n <> x0 ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) consider l being Element of NAT such that A10: for m being Element of NAT st l <= m holds ||.((s1 . m) - x0).|| < g by A7, A8, A4, NORMSP_1:def_7; deffunc H1( Element of NAT ) -> Element of the carrier of S = (s1 . $1) - (s2 . $1); consider s3 being sequence of S such that A11: for n being Element of NAT holds s3 . n = H1(n) from FUNCT_2:sch_4(); A12: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s3_._n_=_0._S given n being Element of NAT such that A13: s3 . n = 0. S ; ::_thesis: contradiction (s1 . n) - (s2 . n) = 0. S by A11, A13; then (s1 . n) - x0 = 0. S by FUNCOP_1:7; hence contradiction by A9, RLVECT_1:21; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(s3_^\_l)_._n_=_0._S given n being Element of NAT such that A14: (s3 ^\ l) . n = 0. S ; ::_thesis: contradiction s3 . (n + l) = 0. S by A14, NAT_1:def_3; hence contradiction by A12; ::_thesis: verum end; then A15: s3 ^\ l is non-zero by Th7; reconsider c = s2 ^\ l as constant sequence of S ; A16: s3 = s1 - s2 by A11, NORMSP_1:def_3; A17: s2 is convergent by Th18; then A18: s3 is convergent by A7, A16, NORMSP_1:20; then A19: s3 ^\ l is convergent by LOPBAN_3:9; lim s2 = s2 . 0 by Th18 .= x0 by FUNCOP_1:7 ; then lim s3 = x0 - x0 by A7, A8, A17, A16, NORMSP_1:26 .= 0. S by RLVECT_1:15 ; then lim (s3 ^\ l) = 0. S by A18, LOPBAN_3:9; then reconsider h = s3 ^\ l as non-zero 0. S -convergent sequence of S by A19, A15, Def4; now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_/*_(h_+_c))_-_(f_/*_c))_+_(f_/*_c))_._n_=_(f_/*_(h_+_c))_._n let n be Element of NAT ; ::_thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by NORMSP_1:def_2 .= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by NORMSP_1:def_3 .= ((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n)) by RLVECT_1:29 .= ((f /* (h + c)) . n) - (0. T) by RLVECT_1:15 .= (f /* (h + c)) . n by RLVECT_1:13 ; ::_thesis: verum end; then A20: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63; now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_+_c)_._n_=_(s1_^\_l)_._n let n be Element of NAT ; ::_thesis: (h + c) . n = (s1 ^\ l) . n thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A16, Th15 .= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3 .= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def_2 .= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def_3 .= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29 .= (s1 . (n + l)) - (0. S) by RLVECT_1:15 .= s1 . (l + n) by RLVECT_1:13 .= (s1 ^\ l) . n by NAT_1:def_3 ; ::_thesis: verum end; then A21: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A20, FUNCT_2:63 .= (f /* s1) ^\ l by A6, VALUED_0:27 ; A22: rng c = {x0} proof thus rng c c= {x0} :: according to XBOOLE_0:def_10 ::_thesis: {x0} c= rng c proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in {x0} ) assume y in rng c ; ::_thesis: y in {x0} then consider n being Element of NAT such that A23: y = (s2 ^\ l) . n by NFCONT_1:6; y = s2 . (n + l) by A23, NAT_1:def_3; then y = x0 by FUNCOP_1:7; hence y in {x0} by TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x0} or y in rng c ) assume y in {x0} ; ::_thesis: y in rng c then A24: y = x0 by TARSKI:def_1; c . 0 = s2 . (0 + l) by NAT_1:def_3 .= y by A24, FUNCOP_1:7 ; hence y in rng c by NFCONT_1:6; ::_thesis: verum end; A25: 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_ ||.(((f_/*_c)_._m)_-_(f_/._x0)).||_<_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 ||.(((f /* c) . m) - (f /. x0)).|| < p ) assume A26: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((f /* c) . m) - (f /. x0)).|| < p take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds ||.(((f /* c) . m) - (f /. x0)).|| < p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p ) assume n <= m ; ::_thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p x0 in N by NFCONT_1:4; then rng c c= dom f by A2, A22, ZFMISC_1:31; then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109 .= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def_3 .= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1:7 .= ||.(0. T).|| by RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A26; ::_thesis: verum end; then A27: f /* c is convergent by NORMSP_1:def_6; A28: rng (h + c) c= N proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in N ) assume A29: y in rng (h + c) ; ::_thesis: y in N then consider n being Element of NAT such that A30: y = (h + c) . n by NFCONT_1:6; reconsider y1 = y as Point of S by A29; (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A16, Th15 .= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3 .= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def_2 .= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def_3 .= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29 .= (s1 . (n + l)) - (0. S) by RLVECT_1:15 .= s1 . (l + n) by RLVECT_1:13 ; then ||.(((h + c) . n) - x0).|| < g by A10, NAT_1:12; then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A30; hence y in N by A5; ::_thesis: verum end; then A31: (f /* (h + c)) - (f /* c) is convergent by A1, A2, A22, Th34; then ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A27, NORMSP_1:19; hence f /* s1 is convergent by A21, LOPBAN_3:10; ::_thesis: f /. x0 = lim (f /* s1) A32: lim ((f /* (h + c)) - (f /* c)) = 0. T by A1, A2, A22, A28, Th34; lim (f /* c) = f /. x0 by A25, A27, NORMSP_1:def_7; then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. T) + (f /. x0) by A31, A32, A27, NORMSP_1:25 .= f /. x0 by RLVECT_1:4 ; hence f /. x0 = lim (f /* s1) by A31, A27, A21, LOPBAN_3:11, NORMSP_1:19; ::_thesis: verum end; x0 in N by NFCONT_1:4; hence f is_continuous_in x0 by A2, A3, Th27; ::_thesis: verum end; theorem :: NDIFF_1:45 for X being set for S, T being non trivial RealNormSpace for f being PartFunc of S,T st f is_differentiable_on X holds f is_continuous_on X proof let X be set ; ::_thesis: for S, T being non trivial RealNormSpace for f being PartFunc of S,T st f is_differentiable_on X holds f is_continuous_on X let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_differentiable_on X holds f is_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_differentiable_on X implies f is_continuous_on X ) assume A1: f is_differentiable_on X ; ::_thesis: f is_continuous_on X hence X c= dom f by Def8; :: according to NFCONT_1:def_7 ::_thesis: for b1 being Element of the carrier of S holds ( not b1 in X or f | X is_continuous_in b1 ) let x be Point of S; ::_thesis: ( not x in X or f | X is_continuous_in x ) assume x in X ; ::_thesis: f | X is_continuous_in x then f | X is_differentiable_in x by A1, Def8; hence f | X is_continuous_in x by Th44; ::_thesis: verum end; theorem :: NDIFF_1:46 for X being set for T, S being non trivial RealNormSpace for f being PartFunc of S,T for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds f is_differentiable_on Z proof let X be set ; ::_thesis: for T, S being non trivial RealNormSpace for f being PartFunc of S,T for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let T, S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let Z be Subset of S; ::_thesis: ( Z is open & f is_differentiable_on X & Z c= X implies f is_differentiable_on Z ) assume A1: Z is open ; ::_thesis: ( not f is_differentiable_on X or not Z c= X or f is_differentiable_on Z ) assume that A2: f is_differentiable_on X and A3: Z c= X ; ::_thesis: f is_differentiable_on Z X c= dom f by A2, Def8; hence A4: Z c= dom f by A3, XBOOLE_1:1; :: according to NDIFF_1:def_8 ::_thesis: for x being Point of S st x in Z holds f | Z is_differentiable_in x let x0 be Point of S; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 ) assume A5: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0 then consider N1 being Neighbourhood of x0 such that A6: N1 c= Z by A1, Th2; f | X is_differentiable_in x0 by A2, A3, A5, Def8; then consider N being Neighbourhood of x0 such that A7: N c= dom (f | X) and A8: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N holds ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6; consider N2 being Neighbourhood of x0 such that A9: N2 c= N and A10: N2 c= N1 by Th1; A11: N2 c= Z by A6, A10, XBOOLE_1:1; take N2 ; :: according to NDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) dom (f | X) = (dom f) /\ X by RELAT_1:61; then dom (f | X) c= dom f by XBOOLE_1:17; then N c= dom f by A7, XBOOLE_1:1; then N2 c= dom f by A9, XBOOLE_1:1; then N2 c= (dom f) /\ Z by A11, XBOOLE_1:19; hence A12: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that A13: for x being Point of S st x in N holds ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8; take L ; ::_thesis: ex R being RestFunc of S,T st for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) take R ; ::_thesis: for x being Point of S st x in N2 holds ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) let x be Point of S; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) assume A14: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) then ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A9, A13; then A15: ((f | X) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, A5, PARTFUN2:17; x in N by A9, A14; then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A7, A15, PARTFUN2:15; then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A4, A5, PARTFUN2:17; hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A12, A14, PARTFUN2:15; ::_thesis: verum end; theorem :: NDIFF_1:47 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 & 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)) ) ) ) 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 & 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)) ) ) ) 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 & 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)) ) ) ) let x0 be Point of S; ::_thesis: ( f is_differentiable_in x0 implies ex N being Neighbourhood of x0 st ( N c= dom f & 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)) ) ) ) ) assume f is_differentiable_in x0 ; ::_thesis: ex N being Neighbourhood of x0 st ( N c= dom f & 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)) ) ) ) then consider N being Neighbourhood of x0 such that A1: N c= dom f and A2: ex R being RestFunc of S,T st for x being Point of S st x in N holds (f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) by Def7; take N ; ::_thesis: ( N c= dom f & 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)) ) ) ) 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)) ) ) proof 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) ; consider R being RestFunc of S,T such that A3: 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; take R ; ::_thesis: ( 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)) ) ) (f /. x0) - (f /. x0) = (L . (x0 - x0)) + (R /. (x0 - x0)) by A3, NFCONT_1:4; then 0. T = (L . (x0 - x0)) + (R /. (x0 - x0)) by RLVECT_1:15; then 0. T = (L . (0. S)) + (R /. (x0 - x0)) by RLVECT_1:15; then A4: 0. T = (L . (0. S)) + (R /. (0. S)) by RLVECT_1:15; L . (0. S) = (modetrans (L,S,T)) . (0. S) by LOPBAN_1:def_11 .= (modetrans (L,S,T)) . (0 * (0. S)) by RLVECT_1:10 .= 0 * ((modetrans (L,S,T)) . (0. S)) by LOPBAN_1:def_5 .= 0. T by RLVECT_1:10 ; hence A5: R /. (0. S) = 0. T by A4, RLVECT_1:4; ::_thesis: ( 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)) ) ) A6: now__::_thesis:_for_s1_being_sequence_of_S_st_rng_s1_c=_dom_R_&_s1_is_convergent_&_lim_s1_=_0._S_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_0._S_)_holds_ (_R_/*_s1_is_convergent_&_lim_(R_/*_s1)_=_R_/._(0._S)_) let s1 be sequence of S; ::_thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0. S & ( for n being Element of NAT holds s1 . n <> 0. S ) implies ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) ) assume that rng s1 c= dom R and A7: ( s1 is convergent & lim s1 = 0. S ) and A8: for n being Element of NAT holds s1 . n <> 0. S ; ::_thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) s1 is non-zero by A8, Th7; then s1 is non-zero 0. S -convergent sequence of S by A7, Def4; hence ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) by A5, Th24; ::_thesis: verum end; R is total by Def5; then dom R = the carrier of S by PARTFUN1:def_2; hence ( 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 A3, A6, Th27; ::_thesis: verum end; hence ( N c= dom f & 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 A1; ::_thesis: verum end;