:: NDIFF_4 semantic presentation begin reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:45; set ZR = [#] REAL; Lm1: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; theorem Th1: :: NDIFF_4:1 for m being Element of NAT for f1, f2 being PartFunc of REAL,(REAL m) holds f1 - f2 = f1 + (- f2) proof let m be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL m) holds f1 - f2 = f1 + (- f2) let f1, f2 be PartFunc of REAL,(REAL m); ::_thesis: f1 - f2 = f1 + (- f2) A1: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def_46; A2: dom (f1 + (- f2)) = (dom f1) /\ (dom (- f2)) by VALUED_2:def_45; A3: dom (- f2) = dom f2 by NFCONT_4:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_._x_=_(f1_+_(-_f2))_._x let x be set ; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (f1 + (- f2)) . x ) assume A4: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (f1 + (- f2)) . x then A5: x in dom f2 by A1, XBOOLE_0:def_4; then A6: ( f2 . x = f2 /. x & (- f2) . x = (- f2) /. x ) by A3, PARTFUN1:def_6; thus (f1 - f2) . x = (f1 . x) - (f2 . x) by A4, VALUED_2:def_46 .= (f1 . x) + ((- f2) . x) by A3, A5, A6, NFCONT_4:def_3 .= (f1 + (- f2)) . x by A1, A2, A3, A4, VALUED_2:def_45 ; ::_thesis: verum end; hence f1 - f2 = f1 + (- f2) by A1, A2, A3, FUNCT_1:2; ::_thesis: verum end; definition let n be non empty Element of NAT ; let f be PartFunc of REAL,(REAL n); let x be real number ; predf is_differentiable_in x means :Def1: :: NDIFF_4:def 1 ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & g is_differentiable_in x ); end; :: deftheorem Def1 defines is_differentiable_in NDIFF_4:def_1_:_ for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for x being real number holds ( f is_differentiable_in x iff ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & g is_differentiable_in x ) ); theorem Th2: :: NDIFF_4:2 for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) for x being real number st h = f holds ( f is_differentiable_in x iff h is_differentiable_in x ) proof let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) for x being real number st h = f holds ( f is_differentiable_in x iff h is_differentiable_in x ) let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) for x being real number st h = f holds ( f is_differentiable_in x iff h is_differentiable_in x ) let h be PartFunc of REAL,(REAL-NS n); ::_thesis: for x being real number st h = f holds ( f is_differentiable_in x iff h is_differentiable_in x ) let x be real number ; ::_thesis: ( h = f implies ( f is_differentiable_in x iff h is_differentiable_in x ) ) assume A1: h = f ; ::_thesis: ( f is_differentiable_in x iff h is_differentiable_in x ) hereby ::_thesis: ( h is_differentiable_in x implies f is_differentiable_in x ) assume f is_differentiable_in x ; ::_thesis: h is_differentiable_in x then ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & g is_differentiable_in x ) by Def1; hence h is_differentiable_in x by A1; ::_thesis: verum end; thus ( h is_differentiable_in x implies f is_differentiable_in x ) by A1, Def1; ::_thesis: verum end; definition let n be non empty Element of NAT ; let f be PartFunc of REAL,(REAL n); let x be real number ; func diff (f,x) -> Element of REAL n means :Def2: :: NDIFF_4:def 2 ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & it = diff (g,x) ); existence ex b1 being Element of REAL n ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & b1 = diff (g,x) ) proof reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; diff (g,x) is Element of REAL n by REAL_NS1:def_4; hence ex b1 being Element of REAL n ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & b1 = diff (g,x) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL n st ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & b1 = diff (g,x) ) & ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & b2 = diff (g,x) ) holds b1 = b2 ; end; :: deftheorem Def2 defines diff NDIFF_4:def_2_:_ for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for x being real number for b4 being Element of REAL n holds ( b4 = diff (f,x) iff ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & b4 = diff (g,x) ) ); theorem Th3: :: NDIFF_4:3 for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) for x being real number st h = f holds diff (f,x) = diff (h,x) proof let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) for x being real number st h = f holds diff (f,x) = diff (h,x) let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) for x being real number st h = f holds diff (f,x) = diff (h,x) let h be PartFunc of REAL,(REAL-NS n); ::_thesis: for x being real number st h = f holds diff (f,x) = diff (h,x) let x be real number ; ::_thesis: ( h = f implies diff (f,x) = diff (h,x) ) ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & diff (f,x) = diff (g,x) ) by Def2; hence ( h = f implies diff (f,x) = diff (h,x) ) ; ::_thesis: verum end; definition let n be non empty Element of NAT ; let f be PartFunc of REAL,(REAL n); let X be set ; predf is_differentiable_on X means :Def3: :: NDIFF_4:def 3 ( X c= dom f & ( for x being Real st x in X holds f | X is_differentiable_in x ) ); end; :: deftheorem Def3 defines is_differentiable_on NDIFF_4:def_3_:_ for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for X being set holds ( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds f | X is_differentiable_in x ) ) ); theorem Th4: :: NDIFF_4:4 for X being set for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds X is Subset of REAL proof let X be set ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds X is Subset of REAL let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds X is Subset of REAL let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X implies X is Subset of REAL ) assume f is_differentiable_on X ; ::_thesis: X is Subset of REAL then X c= dom f by Def3; hence X is Subset of REAL by XBOOLE_1:1; ::_thesis: verum end; theorem Th5: :: NDIFF_4:5 for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) implies f is_differentiable_on Z ) proof assume A1: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) A2: Z c= dom g by A1, Def3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ g_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies g | Z is_differentiable_in x ) assume x in Z ; ::_thesis: g | Z is_differentiable_in x then f | Z is_differentiable_in x by A1, Def3; hence g | Z is_differentiable_in x by Th2; ::_thesis: verum end; then A3: g is_differentiable_on Z by A2, NDIFF_3:def_5; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies f is_differentiable_in x ) assume x in Z ; ::_thesis: f is_differentiable_in x then g is_differentiable_in x by A3, NDIFF_3:10; hence f is_differentiable_in x by Def1; ::_thesis: verum end; hence ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) by A1, Def3; ::_thesis: verum end; assume A4: ( Z c= dom f & ( for x being Real st x in Z holds f is_differentiable_in x ) ) ; ::_thesis: f is_differentiable_on Z now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ g_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies g is_differentiable_in x ) assume x in Z ; ::_thesis: g is_differentiable_in x then f is_differentiable_in x by A4; hence g is_differentiable_in x by Th2; ::_thesis: verum end; then A5: g is_differentiable_on Z by A4, NDIFF_3:10; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ f_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x ) assume x in Z ; ::_thesis: f | Z is_differentiable_in x then g | Z is_differentiable_in x by A5, NDIFF_3:def_5; hence f | Z is_differentiable_in x by Def1; ::_thesis: verum end; hence f is_differentiable_on Z by A4, Def3; ::_thesis: verum end; theorem Th6: :: NDIFF_4:6 for n being non empty Element of NAT for Y being Subset of REAL for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds Y is open proof let n be non empty Element of NAT ; ::_thesis: for Y being Subset of REAL for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds Y is open let Y be Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds Y is open let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on Y implies Y is open ) assume A1: f is_differentiable_on Y ; ::_thesis: Y is open reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: Y c= dom g by A1, Def3; now__::_thesis:_for_x_being_Real_st_x_in_Y_holds_ g_|_Y_is_differentiable_in_x let x be Real; ::_thesis: ( x in Y implies g | Y is_differentiable_in x ) assume x in Y ; ::_thesis: g | Y is_differentiable_in x then f | Y is_differentiable_in x by A1, Def3; hence g | Y is_differentiable_in x by Th2; ::_thesis: verum end; then g is_differentiable_on Y by A2, NDIFF_3:def_5; hence Y is open by NDIFF_3:11; ::_thesis: verum end; definition let n be non empty Element of NAT ; let f be PartFunc of REAL,(REAL n); let X be set ; assume A1: f is_differentiable_on X ; funcf `| X -> PartFunc of REAL,(REAL n) means :Def4: :: NDIFF_4:def 4 ( dom it = X & ( for x being Real st x in X holds it . x = diff (f,x) ) ); existence ex b1 being PartFunc of REAL,(REAL n) st ( dom b1 = X & ( for x being Real st x in X holds b1 . x = diff (f,x) ) ) proof deffunc H1( Real) -> Element of REAL n = diff (f,\$1); defpred S1[ set ] means \$1 in X; consider F0 being PartFunc of REAL,(REAL n) such that A2: ( ( for x being Real holds ( x in dom F0 iff S1[x] ) ) & ( for x being Real st x in dom F0 holds F0 . x = H1(x) ) ) from SEQ_1:sch_3(); take F0 ; ::_thesis: ( dom F0 = X & ( for x being Real st x in X holds F0 . x = diff (f,x) ) ) now__::_thesis:_for_y_being_set_st_y_in_X_holds_ y_in_dom_F0 A3: X is Subset of REAL by A1, Th4; let y be set ; ::_thesis: ( y in X implies y in dom F0 ) assume y in X ; ::_thesis: y in dom F0 hence y in dom F0 by A2, A3; ::_thesis: verum end; then A4: X c= dom F0 by TARSKI:def_3; for y being set st y in dom F0 holds y in X by A2; then dom F0 c= X by TARSKI:def_3; hence dom F0 = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Real st x in X holds F0 . x = diff (f,x) now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ F0_._x_=_diff_(f,x) let x be Real; ::_thesis: ( x in X implies F0 . x = diff (f,x) ) assume x in X ; ::_thesis: F0 . x = diff (f,x) then x in dom F0 by A2; hence F0 . x = diff (f,x) by A2; ::_thesis: verum end; hence for x being Real st x in X holds F0 . x = diff (f,x) ; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of REAL,(REAL n) st dom b1 = X & ( for x being Real st x in X holds b1 . x = diff (f,x) ) & dom b2 = X & ( for x being Real st x in X holds b2 . x = diff (f,x) ) holds b1 = b2 proof let F0, G0 be PartFunc of REAL,(REAL n); ::_thesis: ( dom F0 = X & ( for x being Real st x in X holds F0 . x = diff (f,x) ) & dom G0 = X & ( for x being Real st x in X holds G0 . x = diff (f,x) ) implies F0 = G0 ) assume that A5: dom F0 = X and A6: for x being Real st x in X holds F0 . x = diff (f,x) and A7: dom G0 = X and A8: for x being Real st x in X holds G0 . x = diff (f,x) ; ::_thesis: F0 = G0 now__::_thesis:_for_x_being_Real_st_x_in_dom_F0_holds_ F0_._x_=_G0_._x let x be Real; ::_thesis: ( x in dom F0 implies F0 . x = G0 . x ) assume A9: x in dom F0 ; ::_thesis: F0 . x = G0 . x then F0 . x = diff (f,x) by A5, A6; hence F0 . x = G0 . x by A5, A8, A9; ::_thesis: verum end; hence F0 = G0 by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def4 defines `| NDIFF_4:def_4_:_ for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for X being set st f is_differentiable_on X holds for b4 being PartFunc of REAL,(REAL n) holds ( b4 = f `| X iff ( dom b4 = X & ( for x being Real st x in X holds b4 . x = diff (f,x) ) ) ); theorem :: NDIFF_4:7 for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n ) ) proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & ex r being Element of REAL n st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n ) ) ) assume A1: Z c= dom f ; ::_thesis: ( for r being Element of REAL n holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n ) ) ) given r being Element of REAL n such that A2: rng f = {r} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n ) ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A3: r is Point of (REAL-NS n) by REAL_NS1:def_4; then A4: ( g is_differentiable_on Z & ( for x being Real st x in Z holds (g `| Z) /. x = 0. (REAL-NS n) ) ) by A1, A2, NDIFF_3:12; A5: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ f_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x ) assume x in Z ; ::_thesis: f | Z is_differentiable_in x then g | Z is_differentiable_in x by A4, NDIFF_3:def_5; hence f | Z is_differentiable_in x by Def1; ::_thesis: verum end; then A6: f is_differentiable_on Z by A1, Def3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (f_`|_Z)_/._x_=_0*_n let x be Real; ::_thesis: ( x in Z implies (f `| Z) /. x = 0* n ) assume A7: x in Z ; ::_thesis: (f `| Z) /. x = 0* n then A8: (g `| Z) /. x = 0. (REAL-NS n) by A3, A1, A2, NDIFF_3:12; x in dom (g `| Z) by A4, A7, NDIFF_3:def_6; then A9: (g `| Z) . x = 0. (REAL-NS n) by A8, PARTFUN1:def_6; A10: (g `| Z) . x = diff (g,x) by A7, A4, NDIFF_3:def_6; A11: (f `| Z) . x = diff (f,x) by A7, A6, Def4; diff (f,x) = diff (g,x) by Th3; then A12: (f `| Z) . x = 0* n by A9, A10, A11, REAL_NS1:def_4; x in dom (f `| Z) by A6, Def4, A7; hence (f `| Z) /. x = 0* n by A12, PARTFUN1:def_6; ::_thesis: verum end; hence ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n ) ) by A5, A1, Def3; ::_thesis: verum end; theorem :: NDIFF_4:8 for n being non empty Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) proof let n be non empty Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for N being Neighbourhood of x0 st f = g & f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) let N be Neighbourhood of x0; ::_thesis: ( f = g & f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) ) assume that A1: f = g and A2: f is_differentiable_in x0 and A3: N c= dom f ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) A4: g is_differentiable_in x0 by A1, A2, Th2; let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) let c be constant Real_Sequence; ::_thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) ) assume ( rng c = {x0} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) then ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (g,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) by A4, A1, A3, NDIFF_3:13; hence ( (h ") (#) ((g /* (h + c)) - (g /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((g /* (h + c)) - (g /* c))) ) by A1, Th3; ::_thesis: verum end; theorem Th9: :: NDIFF_4:9 for x0, r being Real for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) proof let x0, r be Real; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) 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 REAL,(REAL n); ::_thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) ) assume f is_differentiable_in x0 ; ::_thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) then consider g being PartFunc of REAL,(REAL-NS n) such that A1: ( f = g & g is_differentiable_in x0 ) by Def1; A2: ( r (#) g is_differentiable_in x0 & diff ((r (#) g),x0) = r * (diff (g,x0)) ) by A1, NDIFF_3:16; A3: r (#) f = r (#) g by A1, NFCONT_4:6; A4: diff (f,x0) = diff (g,x0) by A1, Th3; diff ((r (#) f),x0) = diff ((r (#) g),x0) by A1, Th3, NFCONT_4:6; hence ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by A3, A2, Def1, A4, REAL_NS1:3; ::_thesis: verum end; theorem Th10: :: NDIFF_4:10 for x0 being Real for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) proof let x0 be Real; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_in x0 implies ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) ) (- 1) (#) f = - f by NFCONT_4:7; hence ( f is_differentiable_in x0 implies ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) ) by Th9; ::_thesis: verum end; theorem Th11: :: NDIFF_4:11 for x0 being Real for n being non empty Element of NAT for f1, f2 being PartFunc of REAL,(REAL n) 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 x0 be Real; ::_thesis: for n being non empty Element of NAT for f1, f2 being PartFunc of REAL,(REAL n) 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 n be non empty Element of NAT ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) 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 REAL,(REAL n); ::_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 A1: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) ; ::_thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) consider g1 being PartFunc of REAL,(REAL-NS n) such that A2: ( f1 = g1 & g1 is_differentiable_in x0 ) by A1, Def1; consider g2 being PartFunc of REAL,(REAL-NS n) such that A3: ( f2 = g2 & g2 is_differentiable_in x0 ) by A1, Def1; A4: ( g1 + g2 is_differentiable_in x0 & diff ((g1 + g2),x0) = (diff (g1,x0)) + (diff (g2,x0)) ) by A2, A3, NDIFF_3:14; A5: f1 + f2 = g1 + g2 by A2, A3, NFCONT_4:5; A6: ( diff (f1,x0) = diff (g1,x0) & diff (f2,x0) = diff (g2,x0) ) by A2, A3, Th3; diff ((f1 + f2),x0) = diff ((g1 + g2),x0) by A2, A3, Th3, NFCONT_4:5; hence ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) by A5, A4, Def1, A6, REAL_NS1:2; ::_thesis: verum end; theorem :: NDIFF_4:12 for x0 being Real for n being non empty Element of NAT for f1, f2 being PartFunc of REAL,(REAL n) 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 x0 be Real; ::_thesis: for n being non empty Element of NAT for f1, f2 being PartFunc of REAL,(REAL n) 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 n be non empty Element of NAT ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) 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 REAL,(REAL n); ::_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)) ) ) A1: f1 - f2 = f1 + (- f2) by Th1; assume A2: f1 is_differentiable_in x0 ; ::_thesis: ( not f2 is_differentiable_in x0 or ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) ) assume f2 is_differentiable_in x0 ; ::_thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) then ( - f2 is_differentiable_in x0 & diff ((- f2),x0) = - (diff (f2,x0)) ) by Th10; hence ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) by A1, A2, Th11; ::_thesis: verum end; theorem Th13: :: NDIFF_4:13 for r being Real for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) proof let r be Real; ::_thesis: for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) ) assume that A1: Z c= dom f and A2: f is_differentiable_on Z ; ::_thesis: ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A3: dom f = dom (r (#) f) by VALUED_2:def_39; A4: r (#) f = r (#) g by NFCONT_4:6; A5: Z c= dom (r (#) g) by A3, A1, NFCONT_4:6; A6: Z c= dom g by A2, Def3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ g_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies g | Z is_differentiable_in x ) assume x in Z ; ::_thesis: g | Z is_differentiable_in x then f | Z is_differentiable_in x by A2, Def3; hence g | Z is_differentiable_in x by Th2; ::_thesis: verum end; then g is_differentiable_on Z by A6, NDIFF_3:def_5; then A7: ( r (#) g is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) g) `| Z) . x = r * (diff (g,x)) ) ) by A5, NDIFF_3:19; A8: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (r_(#)_f)_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (r (#) f) | Z is_differentiable_in x ) assume x in Z ; ::_thesis: (r (#) f) | Z is_differentiable_in x then (r (#) g) | Z is_differentiable_in x by A7, NDIFF_3:def_5; hence (r (#) f) | Z is_differentiable_in x by A4, Def1; ::_thesis: verum end; then A9: r (#) f is_differentiable_on Z by A3, A1, Def3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((r_(#)_f)_`|_Z)_._x_=_r_*_(diff_(f,x)) let x be Real; ::_thesis: ( x in Z implies ((r (#) f) `| Z) . x = r * (diff (f,x)) ) assume A10: x in Z ; ::_thesis: ((r (#) f) `| Z) . x = r * (diff (f,x)) then f is_differentiable_in x by A2, Th5; then ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r * (diff (f,x)) ) by Th9; hence ((r (#) f) `| Z) . x = r * (diff (f,x)) by A10, A9, Def4; ::_thesis: verum end; hence ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) by A3, A8, A1, Def3; ::_thesis: verum end; theorem Th14: :: NDIFF_4:14 for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds ( - f is_differentiable_on Z & ( for x being Real st x in Z holds ((- f) `| Z) . x = - (diff (f,x)) ) ) proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds ( - f is_differentiable_on Z & ( for x being Real st x in Z holds ((- f) `| Z) . x = - (diff (f,x)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds ( - f is_differentiable_on Z & ( for x being Real st x in Z holds ((- f) `| Z) . x = - (diff (f,x)) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & f is_differentiable_on Z implies ( - f is_differentiable_on Z & ( for x being Real st x in Z holds ((- f) `| Z) . x = - (diff (f,x)) ) ) ) (- 1) (#) f = - f by NFCONT_4:7; hence ( Z c= dom f & f is_differentiable_on Z implies ( - f is_differentiable_on Z & ( for x being Real st x in Z holds ((- f) `| Z) . x = - (diff (f,x)) ) ) ) by Th13; ::_thesis: verum end; theorem Th15: :: NDIFF_4:15 for n being non empty Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) let f1, f2 be PartFunc of REAL,(REAL n); ::_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 Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) ) assume that A1: Z c= dom (f1 + f2) and A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) ) reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A3: f1 + f2 = g1 + g2 by NFCONT_4:5; A4: Z c= dom (g1 + g2) by A1, NFCONT_4:5; A5: ( Z c= dom g1 & Z c= dom g2 ) by A2, Def3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ g1_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies g1 | Z is_differentiable_in x ) assume x in Z ; ::_thesis: g1 | Z is_differentiable_in x then f1 | Z is_differentiable_in x by A2, Def3; hence g1 | Z is_differentiable_in x by Th2; ::_thesis: verum end; then A6: g1 is_differentiable_on Z by A5, NDIFF_3:def_5; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ g2_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies g2 | Z is_differentiable_in x ) assume x in Z ; ::_thesis: g2 | Z is_differentiable_in x then f2 | Z is_differentiable_in x by A2, Def3; hence g2 | Z is_differentiable_in x by Th2; ::_thesis: verum end; then g2 is_differentiable_on Z by A5, NDIFF_3:def_5; then A7: ( g1 + g2 is_differentiable_on Z & ( for x being Real st x in Z holds ((g1 + g2) `| Z) . x = (diff (g1,x)) + (diff (g2,x)) ) ) by A4, A6, NDIFF_3:17; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (f1_+_f2)_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (f1 + f2) | Z is_differentiable_in x ) assume x in Z ; ::_thesis: (f1 + f2) | Z is_differentiable_in x then (g1 + g2) | Z is_differentiable_in x by A7, NDIFF_3:def_5; hence (f1 + f2) | Z is_differentiable_in x by A3, Def1; ::_thesis: verum end; hence A8: f1 + f2 is_differentiable_on Z by A1, Def3; ::_thesis: for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) assume A9: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) then ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th5; then ( f1 + f2 is_differentiable_in x & diff ((f1 + f2),x) = (diff (f1,x)) + (diff (f2,x)) ) by Th11; hence ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A9, A8, Def4; ::_thesis: verum end; theorem :: NDIFF_4:16 for n being non empty Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) let f1, f2 be PartFunc of REAL,(REAL n); ::_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 Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) ) A1: f1 - f2 = f1 + (- f2) by Th1; A2: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def_46; assume that A3: Z c= dom (f1 - f2) and A4: f1 is_differentiable_on Z and A5: f2 is_differentiable_on Z ; ::_thesis: ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) Z c= dom f2 by A3, A2, XBOOLE_1:18; then A6: - f2 is_differentiable_on Z by A5, Th14; hence f1 - f2 is_differentiable_on Z by A1, A3, A4, Th15; ::_thesis: for x being Real st x in Z holds ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) let x be Real; ::_thesis: ( x in Z implies ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) assume A7: x in Z ; ::_thesis: ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) then A8: f2 is_differentiable_in x by A5, Th5; thus ((f1 - f2) `| Z) . x = (diff (f1,x)) + (diff ((- f2),x)) by A1, A3, A4, A6, A7, Th15 .= (diff (f1,x)) - (diff (f2,x)) by A8, Th10 ; ::_thesis: verum end; theorem :: NDIFF_4:17 for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0* n ) ) proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0* n ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0* n ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0* n ) ) ) assume that A1: Z c= dom f and A2: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = 0* n ) ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A3: g | Z is constant by A2; then A4: ( g is_differentiable_on Z & ( for x being Real st x in Z holds (g `| Z) . x = 0. (REAL-NS n) ) ) by A1, NDIFF_3:20; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ f_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x ) assume x in Z ; ::_thesis: f | Z is_differentiable_in x then g | Z is_differentiable_in x by A4, NDIFF_3:def_5; hence f | Z is_differentiable_in x by Def1; ::_thesis: verum end; hence A5: f is_differentiable_on Z by A1, Def3; ::_thesis: for x being Real st x in Z holds (f `| Z) . x = 0* n let x be Real; ::_thesis: ( x in Z implies (f `| Z) . x = 0* n ) assume A6: x in Z ; ::_thesis: (f `| Z) . x = 0* n then A7: (g `| Z) . x = 0. (REAL-NS n) by A3, A1, NDIFF_3:20; A8: (g `| Z) . x = diff (g,x) by A6, A4, NDIFF_3:def_6; A9: (f `| Z) . x = diff (f,x) by A6, A5, Def4; diff (f,x) = diff (g,x) by Th3; hence (f `| Z) . x = 0* n by A7, A8, A9, REAL_NS1:def_4; ::_thesis: verum end; theorem Th18: :: NDIFF_4:18 for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) let r, p be Element of REAL n; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds f /. x = (x * r) + p ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) ) assume that A1: Z c= dom f and A2: for x being Real st x in Z holds f /. x = (x * r) + p ; ::_thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = r ) ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; reconsider r1 = r, p1 = p as Point of (REAL-NS n) by REAL_NS1:def_4; A3: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ g_/._x_=_(x_*_r1)_+_p1 let x be Real; ::_thesis: ( x in Z implies g /. x = (x * r1) + p1 ) assume x in Z ; ::_thesis: g /. x = (x * r1) + p1 then A4: f /. x = (x * r) + p by A2; A5: f /. x = g /. x by REAL_NS1:def_4; x * r = x * r1 by REAL_NS1:3; hence g /. x = (x * r1) + p1 by A4, A5, REAL_NS1:2; ::_thesis: verum end; then A6: ( g is_differentiable_on Z & ( for x being Real st x in Z holds (g `| Z) . x = r1 ) ) by A1, NDIFF_3:21; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ f_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x ) assume x in Z ; ::_thesis: f | Z is_differentiable_in x then g | Z is_differentiable_in x by A6, NDIFF_3:def_5; hence f | Z is_differentiable_in x by Def1; ::_thesis: verum end; hence A7: f is_differentiable_on Z by A1, Def3; ::_thesis: for x being Real st x in Z holds (f `| Z) . x = r let x be Real; ::_thesis: ( x in Z implies (f `| Z) . x = r ) assume A8: x in Z ; ::_thesis: (f `| Z) . x = r then A9: (g `| Z) . x = diff (g,x) by A6, NDIFF_3:def_6; A10: (f `| Z) . x = diff (f,x) by A8, A7, Def4; diff (f,x) = diff (g,x) by Th3; hence (f `| Z) . x = r by A8, A3, A1, A9, A10, NDIFF_3:21; ::_thesis: verum end; theorem :: NDIFF_4:19 for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for x0 being Real st f is_differentiable_in x0 holds f is_continuous_in x0 proof let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for x0 being Real st f is_differentiable_in x0 holds f is_continuous_in x0 let f be PartFunc of REAL,(REAL n); ::_thesis: for x0 being Real st f is_differentiable_in x0 holds f is_continuous_in x0 let x0 be Real; ::_thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 ) assume f is_differentiable_in x0 ; ::_thesis: f is_continuous_in x0 then consider g being PartFunc of REAL,(REAL-NS n) such that A1: ( f = g & g is_differentiable_in x0 ) by Def1; g is_continuous_in x0 by A1, NDIFF_3:22; hence f is_continuous_in x0 by A1, NFCONT_4:def_1; ::_thesis: verum end; theorem :: NDIFF_4:20 for X being set for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds f | X is continuous proof let X be set ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds f | X is continuous let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X holds f | X is continuous let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X implies f | X is continuous ) assume A1: f is_differentiable_on X ; ::_thesis: f | X is continuous reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: X c= dom g by A1, Def3; now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ g_|_X_is_differentiable_in_x let x be Real; ::_thesis: ( x in X implies g | X is_differentiable_in x ) assume x in X ; ::_thesis: g | X is_differentiable_in x then f | X is_differentiable_in x by A1, Def3; hence g | X is_differentiable_in x by Th2; ::_thesis: verum end; then g is_differentiable_on X by A2, NDIFF_3:def_5; then g | X is continuous by NDIFF_3:23; hence f | X is continuous by NFCONT_4:23; ::_thesis: verum end; theorem Th21: :: NDIFF_4:21 for X being set for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z proof let X be set ; ::_thesis: for n being non empty Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z ) assume A1: ( f is_differentiable_on X & Z c= X ) ; ::_thesis: f is_differentiable_on Z then A2: ( X c= dom f & ( for x being Real st x in X holds f | X is_differentiable_in x ) ) by Def3; A3: Z c= dom f by A1, A2, XBOOLE_1:1; reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ g_|_X_is_differentiable_in_x let x be Real; ::_thesis: ( x in X implies g | X is_differentiable_in x ) assume x in X ; ::_thesis: g | X is_differentiable_in x then f | X is_differentiable_in x by A1, Def3; hence g | X is_differentiable_in x by Th2; ::_thesis: verum end; then g is_differentiable_on X by A2, NDIFF_3:def_5; then A4: g is_differentiable_on Z by A1, NDIFF_3:24; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ f_|_Z_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies f | Z is_differentiable_in x ) assume x in Z ; ::_thesis: f | Z is_differentiable_in x then g | Z is_differentiable_in x by A4, NDIFF_3:def_5; hence f | Z is_differentiable_in x by Def1; ::_thesis: verum end; hence f is_differentiable_on Z by A3, Def3; ::_thesis: verum end; definition let n be non empty Element of NAT ; let f be PartFunc of REAL,(REAL n); attrf is differentiable means :Def5: :: NDIFF_4:def 5 f is_differentiable_on dom f; end; :: deftheorem Def5 defines differentiable NDIFF_4:def_5_:_ for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) holds ( f is differentiable iff f is_differentiable_on dom f ); registration let n be non empty Element of NAT ; clusterREAL --> (0* n) -> differentiable for Function of REAL,(REAL n); coherence for b1 being Function of REAL,(REAL n) st b1 = REAL --> (0* n) holds b1 is differentiable proof set f = REAL --> (0* n); A1: [#] REAL = dom (REAL --> (0* n)) by FUNCT_2:def_1; now__::_thesis:_for_x_being_Real_st_x_in_[#]_REAL_holds_ (REAL_-->_(0*_n))_/._x_=_(x_*_(0*_n))_+_(0*_n) let x be Real; ::_thesis: ( x in [#] REAL implies (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n) ) assume x in [#] REAL ; ::_thesis: (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n) A2: (REAL --> (0* n)) /. x = 0* n by FUNCOP_1:7 .= 0. (TOP-REAL n) by EUCLID:70 .= x * (0. (TOP-REAL n)) by EUCLID:28 .= (x * (0. (TOP-REAL n))) + (0. (TOP-REAL n)) by EUCLID:27 ; A3: x * (0. (TOP-REAL n)) = x (#) (0* n) by EUCLID:65, EUCLID:70; 0. (TOP-REAL n) = 0* n by EUCLID:70; hence (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n) by A2, A3, EUCLID:64; ::_thesis: verum end; then REAL --> (0* n) is_differentiable_on [#] REAL by A1, Th18; hence for b1 being Function of REAL,(REAL n) st b1 = REAL --> (0* n) holds b1 is differentiable by A1, Def5; ::_thesis: verum end; end; registration let n be non empty Element of NAT ; cluster non empty Relation-like REAL -defined REAL n -valued Function-like total quasi_total V239() V240() V241() differentiable for Element of K6(K7(REAL,(REAL n))); existence ex b1 being Function of REAL,(REAL n) st b1 is differentiable proof take REAL --> (0* n) ; ::_thesis: REAL --> (0* n) is differentiable thus REAL --> (0* n) is differentiable ; ::_thesis: verum end; end; theorem :: NDIFF_4:22 for n being non empty Element of NAT for Z being open Subset of REAL for f being differentiable PartFunc of REAL,(REAL n) st Z c= dom f holds f is_differentiable_on Z proof let n be non empty Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being differentiable PartFunc of REAL,(REAL n) st Z c= dom f holds f is_differentiable_on Z let Z be open Subset of REAL; ::_thesis: for f being differentiable PartFunc of REAL,(REAL n) st Z c= dom f holds f is_differentiable_on Z let f be differentiable PartFunc of REAL,(REAL n); ::_thesis: ( Z c= dom f implies f is_differentiable_on Z ) f is_differentiable_on dom f by Def5; hence ( Z c= dom f implies f is_differentiable_on Z ) by Th21; ::_thesis: verum end; theorem Th23: :: NDIFF_4:23 for n being non empty Element of NAT for R being PartFunc of REAL,(REAL-NS n) 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 Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) ) proof let n be non empty Element of NAT ; ::_thesis: for R being PartFunc of REAL,(REAL-NS n) 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 Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) ) let R be PartFunc of REAL,(REAL-NS n); ::_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 Real st z <> 0 & |.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 Real st z <> 0 & |.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_Real_st_ (_z_<>_0_&_|.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_Real_st_z_<>_0_&_|.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 Real st ( z <> 0 & |.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 Real st z <> 0 & |.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 Real st ( z <> 0 & |.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 Real st z <> 0 & |.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 Real st ( z <> 0 & |.z.| < d & not (|.z.| ") * ||.(R /. z).|| < r ) ; defpred S1[ Element of NAT , Real] means ( \$2 <> 0 & |.\$2.| < 1 / (\$1 + 1) & not (|.\$2.| ") * ||.(R /. \$2).|| < r ); A6: for n being Element of NAT ex z being Real st S1[n,z] proof let n be Element of NAT ; ::_thesis: ex z being Real st S1[n,z] 1 / (n + 1) is Real by XREAL_0:def_1; hence ex z being Real st S1[n,z] by A5; ::_thesis: verum end; consider s being Real_Sequence 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_number_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((s_._m)_-_0).|_<_p let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - 0).| < 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).| < p consider n being Element of NAT such that A10: p " < n by SEQ_4:3; reconsider q0 = 0 , q1 = 1 as real number ; (p ") + q0 < n + q1 by A10, XREAL_1:8; then A11: 1 / (n + 1) < 1 / (p ") by A9, XREAL_1:76; take n = n; ::_thesis: for m being Element of NAT st n <= m holds |.((s . m) - 0).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s . m) - 0).| < p ) assume n <= m ; ::_thesis: |.((s . m) - 0).| < p then A12: n + 1 <= m + 1 by XREAL_1:6; 1 / (m + 1) <= 1 / (n + 1) by A12, XREAL_1:118; then |.((s . m) - 0).| < 1 / (n + 1) by A7, XXREAL_0:2; hence |.((s . m) - 0).| < p by A11, XXREAL_0:2; ::_thesis: verum end; A13: s is convergent by A8, SEQ_2:def_6; then A14: lim s = 0 by A8, SEQ_2:def_7; s is non-zero by A7, SEQ_1:5; then reconsider s = s as non-zero 0 -convergent Real_Sequence by A13, A14, FDIFF_1:def_1; ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) ) by A3, NDIFF_3:def_1; then consider n0 being Element of NAT such that A15: for m being Element of NAT st n0 <= m holds ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A4, NORMSP_1:def_7; A16: ||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| < r by A15; A17: ||.(((s . n0) ") * (R /. (s . n0))).|| = (abs ((s . n0) ")) * ||.(R /. (s . n0)).|| by NORMSP_1:def_1 .= (|.(s . n0).| ") * ||.(R /. (s . n0)).|| by COMPLEX1:66 ; dom R = REAL by A1, PARTFUN1:def_2; then A18: rng s c= dom R ; ||.((((s ") (#) (R /* s)) . n0) - (0. (REAL-NS n))).|| = ||.(((s ") (#) (R /* s)) . n0).|| by RLVECT_1:13 .= ||.(((s ") . n0) * ((R /* s) . n0)).|| by NDIFF_1:def_2 .= ||.(((s . n0) ") * ((R /* s) . n0)).|| by VALUED_1:10 .= ||.(((s . n0) ") * (R /. (s . n0))).|| by A18, FUNCT_2:109 ; hence for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) by A7, A16, A17; ::_thesis: verum end; now__::_thesis:_(_(_for_r_being_Real_st_r_>_0_holds_ ex_d_being_Real_st_ (_d_>_0_&_(_for_z_being_Real_st_z_<>_0_&_|.z.|_<_d_holds_ (|.z.|_")_*_||.(R_/._z).||_<_r_)_)_)_implies_R_is_RestFunc-like_) assume A19: for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) ; ::_thesis: R is RestFunc-like now__::_thesis:_for_s_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(s_")_(#)_(R_/*_s)_is_convergent_&_lim_((s_")_(#)_(R_/*_s))_=_0._(REAL-NS_n)_) let s be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (s ") (#) (R /* s) is convergent & lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) ) A20: ( s is convergent & lim s = 0 ) ; A21: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_n0_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n0_<=_m_holds_ ||.((((s_")_(#)_(R_/*_s))_._m)_-_(0._(REAL-NS_n))).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r ) assume r > 0 ; ::_thesis: ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r then consider d being Real such that A22: d > 0 and A23: for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r by A19; consider n0 being Element of NAT such that A24: for m being Element of NAT st n0 <= m holds |.((s . m) - 0).| < d by A20, A22, SEQ_2:def_7; take n0 = n0; ::_thesis: for m being Element of NAT st n0 <= m holds ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r thus for m being Element of NAT st n0 <= m holds ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r ::_thesis: verum proof dom R = REAL by A1, PARTFUN1:def_2; then A25: rng s c= dom R ; let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r ) assume n0 <= m ; ::_thesis: ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r then A26: |.((s . m) - 0).| < d by A24; A27: s . m <> 0 by SEQ_1:5; (|.(s . m).| ") * ||.(R /. (s . m)).|| = (abs ((s . m) ")) * ||.(R /. (s . m)).|| by COMPLEX1:66 .= ||.(((s . m) ") * (R /. (s . m))).|| by NORMSP_1:def_1 .= ||.(((s . m) ") * ((R /* s) . m)).|| by A25, FUNCT_2:109 .= ||.(((s ") . m) * ((R /* s) . m)).|| by VALUED_1:10 .= ||.(((s ") (#) (R /* s)) . m).|| by NDIFF_1:def_2 .= ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| by RLVECT_1:13 ; hence ||.((((s ") (#) (R /* s)) . m) - (0. (REAL-NS n))).|| < r by A23, A26, A27; ::_thesis: verum end; end; hence (s ") (#) (R /* s) is convergent by NORMSP_1:def_6; ::_thesis: lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) hence lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) by A21, NORMSP_1:def_7; ::_thesis: verum end; hence R is RestFunc-like by A1, NDIFF_3:def_1; ::_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 Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) ) by A2; ::_thesis: verum end; theorem Th24: :: NDIFF_4:24 for i being Element of NAT for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) for x0 being real number st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) proof let i be Element of NAT ; ::_thesis: for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) for x0 being real number st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) let n be non empty Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for x0 being real number st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for x0 being real number st 1 <= i & i <= n & g is_differentiable_in x0 holds ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) let x0 be real number ; ::_thesis: ( 1 <= i & i <= n & g is_differentiable_in x0 implies ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) ) assume A1: ( 1 <= i & i <= n & g is_differentiable_in x0 ) ; ::_thesis: ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) then consider N being Neighbourhood of x0 such that A2: ( N c= dom g & ex DFG being LinearFunc of (REAL-NS n) ex GR being RestFunc of (REAL-NS n) st ( diff (g,x0) = DFG . 1 & ( for x being Real st x in N holds (g /. x) - (g /. x0) = (DFG . (x - x0)) + (GR /. (x - x0)) ) ) ) by NDIFF_3:def_4; consider GR being RestFunc of (REAL-NS n), DFG being LinearFunc of (REAL-NS n) such that A3: ( diff (g,x0) = DFG . 1 & ( for x being Element of REAL st x in N holds (g /. x) - (g /. x0) = (DFG . (x - x0)) + (GR /. (x - x0)) ) ) by A2; consider LP being Point of (REAL-NS n) such that A4: for p being Real holds DFG . p = p * LP by NDIFF_3:def_2; reconsider PG = Proj (i,n) as Function of (REAL-NS n),(REAL-NS 1) ; reconsider L = (Proj (i,n)) * DFG as Function of REAL,(REAL-NS 1) ; A5: for r being Real holds L . r = r * ((Proj (i,n)) . LP) proof let r be Real; ::_thesis: L . r = r * ((Proj (i,n)) . LP) A6: dom L = REAL by FUNCT_2:def_1; DFG . r = r * LP by A4; then (Proj (i,n)) . (DFG . r) = r * ((Proj (i,n)) . LP) by PDIFF_6:27; hence L . r = r * ((Proj (i,n)) . LP) by A6, FUNCT_1:12; ::_thesis: verum end; then reconsider L = L as LinearFunc of (REAL-NS 1) by NDIFF_3:def_2; A7: GR is total by NDIFF_3:def_1; then reconsider FGR = GR as Function of REAL,(REAL-NS n) ; A8: (Proj (i,n)) * FGR is Function of REAL,(REAL-NS 1) ; (Proj (i,n)) * GR is RestFunc of (REAL-NS 1) proof A9: dom GR = REAL by A7, PARTFUN1:def_2; reconsider R = (Proj (i,n)) * GR as PartFunc of REAL,(REAL-NS 1) ; for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) proof let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) ) assume r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) then consider d being Real such that A10: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(GR /. z).|| < r ) ) by A7, Th23; take d ; ::_thesis: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) thus d > 0 by A10; ::_thesis: for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r let z be Element of REAL ; ::_thesis: ( z <> 0 & |.z.| < d implies (|.z.| ") * ||.(R /. z).|| < r ) assume A11: ( z <> 0 & |.z.| < d ) ; ::_thesis: (|.z.| ") * ||.(R /. z).|| < r A12: GR /. z = GR . z by A9, PARTFUN1:def_6; A13: i in Seg n by A1; reconsider GRz = GR /. z as Point of (REAL-NS n) ; reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def_4; reconsider GRzi = GRz1 . i as Element of REAL ; dom (Proj (i,n)) = the carrier of (REAL-NS n) by PARTFUN1:def_2; then A14: z in dom ((Proj (i,n)) * GR) by A9, A12, FUNCT_1:11; then ((Proj (i,n)) * GR) . z = (Proj (i,n)) . (GR . z) by FUNCT_1:12 .= <*((proj (i,n)) . GRz1)*> by A12, PDIFF_1:def_4 ; then A15: ((Proj (i,n)) * GR) . z = <*GRzi*> by PDIFF_1:def_1; A16: abs GRzi <= ||.(GR /. z).|| by A13, REAL_NS1:9; A17: 0 <= |.z.| by COMPLEX1:46; 0 <= abs GRzi by COMPLEX1:46; then A18: (|.z.| ") * (abs GRzi) <= (|.z.| ") * ||.(GR /. z).|| by A16, A17, XREAL_1:66; (|.z.| ") * ||.(GR /. z).|| < r by A10, A11; then A19: (|.z.| ") * (abs GRzi) < r by A18, XXREAL_0:2; ((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR) by A14, FUNCT_1:3; then reconsider Rz = ((Proj (i,n)) * GR) . z as VECTOR of (REAL-NS 1) ; set VGRzi = <*GRzi*>; <*GRzi*> is Element of REAL 1 by FINSEQ_2:98; then ||.Rz.|| = |.<*GRzi*>.| by A15, REAL_NS1:1; then (|.z.| ") * ||.Rz.|| < r by A19, JORDAN2C:10; hence (|.z.| ") * ||.(R /. z).|| < r by A14, PARTFUN1:def_6; ::_thesis: verum end; hence (Proj (i,n)) * GR is RestFunc of (REAL-NS 1) by A8, Th23; ::_thesis: verum end; then reconsider R = (Proj (i,n)) * GR as RestFunc of (REAL-NS 1) ; set pg = (Proj (i,n)) * g; A20: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; then rng g c= dom (Proj (i,n)) ; then A21: dom g = dom ((Proj (i,n)) * g) by RELAT_1:27; A22: dom (Proj (i,n)) = REAL n by A20, REAL_NS1:def_4; A23: for x being Real st x in N holds (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) now__::_thesis:_(_x_in_N_&_x_in_N_implies_(((Proj_(i,n))_*_g)_/._x)_-_(((Proj_(i,n))_*_g)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))_) assume A24: x in N ; ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) then A25: (g /. x) - (g /. x0) = (DFG . (x - x0)) + (GR /. (x - x0)) by A3; A26: x0 in N by RCOMP_1:16; then A27: ( ((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x & ((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 ) by A2, A21, A24, PARTFUN1:def_6; A28: ( g /. x = g . x & g /. x0 = g . x0 ) by A2, A24, A26, PARTFUN1:def_6; reconsider PGSx = (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) as Element of REAL 1 by REAL_NS1:def_4; ((Proj (i,n)) * g) . x in rng ((Proj (i,n)) * g) by A2, A21, A24, FUNCT_1:3; then reconsider PGdx = ((Proj (i,n)) * g) . x as Element of REAL 1 by REAL_NS1:def_4; ((Proj (i,n)) * g) . x0 in rng ((Proj (i,n)) * g) by A2, A21, A26, FUNCT_1:3; then reconsider PGdx0 = ((Proj (i,n)) * g) . x0 as Element of REAL 1 by REAL_NS1:def_4; g . x in rng g by A2, A24, FUNCT_1:3; then reconsider Gx = g . x as Element of REAL n by REAL_NS1:def_4; g . x0 in rng g by A2, A26, FUNCT_1:3; then reconsider Gx0 = g . x0 as Element of REAL n by REAL_NS1:def_4; set ProjGx = (Proj (i,n)) . (g . x); Gx in dom (Proj (i,n)) by A22; then (Proj (i,n)) . (g . x) in rng (Proj (i,n)) by FUNCT_1:3; then reconsider ProjGx = (Proj (i,n)) . (g . x) as Element of REAL 1 by REAL_NS1:def_4; set ProjGx0 = (Proj (i,n)) . (g . x0); Gx0 in dom (Proj (i,n)) by A22; then (Proj (i,n)) . (g . x0) in rng (Proj (i,n)) by FUNCT_1:3; then reconsider ProjGx0 = (Proj (i,n)) . (g . x0) as Element of REAL 1 by REAL_NS1:def_4; reconsider Gx1 = Gx as Element of (REAL-NS n) by REAL_NS1:def_4; reconsider Gx01 = Gx0 as Element of (REAL-NS n) by REAL_NS1:def_4; reconsider Gsx = g /. x as Element of REAL n by REAL_NS1:def_4; reconsider Gsx0 = g /. x0 as Element of REAL n by REAL_NS1:def_4; set dxx0 = x - x0; reconsider Ldxx0 = L . (x - x0) as Element of (REAL-NS 1) ; A29: dom R = REAL by A8, PARTFUN1:def_2; then A30: R /. (x - x0) = R . (x - x0) by PARTFUN1:def_6; then reconsider Rdxx0 = R . (x - x0) as Element of (REAL-NS 1) ; reconsider Lxx0Rxx0 = (L . (x - x0)) + (R /. (x - x0)) as Element of REAL 1 by REAL_NS1:def_4; reconsider Ldiff = DFG . (x - x0) as Element of REAL n by REAL_NS1:def_4; set ProjLdiff = (Proj (i,n)) . Ldiff; (Proj (i,n)) . Ldiff in rng (Proj (i,n)) by A20, FUNCT_1:3; then reconsider ProjLdiff = (Proj (i,n)) . Ldiff as Element of REAL 1 by REAL_NS1:def_4; A31: dom GR = REAL by A7, PARTFUN1:def_2; then GR . (x - x0) in rng GR by FUNCT_1:3; then reconsider Rdiff = GR . (x - x0) as Element of REAL n by REAL_NS1:def_4; A32: Rdiff = GR /. (x - x0) by A31, PARTFUN1:def_6; set ProjRdiff = (Proj (i,n)) . Rdiff; (Proj (i,n)) . Rdiff in rng (Proj (i,n)) by A22, FUNCT_1:3; then reconsider ProjRdiff = (Proj (i,n)) . Rdiff as Element of REAL 1 by REAL_NS1:def_4; dom L = REAL by FUNCT_2:def_1; then ( L . (x - x0) = (Proj (i,n)) . Ldiff & R . (x - x0) = (Proj (i,n)) . Rdiff ) by A29, FUNCT_1:12; then A33: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by REAL_NS1:2; (Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*> by PDIFF_1:def_4; then A34: (Proj (i,n)) . Ldiff = <*(Ldiff . i)*> by PDIFF_1:def_1; Rdiff in dom (Proj (i,n)) by A22; then (Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*> by PDIFF_1:def_4; then A35: (Proj (i,n)) . Rdiff = <*(Rdiff . i)*> by PDIFF_1:def_1; reconsider diffGR = (DFG . (x - x0)) + (GR /. (x - x0)) as Element of REAL n by REAL_NS1:def_4; reconsider Rsdiff = GR /. (x - x0) as Element of REAL n by REAL_NS1:def_4; PGSx = PGdx - PGdx0 by A27, REAL_NS1:5 .= ProjGx - PGdx0 by A2, A21, A24, FUNCT_1:12 .= ProjGx - ProjGx0 by A2, A21, A26, FUNCT_1:12 .= <*((proj (i,n)) . Gx1)*> - ProjGx0 by PDIFF_1:def_4 .= <*((proj (i,n)) . Gx1)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_4 .= <*(Gx . i)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_1 .= <*(Gx . i)*> - <*(Gx0 . i)*> by PDIFF_1:def_1 .= <*((Gx . i) - (Gx0 . i))*> by RVSUM_1:29 .= <*((Gsx - Gsx0) . i)*> by A28, RVSUM_1:27 .= <*(diffGR . i)*> by A25, REAL_NS1:5 .= <*((Ldiff + Rsdiff) . i)*> by REAL_NS1:2 .= <*((Ldiff . i) + (Rsdiff . i))*> by RVSUM_1:11 ; hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A30, A33, A34, A35, A32, RVSUM_1:13; ::_thesis: verum end; hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ; ::_thesis: verum end; hence A36: (Proj (i,n)) * g is_differentiable_in x0 by A2, A21, NDIFF_3:def_3; ::_thesis: (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) L . 1 = 1 * ((Proj (i,n)) . LP) by A5 .= (Proj (i,n)) . LP by RLVECT_1:def_8 .= (Proj (i,n)) . (1 * LP) by RLVECT_1:def_8 .= (Proj (i,n)) . (diff (g,x0)) by A3, A4 ; hence (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) by A36, A2, A21, A23, NDIFF_3:def_4; ::_thesis: verum end; theorem Th25: :: NDIFF_4:25 for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) for x0 being real number holds ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) proof let n be non empty Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for x0 being real number holds ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for x0 being real number holds ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) let x0 be real number ; ::_thesis: ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) thus ( g is_differentiable_in x0 implies for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) by Th24; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ) implies g is_differentiable_in x0 ) assume A1: for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 ; ::_thesis: g is_differentiable_in x0 defpred S1[ Element of NAT , Element of REAL ] means ( \$2 > 0 & ].(x0 - \$2),(x0 + \$2).[ c= dom ((Proj (\$1,n)) * g) & ex Ri being RestFunc of (REAL-NS 1) st for x being Real st x in ].(x0 - \$2),(x0 + \$2).[ holds (((Proj (\$1,n)) * g) /. x) - (((Proj (\$1,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (\$1,n)) * g),x0))) + (Ri /. (x - x0)) ); A2: for k being Element of NAT st k in Seg n holds ex dk being Element of REAL st S1[k,dk] proof let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dk being Element of REAL st S1[k,dk] ) assume k in Seg n ; ::_thesis: ex dk being Element of REAL st S1[k,dk] then ( 1 <= k & k <= n ) by FINSEQ_1:1; then (Proj (k,n)) * g is_differentiable_in x0 by A1; then consider Nk being Neighbourhood of x0 such that A3: ( Nk c= dom ((Proj (k,n)) * g) & ex L being LinearFunc of (REAL-NS 1) ex Rk being RestFunc of (REAL-NS 1) st ( L . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (L . (x - x0)) + (Rk /. (x - x0)) ) ) ) by NDIFF_3:def_4; consider dk being real number such that A4: ( 0 < dk & Nk = ].(x0 - dk),(x0 + dk).[ ) by RCOMP_1:def_6; reconsider dk = dk as Element of REAL by XREAL_0:def_1; take dk ; ::_thesis: S1[k,dk] thus 0 < dk by A4; ::_thesis: ( ].(x0 - dk),(x0 + dk).[ c= dom ((Proj (k,n)) * g) & ex Ri being RestFunc of (REAL-NS 1) st for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Ri /. (x - x0)) ) thus ].(x0 - dk),(x0 + dk).[ c= dom ((Proj (k,n)) * g) by A4, A3; ::_thesis: ex Ri being RestFunc of (REAL-NS 1) st for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Ri /. (x - x0)) thus ex Rk being RestFunc of (REAL-NS 1) st for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) ::_thesis: verum proof consider L being LinearFunc of (REAL-NS 1), Rk being RestFunc of (REAL-NS 1) such that A5: ( L . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (L . (x - x0)) + (Rk /. (x - x0)) ) ) by A3; A6: now__::_thesis:_for_x_being_Real_st_x_in_Nk_holds_ (((Proj_(k,n))_*_g)_/._x)_-_(((Proj_(k,n))_*_g)_/._x0)_=_((x_-_x0)_*_(diff_(((Proj_(k,n))_*_g),x0)))_+_(Rk_/._(x_-_x0)) let x be Real; ::_thesis: ( x in Nk implies (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) ) assume A7: x in Nk ; ::_thesis: (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) consider L1 being Point of (REAL-NS 1) such that A8: for p being Real holds L . p = p * L1 by NDIFF_3:def_2; A9: diff (((Proj (k,n)) * g),x0) = 1 * L1 by A8, A5 .= L1 by RLVECT_1:def_8 ; A10: L . (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A9, A8; thus (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) by A10, A5, A7; ::_thesis: verum end; take Rk ; ::_thesis: for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) thus for x being Real st x in ].(x0 - dk),(x0 + dk).[ holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (Rk /. (x - x0)) by A4, A6; ::_thesis: verum end; end; consider d being FinSequence of REAL such that A11: ( dom d = Seg n & ( for k being Element of NAT st k in Seg n holds S1[k,d /. k] ) ) from RECDEF_1:sch_17(A2); set d0 = min d; len d = n by A11, FINSEQ_1:def_3; then A12: min_p d in dom d by RFINSEQ2:def_2; then d /. (min_p d) > 0 by A11; then A13: min d > 0 by A12, PARTFUN1:def_6; defpred S2[ Real, set ] means ex y being Element of REAL n st ( \$2 = y & ( for i being Element of NAT st i in Seg n holds y . i = (proj (1,1)) . (\$1 * (diff (((Proj (i,n)) * g),x0))) ) ); A14: for x being Real ex y being Point of (REAL-NS n) st S2[x,y] proof let x be Real; ::_thesis: ex y being Point of (REAL-NS n) st S2[x,y] defpred S3[ Element of NAT , set ] means \$2 = (proj (1,1)) . (x * (diff (((Proj (\$1,n)) * g),x0))); A15: for i being Element of NAT st i in Seg n holds ex r being Element of REAL st S3[i,r] ; consider y being FinSequence of REAL such that A16: ( dom y = Seg n & ( for i being Element of NAT st i in Seg n holds S3[i,y /. i] ) ) from RECDEF_1:sch_17(A15); len y = n by A16, FINSEQ_1:def_3; then reconsider y = y as Element of REAL n by FINSEQ_2:92; A17: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ y_._i_=_(proj_(1,1))_._(x_*_(diff_(((Proj_(i,n))_*_g),x0))) let i be Element of NAT ; ::_thesis: ( i in Seg n implies y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) ) assume i in Seg n ; ::_thesis: y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) then ( S3[i,y /. i] & y /. i = y . i ) by A16, PARTFUN1:def_6; hence y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) ; ::_thesis: verum end; reconsider y0 = y as Point of (REAL-NS n) by REAL_NS1:def_4; ex y being Element of REAL n st ( y0 = y & ( for i being Element of NAT st i in Seg n holds y . i = (proj (1,1)) . (x * (diff (((Proj (i,n)) * g),x0))) ) ) by A17; hence ex y0 being Point of (REAL-NS n) st S2[x,y0] ; ::_thesis: verum end; consider L being Function of REAL,(REAL-NS n) such that A18: for x being Real holds S2[x,L . x] from FUNCT_2:sch_3(A14); for r being Real holds L . r = r * (L . 1) proof let r be Real; ::_thesis: L . r = r * (L . 1) consider Lx being Element of REAL n such that A19: ( L . 1 = Lx & ( for i being Element of NAT st i in Seg n holds Lx . i = (proj (1,1)) . (1 * (diff (((Proj (i,n)) * g),x0))) ) ) by A18; A20: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ Lx_._i_=_(proj_(1,1))_._(diff_(((Proj_(i,n))_*_g),x0)) let i be Element of NAT ; ::_thesis: ( i in Seg n implies Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) ) assume i in Seg n ; ::_thesis: Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) then Lx . i = (proj (1,1)) . (1 * (diff (((Proj (i,n)) * g),x0))) by A19; hence Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) by RLVECT_1:def_8; ::_thesis: verum end; consider Lrx being Element of REAL n such that A21: ( L . r = Lrx & ( for i being Element of NAT st i in Seg n holds Lrx . i = (proj (1,1)) . (r * (diff (((Proj (i,n)) * g),x0))) ) ) by A18; A22: dom (r * Lx) = Seg n by FINSEQ_2:124; then A23: dom (r * Lx) = dom Lrx by FINSEQ_2:124; for i0 being Nat st i0 in dom (r * Lx) holds (r * Lx) . i0 = Lrx . i0 proof let i0 be Nat; ::_thesis: ( i0 in dom (r * Lx) implies (r * Lx) . i0 = Lrx . i0 ) reconsider i = i0 as Element of NAT by ORDINAL1:def_12; assume i0 in dom (r * Lx) ; ::_thesis: (r * Lx) . i0 = Lrx . i0 then A24: ( Lx . i = (proj (1,1)) . (diff (((Proj (i,n)) * g),x0)) & Lrx . i = (proj (1,1)) . (r * (diff (((Proj (i,n)) * g),x0))) ) by A20, A21, A22; A25: (r * 1) * (diff (((Proj (i,n)) * g),x0)) = r * (1 * (diff (((Proj (i,n)) * g),x0))) by RLVECT_1:def_8; reconsider Diffrx = (r * 1) * (diff (((Proj (i,n)) * g),x0)) as Element of REAL 1 by REAL_NS1:def_4; reconsider Diffx = 1 * (diff (((Proj (i,n)) * g),x0)) as Element of REAL 1 by REAL_NS1:def_4; A26: Diffx = diff (((Proj (i,n)) * g),x0) by RLVECT_1:def_8; Diffrx = r * Diffx by A25, REAL_NS1:3; then Lrx . i0 = (r * Diffx) . 1 by A24, PDIFF_1:def_1; then Lrx . i0 = r * (Diffx . 1) by RVSUM_1:45; then Lrx . i0 = r * (Lx . i0) by A24, A26, PDIFF_1:def_1; hence (r * Lx) . i0 = Lrx . i0 by RVSUM_1:45; ::_thesis: verum end; then r * Lx = Lrx by A23, FINSEQ_1:13; hence L . r = r * (L . 1) by A19, A21, REAL_NS1:3; ::_thesis: verum end; then reconsider L = L as linear Function of REAL,(REAL-NS n) by NDIFF_3:def_2; reconsider L0 = L as LinearFunc of (REAL-NS n) ; deffunc H1( Element of REAL ) -> Element of the carrier of (REAL-NS n) = ((g /. (\$1 + x0)) - (g /. x0)) - (L . \$1); consider R being Function of REAL,(REAL-NS n) such that A27: for x being Element of REAL holds R . x = H1(x) from FUNCT_2:sch_4(); A28: for x being Element of REAL for i being Element of NAT st i in Seg n & x + x0 in dom g holds ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) proof let x be Element of REAL ; ::_thesis: for i being Element of NAT st i in Seg n & x + x0 in dom g holds ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) let i be Element of NAT ; ::_thesis: ( i in Seg n & x + x0 in dom g implies ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) ) assume that A29: i in Seg n and A30: x + x0 in dom g ; ::_thesis: ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) A31: |.(x0 - x0).| = 0 by COMPLEX1:44; A32: ( 0 < d /. i & ].(x0 - (d /. i)),(x0 + (d /. i)).[ c= dom ((Proj (i,n)) * g) ) by A29, A11; then x0 in ].(x0 - (d /. i)),(x0 + (d /. i)).[ by A31, RCOMP_1:1; then A33: x0 in dom ((Proj (i,n)) * g) by A32; A34: dom ((Proj (i,n)) * g) c= dom g by RELAT_1:25; reconsider gxx0 = g /. (x + x0), gx0 = g /. x0, Lx = L . x as Element of REAL n by REAL_NS1:def_4; reconsider gxx01 = g /. (x + x0), gx01 = g /. x0, Lx1 = L . x as Point of (REAL-NS n) ; A35: ( - gx0 = (- 1) * (g /. x0) & - Lx = (- 1) * (L . x) ) by REAL_NS1:3; then gxx0 + (- gx0) = (g /. (x + x0)) + ((- 1) * (g /. x0)) by REAL_NS1:2; then A36: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L . x)) by A35, REAL_NS1:2; A37: - 1 is Real by XREAL_0:def_1; gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5; then A38: ((g /. (x + x0)) - (g /. x0)) - (L . x) = (gxx0 - gx0) - Lx by REAL_NS1:5; ((Proj (i,n)) * R) . x = (Proj (i,n)) . (R . x) by FUNCT_2:15; then ((Proj (i,n)) * R) . x = (Proj (i,n)) . (((g /. (x + x0)) - (g /. x0)) - (L . x)) by A27; then ((Proj (i,n)) * R) . x = ((Proj (i,n)) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by A38, A36, PDIFF_6:26; then A39: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + ((Proj (i,n)) . ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by PDIFF_6:26; ( (Proj (i,n)) . ((- 1) * (g /. x0)) = (- 1) * ((Proj (i,n)) . (g /. x0)) & (Proj (i,n)) . ((- 1) * Lx1) = (- 1) * ((Proj (i,n)) . Lx1) ) by A37, PDIFF_6:27; then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + ((- 1) * ((Proj (i,n)) . (L . x))) by A39, RLVECT_1:16; then A40: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) - ((Proj (i,n)) . (L . x)) by RLVECT_1:16; ( g /. (x + x0) in the carrier of (REAL-NS n) & g /. x0 in the carrier of (REAL-NS n) ) ; then A41: ( g /. (x + x0) in dom (Proj (i,n)) & g /. x0 in dom (Proj (i,n)) ) by FUNCT_2:def_1; A42: (Proj (i,n)) . (g /. (x + x0)) = (Proj (i,n)) /. (g /. (x + x0)) .= ((Proj (i,n)) * g) /. (x + x0) by A30, A41, PARTFUN2:4 ; (Proj (i,n)) . (g /. x0) = (Proj (i,n)) /. (g /. x0) .= ((Proj (i,n)) * g) /. x0 by A33, A34, A41, PARTFUN2:4 ; hence ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) by A40, A42, FUNCT_2:15; ::_thesis: verum end; for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) proof let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) ) assume A43: r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) set r0 = ((sqrt n) ") * r; A44: sqrt n > 0 by SQUARE_1:25; then A45: ((sqrt n) ") * r > 0 by A43, XREAL_1:129; defpred S3[ Element of NAT , Element of REAL ] means ( \$2 > 0 & ( for z being Real st z <> 0 & |.z.| < \$2 holds (|.z.| ") * ||.(((Proj (\$1,n)) * R) /. z).|| < ((sqrt n) ") * r ) ); A46: for k being Element of NAT st k in Seg n holds ex dd being Element of REAL st S3[k,dd] proof let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dd being Element of REAL st S3[k,dd] ) assume A47: k in Seg n ; ::_thesis: ex dd being Element of REAL st S3[k,dd] then ( 1 <= k & k <= n ) by FINSEQ_1:1; then (Proj (k,n)) * g is_differentiable_in x0 by A1; then consider Nk being Neighbourhood of x0 such that A48: ( Nk c= dom ((Proj (k,n)) * g) & ex LR being LinearFunc of (REAL-NS 1) ex PR being RestFunc of (REAL-NS 1) st ( LR . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (LR . (x - x0)) + (PR /. (x - x0)) ) ) ) by NDIFF_3:def_4; consider d0 being real number such that A49: ( 0 < d0 & Nk = ].(x0 - d0),(x0 + d0).[ ) by RCOMP_1:def_6; reconsider d0 = d0 as Real by XREAL_0:def_1; consider LR being LinearFunc of (REAL-NS 1), PR being RestFunc of (REAL-NS 1) such that A50: ( LR . 1 = diff (((Proj (k,n)) * g),x0) & ( for x being Real st x in Nk holds (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = (LR . (x - x0)) + (PR /. (x - x0)) ) ) by A48; A51: now__::_thesis:_for_x_being_Real_st_x_in_Nk_holds_ (((Proj_(k,n))_*_g)_/._x)_-_(((Proj_(k,n))_*_g)_/._x0)_=_((x_-_x0)_*_(diff_(((Proj_(k,n))_*_g),x0)))_+_(PR_/._(x_-_x0)) let x be Real; ::_thesis: ( x in Nk implies (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) ) assume A52: x in Nk ; ::_thesis: (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) consider L1 being Point of (REAL-NS 1) such that A53: for p being Real holds LR . p = p * L1 by NDIFF_3:def_2; diff (((Proj (k,n)) * g),x0) = 1 * L1 by A53, A50 .= L1 by RLVECT_1:def_8 ; then LR . (x - x0) = (x - x0) * (diff (((Proj (k,n)) * g),x0)) by A53; hence (((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((x - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. (x - x0)) by A52, A50; ::_thesis: verum end; PR is total by NDIFF_3:def_1; then consider d1 being Real such that A54: ( d1 > 0 & ( for z being Real st z <> 0 & |.z.| < d1 holds (|.z.| ") * ||.(PR /. z).|| < ((sqrt n) ") * r ) ) by A45, Th23; set dd = min (d0,d1); take min (d0,d1) ; ::_thesis: S3[k, min (d0,d1)] for z being Real st z <> 0 & |.z.| < min (d0,d1) holds (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r proof let z be Real; ::_thesis: ( z <> 0 & |.z.| < min (d0,d1) implies (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r ) assume A55: ( z <> 0 & |.z.| < min (d0,d1) ) ; ::_thesis: (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r min (d0,d1) <= d1 by XXREAL_0:17; then |.z.| < d1 by A55, XXREAL_0:2; then A56: (|.z.| ") * ||.(PR /. z).|| < ((sqrt n) ") * r by A55, A54; min (d0,d1) <= d0 by XXREAL_0:17; then A57: |.z.| < d0 by A55, XXREAL_0:2; (z + x0) - x0 = z ; then A58: z + x0 in ].(x0 - d0),(x0 + d0).[ by A57, RCOMP_1:1; then A59: z + x0 in dom ((Proj (k,n)) * g) by A48, A49; (((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0) = (((z + x0) - x0) * (diff (((Proj (k,n)) * g),x0))) + (PR /. ((z + x0) - x0)) by A58, A49, A51; then A60: PR /. z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (z * (diff (((Proj (k,n)) * g),x0))) by RLVECT_4:1; dom ((Proj (k,n)) * g) c= dom g by RELAT_1:25; then A61: ((Proj (k,n)) * R) . z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (((Proj (k,n)) * L) . z) by A59, A47, A28; consider y being Element of REAL n such that A62: ( L . z = y & ( for i being Element of NAT st i in Seg n holds y . i = (proj (1,1)) . (z * (diff (((Proj (i,n)) * g),x0))) ) ) by A18; A63: y . k = (proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))) by A62, A47; z * (diff (((Proj (k,n)) * g),x0)) is Element of REAL 1 by REAL_NS1:def_4; then consider Dk being Element of REAL such that A64: z * (diff (((Proj (k,n)) * g),x0)) = <*Dk*> by FINSEQ_2:97; reconsider y1 = y as Point of (REAL-NS n) by REAL_NS1:def_4; dom L = REAL by FUNCT_2:def_1; then ((Proj (k,n)) * L) . z = (Proj (k,n)) . (L . z) by FUNCT_1:13; then ((Proj (k,n)) * L) . z = <*((proj (k,n)) . y1)*> by A62, PDIFF_1:def_4; then ((Proj (k,n)) * L) . z = <*((proj (1,1)) . (z * (diff (((Proj (k,n)) * g),x0))))*> by A63, PDIFF_1:def_1; hence (|.z.| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r by A56, A60, A61, A64, PDIFF_1:1; ::_thesis: verum end; hence S3[k, min (d0,d1)] by A49, A54, XXREAL_0:21; ::_thesis: verum end; consider dd being FinSequence of REAL such that A65: ( dom dd = Seg n & ( for i being Element of NAT st i in Seg n holds S3[i,dd /. i] ) ) from RECDEF_1:sch_17(A46); take d = min dd; ::_thesis: ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) len dd = n by A65, FINSEQ_1:def_3; then A66: min_p dd in dom dd by RFINSEQ2:def_2; then A67: dd /. (min_p dd) > 0 by A65; for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r proof let z be Real; ::_thesis: ( z <> 0 & |.z.| < d implies (|.z.| ") * ||.(R /. z).|| < r ) assume A68: ( z <> 0 & |.z.| < d ) ; ::_thesis: (|.z.| ") * ||.(R /. z).|| < r reconsider Rz = R /. z as Element of REAL n by REAL_NS1:def_4; reconsider R0 = n |-> ((|.z.| * (((sqrt n) ") * r)) ^2) as Element of n -tuples_on REAL ; reconsider SRz = sqr Rz as Element of n -tuples_on REAL ; A69: |.z.| > 0 by A68, COMPLEX1:47; A70: for i0 being Nat st i0 in Seg n holds SRz . i0 < R0 . i0 proof let i0 be Nat; ::_thesis: ( i0 in Seg n implies SRz . i0 < R0 . i0 ) reconsider i = i0 as Element of NAT by ORDINAL1:def_12; assume A71: i0 in Seg n ; ::_thesis: SRz . i0 < R0 . i0 then i in dom Rz by FINSEQ_2:124; then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13; then A72: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2; ( 1 <= i & i <= n ) by A71, FINSEQ_1:1; then ( 1 <= i & i <= len dd ) by A65, FINSEQ_1:def_3; then d <= dd . i by RFINSEQ2:2; then d <= dd /. i by A71, A65, PARTFUN1:def_6; then |.z.| < dd /. i by A68, XXREAL_0:2; then (|.z.| ") * ||.(((Proj (i,n)) * R) /. z).|| < ((sqrt n) ") * r by A68, A71, A65; then A73: ||.(((Proj (i,n)) * R) /. z).|| < (((sqrt n) ") * r) / (|.z.| ") by A69, XREAL_1:81; reconsider Rzi = <*(Rz . i)*> as Element of REAL 1 by FINSEQ_2:98; ((Proj (i,n)) * R) . z = (Proj (i,n)) . (R . z) by FUNCT_2:15; then ((Proj (i,n)) * R) . z = <*((proj (i,n)) . Rz)*> by PDIFF_1:def_4; then ((Proj (i,n)) * R) . z = <*(Rz . i)*> by PDIFF_1:def_1; then ||.(((Proj (i,n)) * R) . z).|| = |.Rzi.| by REAL_NS1:1; then |.(Rz . i).| < |.z.| * (((sqrt n) ") * r) by A73, JORDAN2C:10; then |.(Rz . i).| ^2 < (|.z.| * (((sqrt n) ") * r)) ^2 by COMPLEX1:46, SQUARE_1:16; then (Rz . i0) ^2 < (|.z.| * (((sqrt n) ") * r)) ^2 by COMPLEX1:75; hence SRz . i0 < R0 . i0 by A71, A72, FINSEQ_2:57; ::_thesis: verum end; A74: for i being Nat st i in dom (sqr Rz) holds 0 <= (sqr Rz) . i proof let i be Nat; ::_thesis: ( i in dom (sqr Rz) implies 0 <= (sqr Rz) . i ) assume i in dom (sqr Rz) ; ::_thesis: 0 <= (sqr Rz) . i then ( i in dom (sqrreal * Rz) & dom (sqrreal * Rz) c= dom Rz ) by RELAT_1:25; then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13; then (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2; hence 0 <= (sqr Rz) . i by XREAL_1:63; ::_thesis: verum end; A75: (|.z.| * (((sqrt n) ") * r)) ^2 >= 0 by XREAL_1:63; A76: ex i being Nat st ( i in Seg n & SRz . i < R0 . i ) proof take 1 ; ::_thesis: ( 1 in Seg n & SRz . 1 < R0 . 1 ) 1 <= n by NAT_1:14; hence 1 in Seg n ; ::_thesis: SRz . 1 < R0 . 1 hence SRz . 1 < R0 . 1 by A70; ::_thesis: verum end; A77: sqrt n > 0 by SQUARE_1:25; for i0 being Nat st i0 in Seg n holds SRz . i0 <= R0 . i0 by A70; then Sum SRz < Sum R0 by A76, RVSUM_1:83; then Sum (sqr Rz) < n * ((|.z.| * (((sqrt n) ") * r)) ^2) by RVSUM_1:80; then |.Rz.| < sqrt (n * ((|.z.| * (((sqrt n) ") * r)) ^2)) by A74, RVSUM_1:84, SQUARE_1:27; then |.Rz.| < (sqrt n) * (sqrt ((|.z.| * (((sqrt n) ") * r)) ^2)) by A75, SQUARE_1:29; then |.Rz.| < (sqrt n) * |.(|.z.| * (((sqrt n) ") * r)).| by COMPLEX1:72; then |.Rz.| < (sqrt n) * (|.z.| * (((sqrt n) ") * r)) by A44, A43, A69, ABSVALUE:def_1; then |.Rz.| < ((sqrt n) * (((sqrt n) ") * r)) * |.z.| ; then |.Rz.| / |.z.| < (sqrt n) * (((sqrt n) ") * r) by A69, XREAL_1:83; then (|.z.| ") * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) ")) * r by REAL_NS1:1; then (|.z.| ") * ||.(R /. z).|| < 1 * r by A77, XCMPLX_0:def_7; hence (|.z.| ") * ||.(R /. z).|| < r ; ::_thesis: verum end; hence ( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < r ) ) by A67, A66, PARTFUN1:def_6; ::_thesis: verum end; then reconsider R = R as RestFunc of (REAL-NS n) by Th23; reconsider N = ].(x0 - (min d)),(x0 + (min d)).[ as Neighbourhood of x0 by A13, RCOMP_1:def_6; now__::_thesis:_for_x_being_set_st_x_in_N_holds_ x_in_dom_g let x be set ; ::_thesis: ( x in N implies x in dom g ) assume A78: x in N ; ::_thesis: x in dom g then reconsider y = x as Real ; A79: |.(y - x0).| < min d by A78, RCOMP_1:1; 1 <= n by NAT_1:14; then A80: ( 1 in Seg n & 1 in dom d ) by A11; then A81: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom ((Proj (1,n)) * g) by A11; dom ((Proj (1,n)) * g) c= dom g by RELAT_1:25; then A82: ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ c= dom g by A81, XBOOLE_1:1; len d = n by A11, FINSEQ_1:def_3; then 1 <= len d by NAT_1:14; then min d <= d . 1 by RFINSEQ2:2; then min d <= d /. 1 by A80, PARTFUN1:def_6; then |.(y - x0).| < d /. 1 by A79, XXREAL_0:2; then y in ].(x0 - (d /. 1)),(x0 + (d /. 1)).[ by RCOMP_1:1; hence x in dom g by A82; ::_thesis: verum end; then A83: N c= dom g by TARSKI:def_3; ex L being LinearFunc of (REAL-NS n) ex R being RestFunc of (REAL-NS n) st for x being Real st x in N holds (g /. x) - (g /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof take L0 ; ::_thesis: ex R being RestFunc of (REAL-NS n) st for x being Real st x in N holds (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) take R ; ::_thesis: for x being Real st x in N holds (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) let x be Real; ::_thesis: ( x in N implies (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) A84: dom R = REAL by PARTFUN1:def_2; R . (x - x0) = ((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0)) by A27; then R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by A84, PARTFUN1:def_6; then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + ((- (L0 . (x - x0))) + (L0 . (x - x0))) by RLVECT_1:def_3; then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + (0. (REAL-NS n)) by RLVECT_1:5; hence (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) by RLVECT_1:4; ::_thesis: verum end; hence g is_differentiable_in x0 by A83, NDIFF_3:def_3; ::_thesis: verum end; theorem :: NDIFF_4:26 for i being Element of NAT for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for x0 being real number st 1 <= i & i <= n & f is_differentiable_in x0 holds ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) proof let i be Element of NAT ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for x0 being real number st 1 <= i & i <= n & f is_differentiable_in x0 holds ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for x0 being real number st 1 <= i & i <= n & f is_differentiable_in x0 holds ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) let f be PartFunc of REAL,(REAL n); ::_thesis: for x0 being real number st 1 <= i & i <= n & f is_differentiable_in x0 holds ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) let x0 be real number ; ::_thesis: ( 1 <= i & i <= n & f is_differentiable_in x0 implies ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) ) assume A1: ( 1 <= i & i <= n & f is_differentiable_in x0 ) ; ::_thesis: ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) then consider g being PartFunc of REAL,(REAL-NS n) such that A2: ( f = g & g is_differentiable_in x0 ) by Def1; diff (f,x0) = diff (g,x0) by A2, Th3; hence ( (Proj (i,n)) * f is_differentiable_in x0 & (Proj (i,n)) . (diff (f,x0)) = diff (((Proj (i,n)) * f),x0) ) by A2, A1, Th24; ::_thesis: verum end; theorem :: NDIFF_4:27 for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) for x0 being real number holds ( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 ) proof let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for x0 being real number holds ( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 ) let f be PartFunc of REAL,(REAL n); ::_thesis: for x0 being real number holds ( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 ) let x0 be real number ; ::_thesis: ( f is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 ) thus ( f is_differentiable_in x0 implies for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 ) ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 ) implies f is_differentiable_in x0 ) proof assume f is_differentiable_in x0 ; ::_thesis: for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 then ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & g is_differentiable_in x0 ) by Def1; hence for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 by Th25; ::_thesis: verum end; assume A1: for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_in x0 ; ::_thesis: f is_differentiable_in x0 reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_in x0 by A1; then g is_differentiable_in x0 by Th25; hence f is_differentiable_in x0 by Def1; ::_thesis: verum end; theorem Th28: :: NDIFF_4:28 for X being set for i being Element of NAT for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) proof let X be set ; ::_thesis: for i being Element of NAT for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) let i be Element of NAT ; ::_thesis: for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) let n be non empty Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( 1 <= i & i <= n & g is_differentiable_on X implies ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) ) assume A1: ( 1 <= i & i <= n & g is_differentiable_on X ) ; ::_thesis: ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) then A2: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11; A3: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; rng g c= the carrier of (REAL-NS n) ; then dom ((Proj (i,n)) * g) = dom g by A3, RELAT_1:27; then A4: X c= dom ((Proj (i,n)) * g) by A2, A1, NDIFF_3:10; now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ (Proj_(i,n))_*_g_is_differentiable_in_x let x be Real; ::_thesis: ( x in X implies (Proj (i,n)) * g is_differentiable_in x ) assume x in X ; ::_thesis: (Proj (i,n)) * g is_differentiable_in x then g is_differentiable_in x by A2, A1, NDIFF_3:10; hence (Proj (i,n)) * g is_differentiable_in x by A1, Th24; ::_thesis: verum end; hence A5: (Proj (i,n)) * g is_differentiable_on X by A2, A4, NDIFF_3:10; ::_thesis: (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X then A6: ( dom (((Proj (i,n)) * g) `| X) = X & ( for x being Real st x in X holds (((Proj (i,n)) * g) `| X) . x = diff (((Proj (i,n)) * g),x) ) ) by NDIFF_3:def_6; A7: ( dom (g `| X) = X & ( for x being Real st x in X holds (g `| X) . x = diff (g,x) ) ) by A1, NDIFF_3:def_6; rng (g `| X) c= the carrier of (REAL-NS n) ; then A8: dom ((Proj (i,n)) * (g `| X)) = dom (g `| X) by A3, RELAT_1:27; now__::_thesis:_for_x_being_Real_st_x_in_dom_(((Proj_(i,n))_*_g)_`|_X)_holds_ ((Proj_(i,n))_*_(g_`|_X))_._x_=_(((Proj_(i,n))_*_g)_`|_X)_._x let x be Real; ::_thesis: ( x in dom (((Proj (i,n)) * g) `| X) implies ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x ) assume A9: x in dom (((Proj (i,n)) * g) `| X) ; ::_thesis: ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x then A10: x in X by A5, NDIFF_3:def_6; then g is_differentiable_in x by A2, A1, NDIFF_3:10; then A11: (Proj (i,n)) . (diff (g,x)) = diff (((Proj (i,n)) * g),x) by A1, Th24; A12: (((Proj (i,n)) * g) `| X) . x = diff (((Proj (i,n)) * g),x) by A9, A6; (g `| X) . x = diff (g,x) by A10, A1, NDIFF_3:def_6; hence ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x by A7, A10, A11, A12, FUNCT_1:13; ::_thesis: verum end; hence (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X by A8, A6, A7, PARTFUN1:5; ::_thesis: verum end; theorem Th29: :: NDIFF_4:29 for X being set for i being Element of NAT for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) proof let X be set ; ::_thesis: for i being Element of NAT for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) let i be Element of NAT ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( 1 <= i & i <= n & f is_differentiable_on X implies ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) ) assume A1: ( 1 <= i & i <= n & f is_differentiable_on X ) ; ::_thesis: ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) then A2: X is open Subset of REAL by Th4, Th6; reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A3: X c= dom g by A2, A1, Th5; now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ g_is_differentiable_in_x let x be Real; ::_thesis: ( x in X implies g is_differentiable_in x ) assume x in X ; ::_thesis: g is_differentiable_in x then f is_differentiable_in x by A2, A1, Th5; hence g is_differentiable_in x by Th2; ::_thesis: verum end; then A4: g is_differentiable_on X by A2, A3, NDIFF_3:10; hence (Proj (i,n)) * f is_differentiable_on X by A1, Th28; ::_thesis: (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X A5: ( dom (g `| X) = X & ( for x being Real st x in X holds (g `| X) . x = diff (g,x) ) ) by A4, NDIFF_3:def_6; A6: dom (f `| X) = dom (g `| X) by A1, Def4, A5; A7: now__::_thesis:_for_x_being_Real_st_x_in_dom_(f_`|_X)_holds_ (f_`|_X)_._x_=_(g_`|_X)_._x let x be Real; ::_thesis: ( x in dom (f `| X) implies (f `| X) . x = (g `| X) . x ) assume x in dom (f `| X) ; ::_thesis: (f `| X) . x = (g `| X) . x then A8: x in X by A1, Def4; then A9: (f `| X) . x = diff (f,x) by A1, Def4; diff (f,x) = diff (g,x) by Th3; hence (f `| X) . x = (g `| X) . x by A9, A8, A4, NDIFF_3:def_6; ::_thesis: verum end; g `| X is PartFunc of REAL,(REAL n) by REAL_NS1:def_4; then (Proj (i,n)) * (f `| X) = (Proj (i,n)) * (g `| X) by A6, A7, PARTFUN1:5; hence (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X by A4, A1, Th28; ::_thesis: verum end; theorem Th30: :: NDIFF_4:30 for X being set for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) holds ( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X ) proof let X be set ; ::_thesis: for n being non empty Element of NAT for g being PartFunc of REAL,(REAL-NS n) holds ( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X ) let n be non empty Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) holds ( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( g is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X ) thus ( g is_differentiable_on X implies for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X ) by Th28; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X ) implies g is_differentiable_on X ) assume A1: for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X ; ::_thesis: g is_differentiable_on X 1 <= n by NAT_1:14; then A2: (Proj (1,n)) * g is_differentiable_on X by A1; then A3: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11; A4: dom (Proj (1,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; A5: rng g c= the carrier of (REAL-NS n) ; X c= dom ((Proj (1,n)) * g) by A2, A3, NDIFF_3:10; then A6: X c= dom g by A5, A4, RELAT_1:27; now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ g_is_differentiable_in_x let x be Real; ::_thesis: ( x in X implies g is_differentiable_in x ) assume A7: x in X ; ::_thesis: g is_differentiable_in x now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_ (Proj_(i,n))_*_g_is_differentiable_in_x let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies (Proj (i,n)) * g is_differentiable_in x ) assume ( 1 <= i & i <= n ) ; ::_thesis: (Proj (i,n)) * g is_differentiable_in x then (Proj (i,n)) * g is_differentiable_on X by A1; hence (Proj (i,n)) * g is_differentiable_in x by A7, A3, NDIFF_3:10; ::_thesis: verum end; hence g is_differentiable_in x by Th25; ::_thesis: verum end; hence g is_differentiable_on X by A3, A6, NDIFF_3:10; ::_thesis: verum end; theorem :: NDIFF_4:31 for X being set for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) holds ( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_on X ) proof let X be set ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) holds ( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_on X ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds ( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_on X ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_differentiable_on X iff for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_on X ) thus ( f is_differentiable_on X implies for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_on X ) by Th29; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_on X ) implies f is_differentiable_on X ) assume A1: for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * f is_differentiable_on X ; ::_thesis: f is_differentiable_on X reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; for i being Element of NAT st 1 <= i & i <= n holds (Proj (i,n)) * g is_differentiable_on X by A1; then A2: g is_differentiable_on X by Th30; then A3: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11; then A4: X c= dom f by A2, NDIFF_3:10; now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ f_is_differentiable_in_x let x be Real; ::_thesis: ( x in X implies f is_differentiable_in x ) assume x in X ; ::_thesis: f is_differentiable_in x then g is_differentiable_in x by A3, A2, NDIFF_3:10; hence f is_differentiable_in x by Def1; ::_thesis: verum end; hence f is_differentiable_on X by A3, A4, Th5; ::_thesis: verum end; theorem Th32: :: NDIFF_4:32 for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds J is_continuous_in x0 proof let J be Function of (REAL-NS 1),REAL; ::_thesis: for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds J is_continuous_in x0 let x0 be Point of (REAL-NS 1); ::_thesis: ( J = proj (1,1) implies J is_continuous_in x0 ) assume A1: J = proj (1,1) ; ::_thesis: J is_continuous_in x0 A2: dom J = the carrier of (REAL-NS 1) by FUNCT_2:def_1; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1_being_Point_of_(REAL-NS_1)_st_x1_in_dom_J_&_||.(x1_-_x0).||_<_s_holds_ abs_((J_/._x1)_-_(J_/._x0))_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds abs ((J /. x1) - (J /. x0)) < r ) ) ) assume A3: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds abs ((J /. x1) - (J /. x0)) < r ) ) take s = r; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds abs ((J /. x1) - (J /. x0)) < r ) ) thus 0 < s by A3; ::_thesis: for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds abs ((J /. x1) - (J /. x0)) < r thus for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds abs ((J /. x1) - (J /. x0)) < r ::_thesis: verum proof let x1 be Point of (REAL-NS 1); ::_thesis: ( x1 in dom J & ||.(x1 - x0).|| < s implies abs ((J /. x1) - (J /. x0)) < r ) (J /. x1) - (J /. x0) = J . (x1 - x0) by A1, PDIFF_1:4; hence ( x1 in dom J & ||.(x1 - x0).|| < s implies abs ((J /. x1) - (J /. x0)) < r ) by A1, PDIFF_1:4; ::_thesis: verum end; end; hence J is_continuous_in x0 by A2, NFCONT_1:8; ::_thesis: verum end; theorem Th33: :: NDIFF_4:33 for x0 being Real for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds I is_continuous_in x0 proof let x0 be Real; ::_thesis: for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds I is_continuous_in x0 let I be Function of REAL,(REAL-NS 1); ::_thesis: ( I = (proj (1,1)) " implies I is_continuous_in x0 ) assume A1: I = (proj (1,1)) " ; ::_thesis: I is_continuous_in x0 A2: I is Function of REAL,(REAL 1) by REAL_NS1:def_4; A3: dom I = REAL by FUNCT_2:def_1; reconsider y0 = x0 as real number ; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_real_number_st_ (_0_<_s_&_(_for_y1_being_real_number_st_y1_in_dom_I_&_abs_(y1_-_y0)_<_s_holds_ ||.((I_/._y1)_-_(I_/._y0)).||_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds ||.((I /. y1) - (I /. y0)).|| < r ) ) ) assume A4: 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds ||.((I /. y1) - (I /. y0)).|| < r ) ) reconsider s1 = r as real number ; take s = s1; ::_thesis: ( 0 < s & ( for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds ||.((I /. y1) - (I /. y0)).|| < r ) ) thus 0 < s by A4; ::_thesis: for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds ||.((I /. y1) - (I /. y0)).|| < r thus for y1 being real number st y1 in dom I & abs (y1 - y0) < s holds ||.((I /. y1) - (I /. y0)).|| < r ::_thesis: verum proof let y1 be real number ; ::_thesis: ( y1 in dom I & abs (y1 - y0) < s implies ||.((I /. y1) - (I /. y0)).|| < r ) assume A5: ( y1 in dom I & abs (y1 - y0) < s ) ; ::_thesis: ||.((I /. y1) - (I /. y0)).|| < r reconsider x1 = y1 as Element of REAL by XREAL_0:def_1; (I /. x1) - (I /. x0) = I . (x1 - x0) by A1, A2, PDIFF_1:3; hence ||.((I /. y1) - (I /. y0)).|| < r by A5, A1, A2, PDIFF_1:3; ::_thesis: verum end; end; hence I is_continuous_in x0 by A3, NFCONT_3:8; ::_thesis: verum end; theorem Th34: :: NDIFF_4:34 for S, T being RealNormSpace for f1 being PartFunc of S,REAL for f2 being PartFunc of REAL,T for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 proof let S, T be RealNormSpace; ::_thesis: for f1 being PartFunc of S,REAL for f2 being PartFunc of REAL,T for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let f1 be PartFunc of S,REAL; ::_thesis: for f2 being PartFunc of REAL,T for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let f2 be PartFunc of REAL,T; ::_thesis: for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let x0 be Point of S; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 ) assume A1: x0 in dom (f2 * f1) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 /. x0 or f2 * f1 is_continuous_in x0 ) assume that A2: f1 is_continuous_in x0 and A3: f2 is_continuous_in f1 /. x0 ; ::_thesis: f2 * f1 is_continuous_in x0 thus x0 in dom (f2 * f1) 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 (f2 * f1) or not b1 is convergent or not lim b1 = x0 or ( (f2 * f1) /* b1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* b1) ) ) let s1 be sequence of S; ::_thesis: ( not rng s1 c= dom (f2 * f1) or not s1 is convergent or not lim s1 = x0 or ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) ) assume that A4: rng s1 c= dom (f2 * f1) and A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) A6: dom (f2 * f1) c= dom f1 by RELAT_1:25; now__::_thesis:_for_x_being_set_st_x_in_rng_(f1_/*_s1)_holds_ x_in_dom_f2 let x be set ; ::_thesis: ( x in rng (f1 /* s1) implies x in dom f2 ) assume x in rng (f1 /* s1) ; ::_thesis: x in dom f2 then consider n being Element of NAT such that A7: x = (f1 /* s1) . n by FUNCT_2:113; s1 . n in rng s1 by VALUED_0:28; then f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11; hence x in dom f2 by A4, A6, A7, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; then A8: rng (f1 /* s1) c= dom f2 by TARSKI:def_3; A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f2_*_f1)_/*_s1)_._n_=_(f2_/*_(f1_/*_s1))_._n let n be Element of NAT ; ::_thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n s1 . n in rng s1 by VALUED_0:28; then A10: s1 . n in dom f1 by A4, FUNCT_1:11; thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108 .= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:13 .= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1 .= (f2 /* (f1 /* s1)) . n by A8, FUNCT_2:108 ; ::_thesis: verum end; then A11: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63; rng s1 c= dom f1 by A4, A6, XBOOLE_1:1; then A12: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) ) by A2, A5, NFCONT_1:def_6; (f2 * f1) /. x0 = f2 /. (f1 /. x0) by A1, PARTFUN2:3 .= lim (f2 /* (f1 /* s1)) by A12, A3, A8, NFCONT_3:def_1 .= lim ((f2 * f1) /* s1) by A9, FUNCT_2:63 ; hence ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) by A3, A12, A8, A11, NFCONT_3:def_1; ::_thesis: verum end; Lm2: ( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds ( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) proof set f = proj (1,1); for y being set st y in REAL holds ex x being set st ( x in REAL 1 & y = (proj (1,1)) . x ) proof let y be set ; ::_thesis: ( y in REAL implies ex x being set st ( x in REAL 1 & y = (proj (1,1)) . x ) ) assume y in REAL ; ::_thesis: ex x being set st ( x in REAL 1 & y = (proj (1,1)) . x ) then reconsider y1 = y as Element of REAL ; reconsider x = <*y1*> as Element of REAL 1 by FINSEQ_2:98; (proj (1,1)) . x = x . 1 by PDIFF_1:def_1; then (proj (1,1)) . x = y by FINSEQ_1:40; hence ex x being set st ( x in REAL 1 & y = (proj (1,1)) . x ) ; ::_thesis: verum end; hence ( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds ( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by FUNCT_2:10, FUNCT_2:def_1, PDIFF_1:1; ::_thesis: verum end; theorem :: NDIFF_4:35 for n being non empty Element of NAT for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) proof let n be non empty Element of NAT ; ::_thesis: for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let J be Function of (REAL-NS 1),REAL; ::_thesis: for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let x0 be Point of (REAL-NS 1); ::_thesis: for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let y0 be Element of REAL ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) ) assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J ) ; ::_thesis: ( f is_continuous_in x0 iff g is_continuous_in y0 ) thus ( f is_continuous_in x0 implies g is_continuous_in y0 ) ::_thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 ) proof reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def_4; A2: J * I = id REAL by A1, Lm2, FUNCT_1:39; A3: f * I = g * (id REAL) by A1, A2, RELAT_1:36 .= g by FUNCT_2:17 ; I /. y0 = x0 by A1, PDIFF_1:1; hence ( f is_continuous_in x0 implies g is_continuous_in y0 ) by A3, Th33, A1, NFCONT_3:15; ::_thesis: verum end; J /. x0 = y0 by A1, PDIFF_1:1; hence ( g is_continuous_in y0 implies f is_continuous_in x0 ) by A1, Th32, Th34; ::_thesis: verum end; theorem :: NDIFF_4:36 for n being non empty Element of NAT for I being Function of REAL,(REAL-NS 1) for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) proof let n be non empty Element of NAT ; ::_thesis: for I being Function of REAL,(REAL-NS 1) for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let I be Function of REAL,(REAL-NS 1); ::_thesis: for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let x0 be Point of (REAL-NS 1); ::_thesis: for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let y0 be Element of REAL ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_continuous_in x0 iff g is_continuous_in y0 ) let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) ) assume A1: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g ) ; ::_thesis: ( f is_continuous_in x0 iff g is_continuous_in y0 ) reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1; thus ( f is_continuous_in x0 implies g is_continuous_in y0 ) ::_thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 ) proof I /. y0 = x0 by A1, PDIFF_1:1; hence ( f is_continuous_in x0 implies g is_continuous_in y0 ) by A1, Th33, NFCONT_3:15; ::_thesis: verum end; A2: I * J = id (REAL-NS 1) by A1, Lm2, Lm1, FUNCT_1:39; A3: g * J = f * (id (REAL-NS 1)) by A2, A1, RELAT_1:36 .= f by FUNCT_2:17 ; J /. x0 = y0 by A1, PDIFF_1:1; hence ( g is_continuous_in y0 implies f is_continuous_in x0 ) by A3, Th32, A1, Th34; ::_thesis: verum end; theorem :: NDIFF_4:37 for x0 being Real for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) proof let x0 be Real; ::_thesis: for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) let I be Function of REAL,(REAL-NS 1); ::_thesis: ( I = (proj (1,1)) " implies ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) ) assume A1: I = (proj (1,1)) " ; ::_thesis: ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) I . 1 = <*1*> by A1, PDIFF_1:1; then reconsider r = <*1*> as Point of (REAL-NS 1) ; A2: for x being Real st x in [#] REAL holds I /. x = (x * r) + (0. (REAL-NS 1)) proof let x be Real; ::_thesis: ( x in [#] REAL implies I /. x = (x * r) + (0. (REAL-NS 1)) ) assume x in [#] REAL ; ::_thesis: I /. x = (x * r) + (0. (REAL-NS 1)) I . 1 in REAL 1 by A1, FUNCT_1:3, PDIFF_1:2; then A3: <*1*> is Element of REAL 1 by A1, PDIFF_1:1; I /. x = <*(x * 1)*> by A1, PDIFF_1:1 .= x * <*1*> by RVSUM_1:47 ; hence I /. x = x * r by A3, REAL_NS1:3 .= (x * r) + (0. (REAL-NS 1)) by RLVECT_1:4 ; ::_thesis: verum end; A4: [#] REAL c= dom I by FUNCT_2:def_1; then A5: ( I is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds (I `| ([#] REAL)) . x = r ) ) by A2, NDIFF_3:21; r = (I `| ([#] REAL)) . x0 by A4, A2, NDIFF_3:21 .= diff (I,x0) by A5, NDIFF_3:def_6 ; hence ( I is_differentiable_in x0 & diff (I,x0) = <*1*> ) by A5, NDIFF_3:10; ::_thesis: verum end; definition let n be non empty Element of NAT ; let f be PartFunc of (REAL-NS n),REAL; let x be Point of (REAL-NS n); predf is_differentiable_in x means :Def6: :: NDIFF_4:def 6 ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & g is_differentiable_in y ); end; :: deftheorem Def6 defines is_differentiable_in NDIFF_4:def_6_:_ for n being non empty Element of NAT for f being PartFunc of (REAL-NS n),REAL for x being Point of (REAL-NS n) holds ( f is_differentiable_in x iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & g is_differentiable_in y ) ); definition let n be non empty Element of NAT ; let f be PartFunc of (REAL-NS n),REAL; let x be Point of (REAL-NS n); func diff (f,x) -> Function of (REAL-NS n),REAL means :Def7: :: NDIFF_4:def 7 ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & it = diff (g,y) ); existence ex b1 being Function of (REAL-NS n),REAL ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & b1 = diff (g,y) ) proof reconsider g = f as PartFunc of (REAL n),REAL by REAL_NS1:def_4; reconsider y = x as Element of REAL n by REAL_NS1:def_4; REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4; then diff (g,y) is Function of (REAL-NS n),REAL ; hence ex b1 being Function of (REAL-NS n),REAL ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & b1 = diff (g,y) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (REAL-NS n),REAL st ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & b2 = diff (g,y) ) holds b1 = b2 ; end; :: deftheorem Def7 defines diff NDIFF_4:def_7_:_ for n being non empty Element of NAT for f being PartFunc of (REAL-NS n),REAL for x being Point of (REAL-NS n) for b4 being Function of (REAL-NS n),REAL holds ( b4 = diff (f,x) iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st ( f = g & x = y & b4 = diff (g,y) ) ); theorem Th38: :: NDIFF_4:38 for J being Function of (REAL 1),REAL for x0 being Element of REAL 1 st J = proj (1,1) holds ( J is_differentiable_in x0 & diff (J,x0) = J ) proof let J be Function of (REAL 1),REAL; ::_thesis: for x0 being Element of REAL 1 st J = proj (1,1) holds ( J is_differentiable_in x0 & diff (J,x0) = J ) let x0 be Element of REAL 1; ::_thesis: ( J = proj (1,1) implies ( J is_differentiable_in x0 & diff (J,x0) = J ) ) assume A1: J = proj (1,1) ; ::_thesis: ( J is_differentiable_in x0 & diff (J,x0) = J ) A2: 1 in Seg 1 ; set R = (REAL 1) --> (0* 1); set L = <>* J; rng J = dom ((proj (1,1)) ") by A1, A2, PDIFF_1:1, PDIFF_1:2; then A3: dom (<>* J) = dom J by RELAT_1:27 .= REAL 1 by A1, A2, PDIFF_1:1 ; reconsider L = <>* J as Function of (REAL 1),(REAL 1) by PDIFF_1:2; set f = <>* J; A4: L = id (dom J) by A1, FUNCT_1:39 .= id (REAL 1) by A1, A2, PDIFF_1:1 ; A5: for x, y being Element of REAL 1 holds L . (x + y) = (L . x) + (L . y) proof let x, y be Element of REAL 1; ::_thesis: L . (x + y) = (L . x) + (L . y) thus L . (x + y) = x + y by A4, FUNCT_1:18 .= (L . x) + y by A4, FUNCT_1:18 .= (L . x) + (L . y) by A4, FUNCT_1:18 ; ::_thesis: verum end; A6: for x being Element of REAL 1 for r being Real holds L . (r * x) = r * (L . x) proof let x be Element of REAL 1; ::_thesis: for r being Real holds L . (r * x) = r * (L . x) let r be Real; ::_thesis: L . (r * x) = r * (L . x) thus L . (r * x) = r * x by A4, FUNCT_1:18 .= r * (L . x) by A4, FUNCT_1:18 ; ::_thesis: verum end; then A7: L is LinearOperator of 1,1 by A5, PDIFF_6:def_1, PDIFF_6:def_2; reconsider r0 = 1 as Real ; A8: { y where y is Element of REAL 1 : |.(y - x0).| < r0 } c= dom (<>* J) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Element of REAL 1 : |.(y - x0).| < r0 } or x in dom (<>* J) ) assume x in { y where y is Element of REAL 1 : |.(y - x0).| < r0 } ; ::_thesis: x in dom (<>* J) then ex y being Element of REAL 1 st ( x = y & |.(y - x0).| < r0 ) ; hence x in dom (<>* J) by A3; ::_thesis: verum end; A9: for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds (|.z.| ") * |.w.| < r ) ) proof let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds (|.z.| ") * |.w.| < r ) ) ) assume A10: r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds (|.z.| ") * |.w.| < r ) ) take d = r; ::_thesis: ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds (|.z.| ") * |.w.| < r ) ) thus 0 < d by A10; ::_thesis: for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds (|.z.| ") * |.w.| < r let z, w be Element of REAL 1; ::_thesis: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z implies (|.z.| ") * |.w.| < r ) assume A11: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z ) ; ::_thesis: (|.z.| ") * |.w.| < r w = 0* 1 by A11, FUNCOP_1:7; then |.w.| = 0 by EUCLID:7; hence (|.z.| ") * |.w.| < r by A10; ::_thesis: verum end; A12: for x being Element of REAL 1 st |.(x - x0).| < r0 holds ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) proof let x be Element of REAL 1; ::_thesis: ( |.(x - x0).| < r0 implies ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) ) assume |.(x - x0).| < r0 ; ::_thesis: ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) A13: (<>* J) /. x0 = L . x0 by A3, PARTFUN1:def_6; A14: - 1 is Real by XREAL_0:def_1; thus ((<>* J) /. x) - ((<>* J) /. x0) = (L . x) - (L . x0) by A13, A3, PARTFUN1:def_6 .= (L . x) + (L . ((- 1) * x0)) by A14, A6 .= L . (x - x0) by A5 .= (L . (x - x0)) + (0* 1) by RVSUM_1:16 .= (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) by FUNCOP_1:7 ; ::_thesis: verum end; then ( <>* J is_differentiable_in x0 & diff ((<>* J),x0) = L ) by A7, A8, A9, PDIFF_6:24; hence J is_differentiable_in x0 by PDIFF_7:def_1; ::_thesis: diff (J,x0) = J A15: rng J c= REAL ; thus diff (J,x0) = (proj (1,1)) * L by A12, A7, A8, A9, PDIFF_6:24 .= ((proj (1,1)) * ((proj (1,1)) ")) * J by RELAT_1:36 .= (id (rng (proj (1,1)))) * J by FUNCT_1:39 .= (id REAL) * J by A2, PDIFF_1:1 .= J by A15, RELAT_1:53 ; ::_thesis: verum end; theorem :: NDIFF_4:39 for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds ( J is_differentiable_in x0 & diff (J,x0) = J ) proof let J be Function of (REAL-NS 1),REAL; ::_thesis: for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds ( J is_differentiable_in x0 & diff (J,x0) = J ) let x0 be Point of (REAL-NS 1); ::_thesis: ( J = proj (1,1) implies ( J is_differentiable_in x0 & diff (J,x0) = J ) ) assume A1: J = proj (1,1) ; ::_thesis: ( J is_differentiable_in x0 & diff (J,x0) = J ) reconsider J0 = J as Function of (REAL 1),REAL by Lm1; reconsider y0 = x0 as Element of REAL 1 by REAL_NS1:def_4; ( J0 is_differentiable_in y0 & diff (J0,y0) = J ) by A1, Th38; hence J is_differentiable_in x0 by Def6; ::_thesis: diff (J,x0) = J ex g being PartFunc of (REAL 1),REAL ex y being Element of REAL 1 st ( J = g & x0 = y & diff (J,x0) = diff (g,y) ) by Def7; hence diff (J,x0) = J by A1, Th38; ::_thesis: verum end; theorem Th40: :: NDIFF_4:40 for n being non empty Element of NAT for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) ) proof let n be non empty Element of NAT ; ::_thesis: for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) ) let I be Function of REAL,(REAL-NS 1); ::_thesis: ( I = (proj (1,1)) " implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) ) ) assume A1: I = (proj (1,1)) " ; ::_thesis: ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) ) thus for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ::_thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) proof let R be RestFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: R * I is RestFunc of (REAL-NS n) A2: R is total by NDIFF_1:def_5; reconsider R0 = R as Function of (REAL 1),(REAL n) by A2, Lm1, REAL_NS1:def_4; reconsider R1 = R * I as PartFunc of REAL,(REAL-NS n) ; A3: R0 * I is Function of REAL,(REAL n) by Lm1; then A4: dom R1 = REAL by FUNCT_2:def_1; A5: for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds (|.z1.| ") * ||.(R1 /. z1).|| < r ) ) proof let r be Real; ::_thesis: ( r > 0 implies ex d being Real st ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds (|.z1.| ") * ||.(R1 /. z1).|| < r ) ) ) assume r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds (|.z1.| ") * ||.(R1 /. z1).|| < r ) ) then consider d being Real such that A6: d > 0 and A7: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r by A2, NDIFF_1:23; take d ; ::_thesis: ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds (|.z1.| ") * ||.(R1 /. z1).|| < r ) ) for z1 being Real st z1 <> 0 & |.z1.| < d holds (|.z1.| ") * ||.(R1 /. z1).|| < r proof let z1 be Real; ::_thesis: ( z1 <> 0 & |.z1.| < d implies (|.z1.| ") * ||.(R1 /. z1).|| < r ) assume that A8: z1 <> 0 and A9: abs z1 < d ; ::_thesis: (|.z1.| ") * ||.(R1 /. z1).|| < r reconsider z = I . z1 as Point of (REAL-NS 1) ; z1 in REAL ; then reconsider z1r = z1 as R_eal by NUMBERS:31; 0 < |.z1r.| by A8, EXTREAL2:4; then abs z1 > 0 by EXTREAL2:1; then ||.z.|| <> 0 by A1, Lm1, PDIFF_1:3; then A10: z <> 0. (REAL-NS 1) ; A11: dom I = REAL by FUNCT_2:def_1; R is total by NDIFF_1:def_5; then dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2; then R /. z = R . (I . z1) by PARTFUN1:def_6; then R /. z = R1 . z1 by A11, FUNCT_1:13; then A12: ||.(R /. z).|| = ||.(R1 /. z1).|| by A4, PARTFUN1:def_6; A13: ||.z.|| " = (abs z1) " by A1, Lm1, PDIFF_1:3; ||.z.|| < d by A1, A9, Lm1, PDIFF_1:3; hence (|.z1.| ") * ||.(R1 /. z1).|| < r by A7, A10, A13, A12; ::_thesis: verum end; hence ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds (|.z1.| ") * ||.(R1 /. z1).|| < r ) ) by A6; ::_thesis: verum end; for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) ) proof let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) ) A14: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_n0_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n0_<=_m_holds_ ||.((((h_")_(#)_(R1_/*_h))_._m)_-_(0._(REAL-NS_n))).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r ) A15: lim h = 0 ; assume r > 0 ; ::_thesis: ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r then consider d being Real such that A16: d > 0 and A17: for z1 being Real st z1 <> 0 & |.z1.| < d holds (|.z1.| ") * ||.(R1 /. z1).|| < r by A5; reconsider d1 = d as real number ; consider n0 being Element of NAT such that A18: for m being Element of NAT st n0 <= m holds abs ((h . m) - 0) < d1 by A16, A15, SEQ_2:def_7; take n0 = n0; ::_thesis: for m being Element of NAT st n0 <= m holds ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r hereby ::_thesis: verum let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r ) A19: h . m <> 0 by SEQ_1:5; rng h c= dom R1 by A4; then A20: ((abs (h . m)) ") * ||.(R1 /. (h . m)).|| = ((abs (h . m)) ") * ||.((R1 /* h) . m).|| by FUNCT_2:109 .= (((abs h) . m) ") * ||.((R1 /* h) . m).|| by SEQ_1:12 .= (((abs h) ") . m) * ||.((R1 /* h) . m).|| by VALUED_1:10 .= ((abs (h ")) . m) * ||.((R1 /* h) . m).|| by SEQ_1:54 .= (abs ((h ") . m)) * ||.((R1 /* h) . m).|| by SEQ_1:12 .= ||.(((h ") . m) * ((R1 /* h) . m)).|| by NORMSP_1:def_1 .= ||.(((h ") (#) (R1 /* h)) . m).|| by NDIFF_1:def_2 .= ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| by RLVECT_1:13 ; assume n0 <= m ; ::_thesis: ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r then abs ((h . m) - 0) < d by A18; hence ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r by A17, A19, A20; ::_thesis: verum end; end; hence (h ") (#) (R1 /* h) is convergent by NORMSP_1:def_6; ::_thesis: lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) hence lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) by A14, NORMSP_1:def_7; ::_thesis: verum end; hence R * I is RestFunc of (REAL-NS n) by A3, NDIFF_3:def_1; ::_thesis: verum end; let L be LinearOperator of (REAL-NS 1),(REAL-NS n); ::_thesis: L * I is LinearFunc of (REAL-NS n) reconsider L0 = L as Function of (REAL 1),(REAL n) by Lm1, REAL_NS1:def_4; reconsider L1 = L0 * I as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; reconsider r = L1 . 1 as Point of (REAL-NS n) by FUNCT_2:5; A21: dom (L0 * I) = REAL by Lm1, FUNCT_2:def_1; for p being Real holds L1 . p = p * r proof reconsider 1p = I . 1 as VECTOR of (REAL-NS 1) ; let p be Real; ::_thesis: L1 . p = p * r dom I = REAL by FUNCT_2:def_1; then L1 . p = L . (I . (p * 1)) by FUNCT_1:13; then L1 . p = L . (p * 1p) by A1, Lm1, PDIFF_1:3; then L1 . p = p * (L . 1p) by LOPBAN_1:def_5; hence L1 . p = p * r by A21, FUNCT_1:12; ::_thesis: verum end; hence L * I is LinearFunc of (REAL-NS n) by NDIFF_3:def_2; ::_thesis: verum end; theorem Th41: :: NDIFF_4:41 for n being non empty Element of NAT for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds ( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) ) proof let n be non empty Element of NAT ; ::_thesis: for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds ( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) ) let J be Function of (REAL-NS 1),REAL; ::_thesis: ( J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) ) ) assume A1: J = proj (1,1) ; ::_thesis: ( ( for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ) & ( for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) ) ) thus for R being RestFunc of (REAL-NS n) holds R * J is RestFunc of (REAL-NS 1),(REAL-NS n) ::_thesis: for L being LinearFunc of (REAL-NS n) holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) proof let R be RestFunc of (REAL-NS n); ::_thesis: R * J is RestFunc of (REAL-NS 1),(REAL-NS n) A2: R is total by NDIFF_3:def_1; reconsider R0 = R as Function of REAL,(REAL n) by A2, REAL_NS1:def_4; reconsider R1 = R0 * J as PartFunc of (REAL-NS 1),(REAL-NS n) by REAL_NS1:def_4; for h being non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1) holds ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS n) ) proof let h be non-zero 0. (REAL-NS 1) -convergent sequence of (REAL-NS 1); ::_thesis: ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS n) ) A3: lim h = 0. (REAL-NS 1) by NDIFF_1:def_4; deffunc H1( Element of NAT ) -> Element of REAL = J . (h . \$1); consider s being Real_Sequence such that A4: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1(); A5: h is convergent by NDIFF_1:def_4; A6: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ abs_((s_._n)_-_0)_<_p let p be real number ; ::_thesis: ( 0 < p implies ex m being Element of NAT st for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p ) A7: p is Real by XREAL_0:def_1; assume 0 < p ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p then consider m being Element of NAT such that A8: for n being Element of NAT st m <= n holds ||.((h . n) - (0. (REAL-NS 1))).|| < p by A5, A3, A7, NORMSP_1:def_7; take m = m; ::_thesis: for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_ abs_((s_._n)_-_0)_<_p let n be Element of NAT ; ::_thesis: ( m <= n implies abs ((s . n) - 0) < p ) assume m <= n ; ::_thesis: abs ((s . n) - 0) < p then ||.((h . n) - (0. (REAL-NS 1))).|| < p by A8; then A9: ||.(h . n).|| < p by RLVECT_1:13; s . n = J . (h . n) by A4; hence abs ((s . n) - 0) < p by A1, A9, PDIFF_1:4; ::_thesis: verum end; hence for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p ; ::_thesis: verum end; then A10: s is convergent by SEQ_2:def_6; then A11: lim s = 0 by A6, SEQ_2:def_7; now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ s_._x_<>_0 let x be set ; ::_thesis: ( x in NAT implies s . x <> 0 ) assume x in NAT ; ::_thesis: s . x <> 0 then reconsider n = x as Element of NAT ; A12: 0 <= abs (s . n) by COMPLEX1:46; h . n <> 0. (REAL-NS 1) by NDIFF_1:6; then A13: ||.(h . n).|| <> 0 by NORMSP_0:def_5; s . n = J . (h . n) by A4; then abs (s . n) <> 0 by A1, A13, PDIFF_1:4; hence s . x <> 0 by A12, COMPLEX1:47; ::_thesis: verum end; then s is non-zero by SEQ_1:4; then reconsider s = s as non-zero 0 -convergent Real_Sequence by A10, A11, FDIFF_1:def_1; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((||.h.||_")_(#)_(R1_/*_h)).||_._n_=_||.((s_")_(#)_(R_/*_s)).||_._n reconsider f1 = R1 as Function ; let n be Element of NAT ; ::_thesis: ||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.((s ") (#) (R /* s)).|| . n A14: rng h c= the carrier of (REAL-NS 1) ; (R /* s) . n = R . (s . n) by A2, FUNCT_2:115; then A15: (R /* s) . n = R . (J . (h . n)) by A4; NAT = dom h by FUNCT_2:def_1; then A16: R1 . (h . n) = (f1 * h) . n by FUNCT_1:13; rng h c= dom R1 by A14, FUNCT_2:def_1; then A17: R1 . (h . n) = (R1 /* h) . n by A16, FUNCT_2:def_11; A18: s . n = J . (h . n) by A4; ||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| by NORMSP_0:def_4 .= ||.(((||.h.|| ") . n) * ((R1 /* h) . n)).|| by NDIFF_1:def_2 .= (abs ((||.h.|| ") . n)) * ||.((R1 /* h) . n).|| by NORMSP_1:def_1 .= (abs ((||.h.|| . n) ")) * ||.((R1 /* h) . n).|| by VALUED_1:10 .= (abs (||.(h . n).|| ")) * ||.((R1 /* h) . n).|| by NORMSP_0:def_4 .= (||.(h . n).|| ") * ||.((R1 /* h) . n).|| by ABSVALUE:def_1 .= ((abs (s . n)) ") * ||.((R1 /* h) . n).|| by A1, A18, PDIFF_1:4 .= ((abs (s . n)) ") * ||.((R /* s) . n).|| by A17, A15, FUNCT_2:15 .= (((abs s) . n) ") * ||.((R /* s) . n).|| by SEQ_1:12 .= (((abs s) ") . n) * ||.((R /* s) . n).|| by VALUED_1:10 .= ((abs (s ")) . n) * ||.((R /* s) . n).|| by SEQ_1:54 .= (abs ((s ") . n)) * ||.((R /* s) . n).|| by SEQ_1:12 .= ||.(((s ") . n) * ((R /* s) . n)).|| by NORMSP_1:def_1 .= ||.(((s ") (#) (R /* s)) . n).|| by NDIFF_1:def_2 .= ||.((s ") (#) (R /* s)).|| . n by NORMSP_0:def_4 ; hence ||.((||.h.|| ") (#) (R1 /* h)).|| . n = ||.((s ") (#) (R /* s)).|| . n ; ::_thesis: verum end; then A19: ||.((||.h.|| ") (#) (R1 /* h)).|| = ||.((s ") (#) (R /* s)).|| by FUNCT_2:63; A20: lim ((s ") (#) (R /* s)) = 0. (REAL-NS n) by NDIFF_3:def_1; A21: (s ") (#) (R /* s) is convergent by NDIFF_3:def_1; A22: lim ||.((s ") (#) (R /* s)).|| = ||.(0. (REAL-NS n)).|| by A20, A21, LOPBAN_1:20 .= 0 ; A23: ||.((s ") (#) (R /* s)).|| is convergent by A21, NORMSP_1:23; A24: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n0_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n0_<=_m_holds_ ||.((((||.h.||_")_(#)_(R1_/*_h))_._m)_-_(0._(REAL-NS_n))).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p ) assume 0 < p ; ::_thesis: ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p then consider n0 being Element of NAT such that A25: for m being Element of NAT st n0 <= m holds abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . m) - 0) < p by A19, A23, A22, SEQ_2:def_7; take n0 = n0; ::_thesis: for m being Element of NAT st n0 <= m holds ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p hereby ::_thesis: verum let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p ) assume n0 <= m ; ::_thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p then abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . m) - 0) < p by A25; then A26: abs ||.(((||.h.|| ") (#) (R1 /* h)) . m).|| < p by NORMSP_0:def_4; ||.(((||.h.|| ") (#) (R1 /* h)) . m).|| < p by A26, ABSVALUE:def_1; hence ||.((((||.h.|| ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < p by RLVECT_1:13; ::_thesis: verum end; end; then (||.h.|| ") (#) (R1 /* h) is convergent by NORMSP_1:def_6; hence ( (||.h.|| ") (#) (R1 /* h) is convergent & lim ((||.h.|| ") (#) (R1 /* h)) = 0. (REAL-NS n) ) by A24, NORMSP_1:def_7; ::_thesis: verum end; hence R * J is RestFunc of (REAL-NS 1),(REAL-NS n) by NDIFF_1:def_5; ::_thesis: verum end; let L be LinearFunc of (REAL-NS n); ::_thesis: L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) consider r being Point of (REAL-NS n) such that A27: for p being Real holds L . p = p * r by NDIFF_3:def_2; reconsider L0 = L as Function of REAL,(REAL n) by REAL_NS1:def_4; set K = ||.r.||; reconsider L1 = L * J as Function of (REAL-NS 1),(REAL-NS n) ; A28: dom L1 = REAL 1 by Lm1, FUNCT_2:def_1; A29: now__::_thesis:_for_x,_y_being_Point_of_(REAL-NS_1)_holds_L1_._(x_+_y)_=_(L1_._x)_+_(L1_._y) let x, y be Point of (REAL-NS 1); ::_thesis: L1 . (x + y) = (L1 . x) + (L1 . y) L1 . (x + y) = L . (J . (x + y)) by Lm1, A28, FUNCT_1:12; then L1 . (x + y) = L . ((J . x) + (J . y)) by A1, PDIFF_1:4; then L1 . (x + y) = ((J . x) + (J . y)) * r by A27; then L1 . (x + y) = ((J . x) * r) + ((J . y) * r) by RLVECT_1:def_6; then L1 . (x + y) = (L . (J . x)) + ((J . y) * r) by A27; then A30: L1 . (x + y) = (L . (J . x)) + (L . (J . y)) by A27; L . (J . x) = L1 . x by Lm1, A28, FUNCT_1:12; hence L1 . (x + y) = (L1 . x) + (L1 . y) by Lm1, A28, A30, FUNCT_1:12; ::_thesis: verum end; now__::_thesis:_for_x_being_Point_of_(REAL-NS_1) for_a_being_Real_holds_L1_._(a_*_x)_=_a_*_(L1_._x) let x be Point of (REAL-NS 1); ::_thesis: for a being Real holds L1 . (a * x) = a * (L1 . x) let a be Real; ::_thesis: L1 . (a * x) = a * (L1 . x) L1 . (a * x) = L . (J . (a * x)) by Lm1, A28, FUNCT_1:12; then L1 . (a * x) = L . (a * (J . x)) by A1, PDIFF_1:4; then L1 . (a * x) = (a * (J . x)) * r by A27; then A31: L1 . (a * x) = a * ((J . x) * r) by RLVECT_1:def_7; L . (J . x) = L1 . x by Lm1, A28, FUNCT_1:12; hence L1 . (a * x) = a * (L1 . x) by A31, A27; ::_thesis: verum end; then reconsider L1 = L1 as LinearOperator of (REAL-NS 1),(REAL-NS n) by A29, VECTSP_1:def_20, LOPBAN_1:def_5; now__::_thesis:_for_x_being_Point_of_(REAL-NS_1)_holds_||.(L1_._x).||_<=_||.r.||_*_||.x.|| let x be Point of (REAL-NS 1); ::_thesis: ||.(L1 . x).|| <= ||.r.|| * ||.x.|| ||.(L1 . x).|| = ||.(L . (J . x)).|| by Lm1, A28, FUNCT_1:12; then ||.(L1 . x).|| = ||.((J . x) * r).|| by A27; then ||.(L1 . x).|| = ||.r.|| * |.(J . x).| by NORMSP_1:def_1; hence ||.(L1 . x).|| <= ||.r.|| * ||.x.|| by A1, PDIFF_1:4; ::_thesis: verum end; hence L * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def_8; ::_thesis: verum end; theorem Th42: :: NDIFF_4:42 for n being non empty Element of NAT for I being Function of REAL,(REAL-NS 1) for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) proof let n be non empty Element of NAT ; ::_thesis: for I being Function of REAL,(REAL-NS 1) for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let I be Function of REAL,(REAL-NS 1); ::_thesis: for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let x0 be Point of (REAL-NS 1); ::_thesis: for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let y0 be Element of REAL ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 implies ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) ) assume that A1: I = (proj (1,1)) " and A2: x0 in dom f and A3: y0 in dom g and A4: x0 = <*y0*> and A5: f * I = g ; ::_thesis: ( not f is_differentiable_in x0 or ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) ) reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1; assume A6: f is_differentiable_in x0 ; ::_thesis: ( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) then consider NN being Neighbourhood of x0 such that A7: NN c= dom f and A8: ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ex R being RestFunc of (REAL-NS 1),(REAL-NS n) st for x being Point of (REAL-NS 1) st x in NN holds (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by NDIFF_1:def_6; A9: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39; A10: g * J = f * (id (REAL-NS 1)) by A9, A5, RELAT_1:36 .= f by FUNCT_2:17 ; consider e being Real such that A11: 0 < e and A12: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= NN by NFCONT_1:def_1; consider L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))), R being RestFunc of (REAL-NS 1),(REAL-NS n) such that A13: for x9 being Point of (REAL-NS 1) st x9 in NN holds (f /. x9) - (f /. x0) = (L . (x9 - x0)) + (R /. (x9 - x0)) by A8; reconsider R0 = R * I as RestFunc of (REAL-NS n) by A1, Th40; L is LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def_9; then reconsider L0 = L * I as LinearFunc of (REAL-NS n) by A1, Th40; set N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; A14: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= the carrier of (REAL-NS 1) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } or y in the carrier of (REAL-NS 1) ) assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; ::_thesis: y in the carrier of (REAL-NS 1) then ex z being Point of (REAL-NS 1) st ( y = z & ||.(z - x0).|| < e ) ; hence y in the carrier of (REAL-NS 1) ; ::_thesis: verum end; then reconsider N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } as Neighbourhood of x0 by A11, NFCONT_1:def_1; set N0 = { z where z is Element of REAL : abs (z - y0) < e } ; A15: N c= dom f by A7, A12, XBOOLE_1:1; now__::_thesis:_for_z_being_set_holds_ (_(_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y0)_<_e__}__implies_z_in_J_.:_N_)_&_(_z_in_J_.:_N_implies_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y0)_<_e__}__)_) let z be set ; ::_thesis: ( ( z in { z where z is Element of REAL : abs (z - y0) < e } implies z in J .: N ) & ( z in J .: N implies z in { z where z is Element of REAL : abs (z - y0) < e } ) ) hereby ::_thesis: ( z in J .: N implies z in { z where z is Element of REAL : abs (z - y0) < e } ) assume z in { z where z is Element of REAL : abs (z - y0) < e } ; ::_thesis: z in J .: N then consider y9 being Element of REAL such that A16: z = y9 and A17: abs (y9 - y0) < e ; reconsider w = I . y9 as Point of (REAL-NS 1) ; x0 = I . y0 by A1, A4, Lm2; then w - x0 = I . (y9 - y0) by A1, Lm1, PDIFF_1:3; then ||.(w - x0).|| = abs (y9 - y0) by A1, Lm1, PDIFF_1:3; then A18: w in { z0 where z0 is Point of (REAL-NS 1) : ||.(z0 - x0).|| < e } by A17; J . (I . y9) = y9 by A1, Lm2, FUNCT_1:35; hence z in J .: N by A18, A16, FUNCT_2:35; ::_thesis: verum end; assume z in J .: N ; ::_thesis: z in { z where z is Element of REAL : abs (z - y0) < e } then consider ww being set such that ww in REAL 1 and A19: ww in N and A20: z = J . ww by FUNCT_2:64; consider w being Point of (REAL-NS 1) such that A21: ww = w and A22: ||.(w - x0).|| < e by A19; reconsider y9 = J . w as Element of REAL ; J . x0 = y0 by A4, Lm2; then J . (w - x0) = y9 - y0 by PDIFF_1:4; then abs (y9 - y0) < e by A22, PDIFF_1:4; hence z in { z where z is Element of REAL : abs (z - y0) < e } by A20, A21; ::_thesis: verum end; then A23: { z where z is Element of REAL : abs (z - y0) < e } = J .: N by TARSKI:1; J .: (dom f) = J .: (J " (dom g)) by A10, RELAT_1:147; then A24: J .: (dom f) = dom (f * I) by A5, Lm2, FUNCT_1:77; A25: I * J = id (REAL 1) by A1, Lm2, FUNCT_1:39; N c= dom f by A7, A12, XBOOLE_1:1; then A26: { z where z is Element of REAL : abs (z - y0) < e } c= dom (f * I) by A24, A23, RELAT_1:123; A27: ].(y0 - e),(y0 + e).[ c= { z where z is Element of REAL : abs (z - y0) < e } proof now__::_thesis:_for_d_being_set_st_d_in_].(y0_-_e),(y0_+_e).[_holds_ d_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y0)_<_e__}_ let d be set ; ::_thesis: ( d in ].(y0 - e),(y0 + e).[ implies d in { z where z is Element of REAL : abs (z - y0) < e } ) assume A28: d in ].(y0 - e),(y0 + e).[ ; ::_thesis: d in { z where z is Element of REAL : abs (z - y0) < e } reconsider y1 = d as Element of REAL by A28; abs (y1 - y0) < e by A28, RCOMP_1:1; hence d in { z where z is Element of REAL : abs (z - y0) < e } ; ::_thesis: verum end; hence ].(y0 - e),(y0 + e).[ c= { z where z is Element of REAL : abs (z - y0) < e } by TARSKI:def_3; ::_thesis: verum end; { z where z is Element of REAL : abs (z - y0) < e } c= ].(y0 - e),(y0 + e).[ proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in { z where z is Element of REAL : abs (z - y0) < e } or d in ].(y0 - e),(y0 + e).[ ) assume d in { z where z is Element of REAL : abs (z - y0) < e } ; ::_thesis: d in ].(y0 - e),(y0 + e).[ then ex r being Element of REAL st ( d = r & abs (r - y0) < e ) ; hence d in ].(y0 - e),(y0 + e).[ by RCOMP_1:1; ::_thesis: verum end; then { z where z is Element of REAL : abs (z - y0) < e } = ].(y0 - e),(y0 + e).[ by A27, XBOOLE_0:def_10; then A29: { z where z is Element of REAL : abs (z - y0) < e } is Neighbourhood of y0 by A11, RCOMP_1:def_6; N c= REAL 1 by A14, REAL_NS1:def_4; then (I * J) .: N = N by A25, FRECHET:13; then A30: I .: { z where z is Element of REAL : abs (z - y0) < e } = N by A23, RELAT_1:126; A31: for y1 being Real st y1 in { z where z is Element of REAL : abs (z - y0) < e } holds ((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0)) proof let y1 be Real; ::_thesis: ( y1 in { z where z is Element of REAL : abs (z - y0) < e } implies ((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0)) ) reconsider y9 = I . y1 as Point of (REAL-NS 1) ; R is total by NDIFF_1:def_5; then A32: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2; R0 is total by NDIFF_3:def_1; then A33: dom (R * I) = REAL by PARTFUN1:def_2; R /. (I . (y1 - y0)) = R . (I . (y1 - y0)) by A32, PARTFUN1:def_6; then R /. (I . (y1 - y0)) = R0 . (y1 - y0) by A33, FUNCT_1:12; then A34: R /. (I . (y1 - y0)) = R0 /. (y1 - y0) by A33, PARTFUN1:def_6; L0 is total ; then A35: dom (L * I) = REAL by PARTFUN1:def_2; assume A36: y1 in { z where z is Element of REAL : abs (z - y0) < e } ; ::_thesis: ((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0)) then A37: I . y1 in N by A30, FUNCT_2:35; then A38: f /. (I . y1) = f . (I . y1) by A15, PARTFUN1:def_6; f /. (I . y1) = (f * I) . y1 by A38, A26, A36, FUNCT_1:12; then A39: f /. (I . y1) = (f * I) /. y1 by A26, A36, PARTFUN1:def_6; A40: x0 = I . y0 by A4, A1, Lm2; then f /. (I . y0) = f . (I . y0) by A2, PARTFUN1:def_6; then f /. (I . y0) = (f * I) . y0 by A3, A5, FUNCT_1:12; then A41: f /. (I . y0) = (f * I) /. y0 by A3, A5, PARTFUN1:def_6; (f /. y9) - (f /. x0) = (L . (y9 - x0)) + (R /. (y9 - x0)) by A13, A12, A37; then A42: (f /. (I . y1)) - (f /. (I . y0)) = (L . (I . (y1 - y0))) + (R /. (y9 - x0)) by A1, A40, Lm1, PDIFF_1:3; L . (I . (y1 - y0)) = L0 . (y1 - y0) by A35, FUNCT_1:12; hence ((f * I) /. y1) - ((f * I) /. y0) = (L0 . (y1 - y0)) + (R0 /. (y1 - y0)) by A40, A42, A34, A39, A41, A1, Lm1, PDIFF_1:3; ::_thesis: verum end; then A43: f * I is_differentiable_in y0 by A29, A26, NDIFF_3:def_3; thus g is_differentiable_in y0 by A5, A31, A29, A26, NDIFF_3:def_3; ::_thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) A44: diff ((f * I),y0) = L0 . 1 by A31, A43, A29, A26, NDIFF_3:def_4; thus A45: diff (g,y0) = ((diff (f,x0)) * I) . 1 by A5, A44, A6, A13, A7, NDIFF_1:def_7 .= (diff (f,x0)) . (I . 1) by A1, FUNCT_1:13, PDIFF_1:2 .= (diff (f,x0)) . <*1*> by A1, Lm2 ; ::_thesis: for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) let r be Element of REAL ; ::_thesis: (diff (f,x0)) . <*r*> = r * (diff (g,y0)) A46: <*1*> is Element of REAL 1 by FINSEQ_2:98; then reconsider x = <*1*> as Point of (REAL-NS 1) by REAL_NS1:def_4; A47: diff (f,x0) is LinearOperator of (REAL-NS 1),(REAL-NS n) by LOPBAN_1:def_9; thus (diff (f,x0)) . <*r*> = (diff (f,x0)) . <*(r * 1)*> .= (diff (f,x0)) . (r * <*1*>) by RVSUM_1:47 .= (diff (f,x0)) . (r * x) by A46, REAL_NS1:3 .= r * (diff (g,y0)) by A45, A47, LOPBAN_1:def_5 ; ::_thesis: verum end; theorem Th43: :: NDIFF_4:43 for n being non empty Element of NAT for I being Function of REAL,(REAL-NS 1) for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) proof let n be non empty Element of NAT ; ::_thesis: for I being Function of REAL,(REAL-NS 1) for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let I be Function of REAL,(REAL-NS 1); ::_thesis: for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let x0 be Point of (REAL-NS 1); ::_thesis: for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let y0 be Element of REAL ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g implies ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) ) assume that A1: I = (proj (1,1)) " and A2: x0 in dom f and A3: y0 in dom g and A4: x0 = <*y0*> and A5: f * I = g ; ::_thesis: ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1; thus ( f is_differentiable_in x0 implies g is_differentiable_in y0 ) by A2, A3, A4, A5, Th42, A1; ::_thesis: ( g is_differentiable_in y0 implies f is_differentiable_in x0 ) assume g is_differentiable_in y0 ; ::_thesis: f is_differentiable_in x0 then consider N0 being Neighbourhood of y0 such that A6: N0 c= dom (f * I) and A7: ex L being LinearFunc of (REAL-NS n) ex R being RestFunc of (REAL-NS n) st for y being Real st y in N0 holds ((f * I) /. y) - ((f * I) /. y0) = (L . (y - y0)) + (R /. (y - y0)) by A5, NDIFF_3:def_3; A8: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39; A9: g * J = f * (id (REAL-NS 1)) by A5, A8, RELAT_1:36 .= f by FUNCT_2:17 ; consider e0 being real number such that A10: 0 < e0 and A11: N0 = ].(y0 - e0),(y0 + e0).[ by RCOMP_1:def_6; reconsider e = e0 as Real by XREAL_0:def_1; set N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; consider L being LinearFunc of (REAL-NS n), R being RestFunc of (REAL-NS n) such that A12: for y1 being Real st y1 in N0 holds ((f * I) /. y1) - ((f * I) /. y0) = (L . (y1 - y0)) + (R /. (y1 - y0)) by A7; reconsider R0 = R * J as RestFunc of (REAL-NS 1),(REAL-NS n) by Th41; reconsider L0 = L * J as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS n) by Th41; now__::_thesis:_for_z_being_set_holds_ (_(_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x0).||_<_e__}__implies_z_in_I_.:_N0_)_&_(_z_in_I_.:_N0_implies_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x0).||_<_e__}__)_) let z be set ; ::_thesis: ( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ) ) hereby ::_thesis: ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ) assume z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; ::_thesis: z in I .: N0 then consider w being Point of (REAL-NS 1) such that A13: z = w and A14: ||.(w - x0).|| < e ; reconsider y2 = J . w as Element of REAL ; J . x0 = y0 by A4, Lm2; then J . (w - x0) = y2 - y0 by PDIFF_1:4; then abs (y2 - y0) < e by A14, PDIFF_1:4; then A15: y2 in N0 by A11, RCOMP_1:1; w in the carrier of (REAL-NS 1) ; then w in dom J by Lm2, REAL_NS1:def_4; then w = I . y2 by A1, FUNCT_1:34; hence z in I .: N0 by A13, A15, FUNCT_2:35; ::_thesis: verum end; assume z in I .: N0 ; ::_thesis: z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } then consider yy being set such that A16: yy in REAL and A17: yy in N0 and A18: z = I . yy by FUNCT_2:64; reconsider y3 = yy as Element of REAL by A16; set w = I . y3; I . y0 = x0 by A4, A1, Lm2; then A19: (I . y3) - x0 = I . (y3 - y0) by A1, Lm1, PDIFF_1:3; abs (y3 - y0) < e by A11, A17, RCOMP_1:1; then ||.((I . y3) - x0).|| < e by A19, A1, Lm1, PDIFF_1:3; hence z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } by A18; ::_thesis: verum end; then A20: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } = I .: N0 by TARSKI:1; I .: (dom g) = I .: (I " (dom f)) by A5, RELAT_1:147; then I .: (dom g) = dom f by A1, Lm1, FUNCT_1:77, PDIFF_1:2; then A21: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= dom f by A5, A6, A20, RELAT_1:123; { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= the carrier of (REAL-NS 1) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } or y in the carrier of (REAL-NS 1) ) assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; ::_thesis: y in the carrier of (REAL-NS 1) then ex z being Point of (REAL-NS 1) st ( y = z & ||.(z - x0).|| < e ) ; hence y in the carrier of (REAL-NS 1) ; ::_thesis: verum end; then A22: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } is Neighbourhood of x0 by A10, NFCONT_1:def_1; J * I = id REAL by A1, Lm2, FUNCT_1:39; then (J * I) .: N0 = N0 by FRECHET:13; then A23: J .: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } = N0 by A20, RELAT_1:126; A24: for y being Point of (REAL-NS 1) st y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } holds (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) proof x0 in the carrier of (REAL-NS 1) ; then x0 in dom J by Lm2, REAL_NS1:def_4; then g . (J . x0) = f . x0 by A9, FUNCT_1:13; then A25: g . (J . x0) = f /. x0 by A2, PARTFUN1:def_6; A26: J . x0 = y0 by A4, Lm2; let y be Point of (REAL-NS 1); ::_thesis: ( y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } implies (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) ) assume A27: y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; ::_thesis: (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) set y3 = J . y; reconsider p1 = g /. (J . y), p2 = g /. y0, q1 = L . ((J . y) - y0), q2 = R /. ((J . y) - y0) as VECTOR of (REAL-NS n) ; A28: J . x0 = y0 by A4, Lm2; (g /. (J . y)) - (g /. y0) = q1 + q2 by A5, A12, A23, A27, FUNCT_2:35; then (g /. (J . y)) - (g /. (J . x0)) = (L . (J . (y - x0))) + (R /. ((J . y) - y0)) by A28, PDIFF_1:4; then A29: (g /. (J . y)) - (g /. (J . x0)) = (L . (J . (y - x0))) + (R /. (J . (y - x0))) by A28, PDIFF_1:4; A30: dom L0 = the carrier of (REAL-NS 1) by FUNCT_2:def_1; y - x0 in the carrier of (REAL-NS 1) ; then y - x0 in dom J by Lm2, REAL_NS1:def_4; then A31: R . (J . (y - x0)) = (R * J) . (y - x0) by FUNCT_1:13; R0 is total by NDIFF_1:def_5; then A32: dom (R * J) = the carrier of (REAL-NS 1) by PARTFUN1:def_2; A33: R . (J . (y - x0)) = R0 /. (y - x0) by A31, A32, PARTFUN1:def_6; J . (y - x0) in dom R by A32, FUNCT_1:11; then A34: R /. (J . (y - x0)) = R0 /. (y - x0) by A33, PARTFUN1:def_6; y in the carrier of (REAL-NS 1) ; then A35: y in dom J by Lm2, REAL_NS1:def_4; g . (J . y) = f . y by A9, A35, FUNCT_1:13; then A36: g . (J . y) = f /. y by A21, A27, PARTFUN1:def_6; J . y in dom g by A21, A27, A9, FUNCT_1:11; then g /. (J . y) = f /. y by A36, PARTFUN1:def_6; then (g /. (J . y)) - (g /. (J . x0)) = (f /. y) - (f /. x0) by A3, A26, A25, PARTFUN1:def_6; hence (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) by A29, A34, A30, FUNCT_1:12; ::_thesis: verum end; L0 is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) by LOPBAN_1:def_9; hence f is_differentiable_in x0 by A22, A21, A24, NDIFF_1:def_6; ::_thesis: verum end; theorem Th44: :: NDIFF_4:44 for n being non empty Element of NAT for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) proof let n be non empty Element of NAT ; ::_thesis: for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let J be Function of (REAL-NS 1),REAL; ::_thesis: for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let x0 be Point of (REAL-NS 1); ::_thesis: for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let y0 be Element of REAL ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J implies ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) ) assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J ) ; ::_thesis: ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def_4; A2: J * I = id REAL by A1, Lm2, FUNCT_1:39; f * I = g * (id REAL) by A1, A2, RELAT_1:36 .= g by FUNCT_2:17 ; hence ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) by A1, Th43; ::_thesis: verum end; theorem :: NDIFF_4:45 for n being non empty Element of NAT for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) proof let n be non empty Element of NAT ; ::_thesis: for J being Function of (REAL-NS 1),REAL for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let J be Function of (REAL-NS 1),REAL; ::_thesis: for x0 being Point of (REAL-NS 1) for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let x0 be Point of (REAL-NS 1); ::_thesis: for y0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let y0 be Element of REAL ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of (REAL-NS 1),(REAL-NS n) st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 holds ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) let f be PartFunc of (REAL-NS 1),(REAL-NS n); ::_thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 implies ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) ) assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J & g is_differentiable_in y0 ) ; ::_thesis: ( f is_differentiable_in x0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) hence A2: f is_differentiable_in x0 by Th44; ::_thesis: ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def_4; A3: J * I = id REAL by A1, Lm2, FUNCT_1:39; f * I = g * (id REAL) by A1, A3, RELAT_1:36 .= g by FUNCT_2:17 ; hence ( diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) ) by A1, Th42, A2; ::_thesis: verum end; theorem Th46: :: NDIFF_4:46 for n being non empty Element of NAT for R being RestFunc of (REAL-NS n) st R /. 0 = 0. (REAL-NS n) holds for e being Real st e > 0 holds ex d being Real st ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) proof let n be non empty Element of NAT ; ::_thesis: for R being RestFunc of (REAL-NS n) st R /. 0 = 0. (REAL-NS n) holds for e being Real st e > 0 holds ex d being Real st ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) let R be RestFunc of (REAL-NS n); ::_thesis: ( R /. 0 = 0. (REAL-NS n) implies for e being Real st e > 0 holds ex d being Real st ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) ) assume A1: R /. 0 = 0. (REAL-NS n) ; ::_thesis: for e being Real st e > 0 holds ex d being Real st ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) let e be Real; ::_thesis: ( e > 0 implies ex d being Real st ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) ) assume A2: e > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) R is total by NDIFF_3:def_1; then consider d being Real such that A3: d > 0 and A4: for z being Real st z <> 0 & |.z.| < d holds (|.z.| ") * ||.(R /. z).|| < e by A2, Th23; take d ; ::_thesis: ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) now__::_thesis:_for_h_being_Real_st_|.h.|_<_d_holds_ ||.(R_/._h).||_<=_e_*_|.h.| let h be Real; ::_thesis: ( |.h.| < d implies ||.(R /. h).|| <= e * |.h.| ) assume A5: |.h.| < d ; ::_thesis: ||.(R /. h).|| <= e * |.h.| now__::_thesis:_(_(_h_<>_0_&_||.(R_/._h).||_<=_e_*_|.h.|_)_or_(_h_=_0_&_||.(R_/._h).||_<=_e_*_|.h.|_)_) percases ( h <> 0 or h = 0 ) ; caseA6: h <> 0 ; ::_thesis: ||.(R /. h).|| <= e * |.h.| then ( 0 <= |.h.| & (|.h.| ") * ||.(R /. h).|| <= e ) by A4, A5, COMPLEX1:46; then |.h.| * ((|.h.| ") * ||.(R /. h).||) <= |.h.| * e by XREAL_1:64; then A7: (|.h.| * (|.h.| ")) * ||.(R /. h).|| <= e * |.h.| ; |.h.| <> 0 by A6, COMPLEX1:45; then 1 * ||.(R /. h).|| <= e * |.h.| by A7, XCMPLX_0:def_7; hence ||.(R /. h).|| <= e * |.h.| ; ::_thesis: verum end; caseA8: h = 0 ; ::_thesis: ||.(R /. h).|| <= e * |.h.| reconsider p0 = 0 as Real ; 0 <= |.h.| by COMPLEX1:46; then p0 * |.h.| <= e * |.h.| by A2; hence ||.(R /. h).|| <= e * |.h.| by A1, A8; ::_thesis: verum end; end; end; hence ||.(R /. h).|| <= e * |.h.| ; ::_thesis: verum end; hence ( d > 0 & ( for h being Real st |.h.| < d holds ||.(R /. h).|| <= e * |.h.| ) ) by A3; ::_thesis: verum end; theorem Th47: :: NDIFF_4:47 for n, m being non empty Element of NAT for R being RestFunc of (REAL-NS n) for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m) proof let n, m be non empty Element of NAT ; ::_thesis: for R being RestFunc of (REAL-NS n) for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m) let R be RestFunc of (REAL-NS n); ::_thesis: for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m) let L be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); ::_thesis: L * R is RestFunc of (REAL-NS m) set S = REAL-NS n; set T = REAL-NS m; consider K being Real such that A1: 0 <= K and A2: for z being Point of (REAL-NS n) holds ||.(L . z).|| <= K * ||.z.|| by LOPBAN_1:def_8; dom L = the carrier of (REAL-NS n) by FUNCT_2:def_1; then A3: rng R c= dom L ; A4: R is total by NDIFF_3:def_1; then A5: dom R = REAL by PARTFUN1:def_2; reconsider p0 = 0 , p1 = 1 as Real ; A6: p0 + K < p1 + K by XREAL_1:8; now__::_thesis:_for_ee_being_Real_st_ee_>_0_holds_ ex_d_being_Real_st_ (_d_>_0_&_(_for_h_being_Real_st_h_<>_0_&_|.h.|_<_d_holds_ (|.h.|_")_*_||.((L_*_R)_/._h).||_<_ee_)_) let ee be Real; ::_thesis: ( ee > 0 implies ex d being Real st ( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds (|.h.| ") * ||.((L * R) /. h).|| < ee ) ) ) assume A7: ee > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds (|.h.| ") * ||.((L * R) /. h).|| < ee ) ) set e = ee / 2; ee / 2 > 0 by A7, XREAL_1:215; then A8: 0 / (1 + K) < (ee / 2) / (1 + K) by A1, XREAL_1:74; set e1 = (ee / 2) / (1 + K); consider d being Real such that A9: 0 < d and A10: for h being Real st h <> 0 & |.h.| < d holds (|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A4, A8, Th23; A11: ee / 2 < ee by A7, XREAL_1:216; now__::_thesis:_for_h_being_Real_st_h_<>_0_&_|.h.|_<_d_holds_ (|.h.|_")_*_||.((L_*_R)_/._h).||_<_ee let h be Real; ::_thesis: ( h <> 0 & |.h.| < d implies (|.h.| ") * ||.((L * R) /. h).|| < ee ) assume that A12: h <> 0 and A13: |.h.| < d ; ::_thesis: (|.h.| ") * ||.((L * R) /. h).|| < ee (|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A10, A12, A13; then (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K)) by A1, XREAL_1:64; then A14: (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= ee / 2 by A1, XCMPLX_1:87; |.h.| <> 0 by A12, COMPLEX1:45; then A15: |.h.| > 0 by COMPLEX1:46; A16: K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).|| by A6, XREAL_1:64; ||.(L . (R /. h)).|| <= K * ||.(R /. h).|| by A2; then ||.(L . (R /. h)).|| <= (K + 1) * ||.(R /. h).|| by A16, XXREAL_0:2; then (|.h.| ") * ||.(L . (R /. h)).|| <= (|.h.| ") * ((K + 1) * ||.(R /. h).||) by A15, XREAL_1:64; then A17: (|.h.| ") * ||.(L . (R /. h)).|| <= ee / 2 by A14, XXREAL_0:2; L . (R /. h) = L /. (R /. h) .= (L * R) /. h by A5, A3, PARTFUN2:5 ; hence (|.h.| ") * ||.((L * R) /. h).|| < ee by A11, A17, XXREAL_0:2; ::_thesis: verum end; hence ex d being Real st ( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds (|.h.| ") * ||.((L * R) /. h).|| < ee ) ) by A9; ::_thesis: verum end; hence L * R is RestFunc of (REAL-NS m) by A4, Th23; ::_thesis: verum end; theorem Th48: :: NDIFF_4:48 for n, m being non empty Element of NAT for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) proof let n, m be non empty Element of NAT ; ::_thesis: for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) set S = REAL-NS n; set T = REAL-NS m; let R1 be RestFunc of (REAL-NS n); ::_thesis: ( R1 /. 0 = 0. (REAL-NS n) implies for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) ) assume R1 /. 0 = 0. (REAL-NS n) ; ::_thesis: for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) then consider d0 being Real such that A1: 0 < d0 and A2: for h being Real st |.h.| < d0 holds ||.(R1 /. h).|| <= 1 * |.h.| by Th46; let R2 be RestFunc of (REAL-NS n),(REAL-NS m); ::_thesis: ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) implies for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) ) assume A3: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) ; ::_thesis: for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) let L be LinearFunc of (REAL-NS n); ::_thesis: R2 * (L + R1) is RestFunc of (REAL-NS m) consider r being Point of (REAL-NS n) such that A4: for h being Real holds L . h = h * r by NDIFF_3:def_2; set K = ||.r.||; R2 is total by NDIFF_1:def_5; then dom R2 = the carrier of (REAL-NS n) by PARTFUN1:def_2; then A5: rng (L + R1) c= dom R2 ; R1 is total by NDIFF_3:def_1; then A6: L + R1 is total by VFUNCT_1:32; then A7: dom (L + R1) = REAL by PARTFUN1:def_2; A8: now__::_thesis:_for_ee_being_Real_st_ee_>_0_holds_ ex_dd1_being_Real_st_ (_dd1_>_0_&_(_for_h_being_Real_st_h_<>_0_&_|.h.|_<_dd1_holds_ (|.h.|_")_*_||.((R2_*_(L_+_R1))_/._h).||_<_ee_)_) let ee be Real; ::_thesis: ( ee > 0 implies ex dd1 being Real st ( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) ) assume A9: ee > 0 ; ::_thesis: ex dd1 being Real st ( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) set e = ee / 2; A10: ee / 2 < ee by A9, XREAL_1:216; set e1 = (ee / 2) / (1 + ||.r.||); ee / 2 > 0 by A9, XREAL_1:215; then 0 / (1 + ||.r.||) < (ee / 2) / (1 + ||.r.||) by XREAL_1:74; then consider d being Real such that A11: 0 < d and A12: for z being Point of (REAL-NS n) st ||.z.|| < d holds ||.(R2 /. z).|| <= ((ee / 2) / (1 + ||.r.||)) * ||.z.|| by A3, NDIFF_2:7; set d1 = d / (1 + ||.r.||); set dd1 = min (d0,(d / (1 + ||.r.||))); A13: min (d0,(d / (1 + ||.r.||))) <= d / (1 + ||.r.||) by XXREAL_0:17; A14: min (d0,(d / (1 + ||.r.||))) <= d0 by XXREAL_0:17; A15: now__::_thesis:_for_h_being_Real_st_h_<>_0_&_|.h.|_<_min_(d0,(d_/_(1_+_||.r.||)))_holds_ (|.h.|_")_*_||.((R2_*_(L_+_R1))_/._h).||_<_ee let h be Real; ::_thesis: ( h <> 0 & |.h.| < min (d0,(d / (1 + ||.r.||))) implies (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) assume that A16: h <> 0 and A17: |.h.| < min (d0,(d / (1 + ||.r.||))) ; ::_thesis: (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee |.h.| < d0 by A14, A17, XXREAL_0:2; then A18: ||.(R1 /. h).|| <= 1 * |.h.| by A2; A19: L . h = h * r by A4; reconsider p0 = 0 as Real ; (||.(L . h).|| - (||.r.|| * |.h.|)) + (||.r.|| * |.h.|) <= p0 + (||.r.|| * |.h.|) by A19, NORMSP_1:def_1; then ( ||.((L . h) + (R1 /. h)).|| <= ||.(L . h).|| + ||.(R1 /. h).|| & ||.(L . h).|| + ||.(R1 /. h).|| <= (||.r.|| * |.h.|) + (1 * |.h.|) ) by A18, NORMSP_1:def_1, XREAL_1:7; then A20: ||.((L . h) + (R1 /. h)).|| <= (||.r.|| + 1) * |.h.| by XXREAL_0:2; |.h.| < d / (1 + ||.r.||) by A13, A17, XXREAL_0:2; then (||.r.|| + 1) * |.h.| < (||.r.|| + 1) * (d / (1 + ||.r.||)) by XREAL_1:68; then ||.((L . h) + (R1 /. h)).|| < (||.r.|| + 1) * (d / (1 + ||.r.||)) by A20, XXREAL_0:2; then ||.((L . h) + (R1 /. h)).|| < d by XCMPLX_1:87; then A21: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + ||.r.||)) * ||.((L . h) + (R1 /. h)).|| by A12; ((ee / 2) / (1 + ||.r.||)) * ||.((L . h) + (R1 /. h)).|| <= ((ee / 2) / (1 + ||.r.||)) * ((||.r.|| + 1) * |.h.|) by A9, A20, XREAL_1:64; then A22: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + ||.r.||)) * ((||.r.|| + 1) * |.h.|) by A21, XXREAL_0:2; A23: R2 /. ((L . h) + (R1 /. h)) = R2 /. ((L /. h) + (R1 /. h)) .= R2 /. ((L + R1) /. h) by A7, VFUNCT_1:def_1 .= (R2 * (L + R1)) /. h by A7, A5, PARTFUN2:5 ; A24: |.h.| <> 0 by A16, COMPLEX1:45; then |.h.| > 0 by COMPLEX1:46; then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= (|.h.| ") * ((((ee / 2) / (1 + ||.r.||)) * (||.r.|| + 1)) * |.h.|) by A23, A22, XREAL_1:64; then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= ((|.h.| * (|.h.| ")) * ((ee / 2) / (1 + ||.r.||))) * (||.r.|| + 1) ; then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= (1 * ((ee / 2) / (1 + ||.r.||))) * (||.r.|| + 1) by A24, XCMPLX_0:def_7; then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= ee / 2 by XCMPLX_1:87; hence (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee by A10, XXREAL_0:2; ::_thesis: verum end; 0 / (1 + ||.r.||) < d / (1 + ||.r.||) by A11, XREAL_1:74; then 0 < min (d0,(d / (1 + ||.r.||))) by A1, XXREAL_0:15; hence ex dd1 being Real st ( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) by A15; ::_thesis: verum end; dom (R2 * (L + R1)) = dom (L + R1) by A5, RELAT_1:27 .= REAL by A6, PARTFUN1:def_2 ; then R2 * (L + R1) is total by PARTFUN1:def_2; hence R2 * (L + R1) is RestFunc of (REAL-NS m) by A8, Th23; ::_thesis: verum end; theorem Th49: :: NDIFF_4:49 for n, m being non empty Element of NAT for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L1 being LinearFunc of (REAL-NS n) for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) proof let n, m be non empty Element of NAT ; ::_thesis: for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L1 being LinearFunc of (REAL-NS n) for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) let R1 be RestFunc of (REAL-NS n); ::_thesis: ( R1 /. 0 = 0. (REAL-NS n) implies for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L1 being LinearFunc of (REAL-NS n) for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) ) assume A1: R1 /. 0 = 0. (REAL-NS n) ; ::_thesis: for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds for L1 being LinearFunc of (REAL-NS n) for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) let R2 be RestFunc of (REAL-NS n),(REAL-NS m); ::_thesis: ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) implies for L1 being LinearFunc of (REAL-NS n) for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) ) assume A2: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) ; ::_thesis: for L1 being LinearFunc of (REAL-NS n) for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) let L1 be LinearFunc of (REAL-NS n); ::_thesis: for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) let L2 be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); ::_thesis: (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) A3: L2 * R1 is RestFunc of (REAL-NS m) by Th47; R2 * (L1 + R1) is RestFunc of (REAL-NS m) by A1, A2, Th48; hence (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) by A3, NDIFF_3:7; ::_thesis: verum end; theorem :: NDIFF_4:50 for n, m being non empty Element of NAT for x0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) proof let n, m be non empty Element of NAT ; ::_thesis: for x0 being Element of REAL for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) let x0 be Element of REAL ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) set S = REAL-NS n; set T = REAL-NS m; let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( g is_differentiable_in x0 implies for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) ) assume A1: g is_differentiable_in x0 ; ::_thesis: for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) consider N1 being Neighbourhood of x0 such that A2: N1 c= dom g and A3: ex L1 being LinearFunc of (REAL-NS n) ex R1 being RestFunc of (REAL-NS n) st ( diff (g,x0) = L1 . 1 & ( for x being Real st x in N1 holds (g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) ) ) by A1, NDIFF_3:def_4; let f be PartFunc of (REAL-NS n),(REAL-NS m); ::_thesis: ( f is_differentiable_in g /. x0 implies ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) ) assume f is_differentiable_in g /. x0 ; ::_thesis: ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) then consider N2 being Neighbourhood of g /. x0 such that A4: N2 c= dom f and A5: ex R2 being RestFunc of (REAL-NS n),(REAL-NS m) st ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) & R2 is_continuous_in 0. (REAL-NS n) & ( for y being Point of (REAL-NS n) st y in N2 holds (f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0))) ) ) by NDIFF_1:47; consider R2 being RestFunc of (REAL-NS n),(REAL-NS m) such that A6: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) and A7: for y being Point of (REAL-NS n) st y in N2 holds (f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0))) by A5; reconsider L2 = diff (f,(g /. x0)) as Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) by LOPBAN_1:def_9; consider L1 being LinearFunc of (REAL-NS n), R1 being RestFunc of (REAL-NS n) such that A8: ( diff (g,x0) = L1 . 1 & ( for x being Real st x in N1 holds (g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) ) ) by A3; consider r being Point of (REAL-NS n) such that A9: for p being Real holds L1 . p = p * r by NDIFF_3:def_2; reconsider p0 = 0 as Element of REAL ; (g /. x0) - (g /. x0) = (L1 . (x0 - x0)) + (R1 /. (x0 - x0)) by A8, RCOMP_1:16; then 0. (REAL-NS n) = (L1 . 0) + (R1 /. 0) by RLVECT_1:15; then 0. (REAL-NS n) = (p0 * r) + (R1 /. 0) by A9; then 0. (REAL-NS n) = (0. (REAL-NS n)) + (R1 /. 0) by RLVECT_1:10; then A10: R1 /. 0 = 0. (REAL-NS n) by RLVECT_1:4; A11: dom (L2 * L1) = REAL by FUNCT_2:def_1; reconsider q = L2 . r as Point of (REAL-NS m) ; for p being Real holds (L2 * L1) . p = p * q proof let p be Real; ::_thesis: (L2 * L1) . p = p * q L2 . (L1 . p) = L2 . (p * r) by A9 .= p * q by LOPBAN_1:def_5 ; hence (L2 * L1) . p = p * q by A11, FUNCT_1:12; ::_thesis: verum end; then reconsider L0 = L2 * L1 as LinearFunc of (REAL-NS m) by NDIFF_3:def_2; g is_continuous_in x0 by A1, NDIFF_3:22; then consider N3 being Neighbourhood of x0 such that A12: g .: N3 c= N2 by NFCONT_3:10; reconsider R0 = (L2 * R1) + (R2 * (L1 + R1)) as RestFunc of (REAL-NS m) by A10, A6, Th49; consider N being Neighbourhood of x0 such that A13: N c= N1 and A14: N c= N3 by RCOMP_1:17; A15: N c= dom (f * g) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N or x in dom (f * g) ) assume A16: x in N ; ::_thesis: x in dom (f * g) then reconsider x9 = x as Real ; A17: x in N1 by A13, A16; then g . x9 in g .: N3 by A2, A14, A16, FUNCT_1:def_6; then g . x9 in N2 by A12; hence x in dom (f * g) by A2, A4, A17, FUNCT_1:11; ::_thesis: verum end; A18: now__::_thesis:_for_x_being_Real_st_x_in_N_holds_ ((f_*_g)_/._x)_-_((f_*_g)_/._x0)_=_(L0_._(x_-_x0))_+_(R0_/._(x_-_x0)) let x be Real; ::_thesis: ( x in N implies ((f * g) /. x) - ((f * g) /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0)) ) assume A19: x in N ; ::_thesis: ((f * g) /. x) - ((f * g) /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0)) A20: (g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A8, A13, A19; x in N1 by A13, A19; then g . x in g .: N3 by A2, A14, A19, FUNCT_1:def_6; then A21: g . x in N2 by A12; x in N1 by A13, A19; then A22: g /. x in N2 by A2, A21, PARTFUN1:def_6; A23: x0 in N by RCOMP_1:16; A24: R1 is total by NDIFF_3:def_1; then A25: dom R1 = REAL by PARTFUN1:def_2; dom L2 = the carrier of (REAL-NS n) by FUNCT_2:def_1; then A26: rng R1 c= dom L2 ; A27: dom (L2 * R1) = REAL by A24, PARTFUN1:def_2; A28: L1 + R1 is total by A24, VFUNCT_1:32; then A29: dom (L1 + R1) = REAL by PARTFUN1:def_2; R2 is total by NDIFF_1:def_5; then dom R2 = the carrier of (REAL-NS n) by PARTFUN1:def_2; then A30: rng (L1 + R1) c= dom R2 ; then dom (R2 * (L1 + R1)) = dom (L1 + R1) by RELAT_1:27 .= REAL by A28, PARTFUN1:def_2 ; then A31: dom ((L2 * R1) + (R2 * (L1 + R1))) = REAL /\ REAL by A27, VFUNCT_1:def_1 .= REAL ; A32: L2 . (R1 /. (x - x0)) = L2 /. (R1 /. (x - x0)) .= (L2 * R1) /. (x - x0) by A25, A26, PARTFUN2:5 ; A33: R2 /. ((L1 . (x - x0)) + (R1 /. (x - x0))) = R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0))) .= R2 /. ((L1 + R1) /. (x - x0)) by A29, VFUNCT_1:def_1 .= (R2 * (L1 + R1)) /. (x - x0) by A29, A30, PARTFUN2:5 ; A34: (L2 * L1) . (x - x0) = L2 . (L1 . (x - x0)) by A11, FUNCT_1:12; thus ((f * g) /. x) - ((f * g) /. x0) = (f /. (g /. x)) - ((f * g) /. x0) by A15, A19, PARTFUN2:3 .= (f /. (g /. x)) - (f /. (g /. x0)) by A15, A23, PARTFUN2:3 .= ((diff (f,(g /. x0))) . ((g /. x) - (g /. x0))) + (R2 /. ((g /. x) - (g /. x0))) by A7, A22 .= ((L2 . (L1 . (x - x0))) + (L2 . (R1 /. (x - x0)))) + ((R2 * (L1 + R1)) /. (x - x0)) by A20, A33, VECTSP_1:def_20 .= (L2 . (L1 . (x - x0))) + (((L2 * R1) /. (x - x0)) + ((R2 * (L1 + R1)) /. (x - x0))) by A32, RLVECT_1:def_3 .= (L0 . (x - x0)) + (R0 /. (x - x0)) by A34, A31, VFUNCT_1:def_1 ; ::_thesis: verum end; hence A35: f * g is_differentiable_in x0 by A15, NDIFF_3:def_3; ::_thesis: diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) (L2 * L1) . 1 = (diff (f,(g /. x0))) . (diff (g,x0)) by A8, A11, FUNCT_1:12; hence diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) by A35, A15, A18, NDIFF_3:def_4; ::_thesis: verum end;