:: PDIFF_1 semantic presentation begin definition let i, n be Nat; func proj (i,n) -> Function of (REAL n),REAL means :Def1: :: PDIFF_1:def 1 for x being Element of REAL n holds it . x = x . i; existence ex b1 being Function of (REAL n),REAL st for x being Element of REAL n holds b1 . x = x . i proof deffunc H1( Element of REAL n) -> Element of REAL = \$1 . i; thus ex f being Function of (REAL n),REAL st for x being Element of REAL n holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (REAL n),REAL st ( for x being Element of REAL n holds b1 . x = x . i ) & ( for x being Element of REAL n holds b2 . x = x . i ) holds b1 = b2 proof let f, g be Function of (REAL n),REAL; ::_thesis: ( ( for x being Element of REAL n holds f . x = x . i ) & ( for x being Element of REAL n holds g . x = x . i ) implies f = g ) assume that A1: for x being Element of REAL n holds f . x = x . i and A2: for x being Element of REAL n holds g . x = x . i ; ::_thesis: f = g now__::_thesis:_for_x_being_Element_of_REAL_n_holds_f_._x_=_g_._x let x be Element of REAL n; ::_thesis: f . x = g . x f . x = x . i by A1; hence f . x = g . x by A2; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines proj PDIFF_1:def_1_:_ for i, n being Nat for b3 being Function of (REAL n),REAL holds ( b3 = proj (i,n) iff for x being Element of REAL n holds b3 . x = x . i ); set W = (proj (1,1)) " ; Lm1: ( proj (1,1) is bijective & 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 x1, x2 being set st x1 in dom (proj (1,1)) & x2 in dom (proj (1,1)) & (proj (1,1)) . x1 = (proj (1,1)) . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom (proj (1,1)) & x2 in dom (proj (1,1)) & (proj (1,1)) . x1 = (proj (1,1)) . x2 implies x1 = x2 ) assume that A1: x1 in dom (proj (1,1)) and A2: x2 in dom (proj (1,1)) and A3: (proj (1,1)) . x1 = (proj (1,1)) . x2 ; ::_thesis: x1 = x2 reconsider y1 = x1, y2 = x2 as Element of REAL 1 by A1, A2; x1 is Tuple of 1, REAL by A1, FINSEQ_2:131; then consider d1 being Element of REAL such that A4: x1 = <*d1*> by FINSEQ_2:97; d1 = <*d1*> . 1 by FINSEQ_1:40; then d1 = (proj (1,1)) . y1 by A4, Def1; then A5: d1 = y2 . 1 by A3, Def1; x2 is Tuple of 1, REAL by A2, FINSEQ_2:131; then ex d2 being Element of REAL st x2 = <*d2*> by FINSEQ_2:97; hence x1 = x2 by A4, A5, FINSEQ_1:40; ::_thesis: verum end; then A6: proj (1,1) is one-to-one by FUNCT_1:def_4; A7: dom (proj (1,1)) = REAL 1 by FUNCT_2:def_1; A8: now__::_thesis:_for_x_being_Element_of_REAL_holds_ (_(proj_(1,1))_._<*x*>_=_x_&_((proj_(1,1))_")_._x_=_<*x*>_) let x be Element of REAL ; ::_thesis: ( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) A9: <*x*> is Element of 1 -tuples_on REAL by FINSEQ_2:98; then (proj (1,1)) . <*x*> = <*x*> . 1 by Def1; hence (proj (1,1)) . <*x*> = x by FINSEQ_1:40; ::_thesis: ((proj (1,1)) ") . x = <*x*> hence ((proj (1,1)) ") . x = <*x*> by A7, A6, A9, FUNCT_1:34; ::_thesis: verum end; A10: 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 Def1; 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; then rng (proj (1,1)) = REAL by FUNCT_2:10; then proj (1,1) is onto by FUNCT_2:def_3; hence ( proj (1,1) is bijective & 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 A6, A10, A8, FUNCT_2:10, FUNCT_2:def_1; ::_thesis: verum end; Lm2: for i, n being Element of NAT st i in Seg n holds proj (i,n) is onto proof let i, n be Element of NAT ; ::_thesis: ( i in Seg n implies proj (i,n) is onto ) set f = proj (i,n); assume A1: i in Seg n ; ::_thesis: proj (i,n) is onto for y being set st y in REAL holds ex x being set st ( x in REAL n & y = (proj (i,n)) . x ) proof let y be set ; ::_thesis: ( y in REAL implies ex x being set st ( x in REAL n & y = (proj (i,n)) . x ) ) assume y in REAL ; ::_thesis: ex x being set st ( x in REAL n & y = (proj (i,n)) . x ) then reconsider y1 = y as Element of REAL ; reconsider x = n |-> y1 as Element of REAL n ; (proj (i,n)) . x = x . i by Def1; then (proj (i,n)) . x = y by A1, FINSEQ_2:57; hence ex x being set st ( x in REAL n & y = (proj (i,n)) . x ) ; ::_thesis: verum end; then rng (proj (i,n)) = REAL by FUNCT_2:10; hence proj (i,n) is onto by FUNCT_2:def_3; ::_thesis: verum end; theorem :: PDIFF_1:1 ( ( for i, n being Element of NAT st i in Seg n holds ( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Element of REAL holds ( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) proof now__::_thesis:_for_i,_n_being_Element_of_NAT_st_i_in_Seg_n_holds_ (_dom_(proj_(i,n))_=_REAL_n_&_rng_(proj_(i,n))_=_REAL_) let i, n be Element of NAT ; ::_thesis: ( i in Seg n implies ( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) assume A1: i in Seg n ; ::_thesis: ( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) thus dom (proj (i,n)) = REAL n by FUNCT_2:def_1; ::_thesis: rng (proj (i,n)) = REAL proj (i,n) is onto by A1, Lm2; hence rng (proj (i,n)) = REAL by FUNCT_2:def_3; ::_thesis: verum end; hence ( ( for i, n being Element of NAT st i in Seg n holds ( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Element of REAL holds ( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by Lm1; ::_thesis: verum end; theorem Th2: :: PDIFF_1:2 ( (proj (1,1)) " is Function of REAL,(REAL 1) & (proj (1,1)) " is one-to-one & dom ((proj (1,1)) ") = REAL & rng ((proj (1,1)) ") = REAL 1 & ex g being Function of REAL,(REAL 1) st ( g is bijective & (proj (1,1)) " = g ) ) proof A1: REAL 1 = rng ((proj (1,1)) ") by Lm1, FUNCT_1:33; REAL = dom ((proj (1,1)) ") by Lm1, FUNCT_1:33; then reconsider g = (proj (1,1)) " as Function of REAL,(REAL 1) by A1, FUNCT_2:1; g is onto by A1, FUNCT_2:def_3; hence ( (proj (1,1)) " is Function of REAL,(REAL 1) & (proj (1,1)) " is one-to-one & dom ((proj (1,1)) ") = REAL & rng ((proj (1,1)) ") = REAL 1 & ex g being Function of REAL,(REAL 1) st ( g is bijective & (proj (1,1)) " = g ) ) by Lm1, FUNCT_1:33; ::_thesis: verum end; registration cluster proj (1,1) -> bijective ; coherence proj (1,1) is bijective by Lm1; end; definition let g be PartFunc of REAL,REAL; func <>* g -> PartFunc of (REAL 1),(REAL 1) equals :: PDIFF_1:def 2 (((proj (1,1)) ") * g) * (proj (1,1)); coherence (((proj (1,1)) ") * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1) proof reconsider f = (proj (1,1)) " as PartFunc of REAL,(REAL 1) by PARTFUN1:9; (f * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1) ; hence (((proj (1,1)) ") * g) * (proj (1,1)) is PartFunc of (REAL 1),(REAL 1) ; ::_thesis: verum end; end; :: deftheorem defines <>* PDIFF_1:def_2_:_ for g being PartFunc of REAL,REAL holds <>* g = (((proj (1,1)) ") * g) * (proj (1,1)); definition let n be Nat; let g be PartFunc of (REAL n),REAL; func <>* g -> PartFunc of (REAL n),(REAL 1) equals :: PDIFF_1:def 3 ((proj (1,1)) ") * g; correctness coherence ((proj (1,1)) ") * g is PartFunc of (REAL n),(REAL 1); proof reconsider f = (proj (1,1)) " as PartFunc of REAL,(REAL 1) by PARTFUN1:9; f * g is PartFunc of (REAL n),(REAL 1) ; hence ((proj (1,1)) ") * g is PartFunc of (REAL n),(REAL 1) ; ::_thesis: verum end; end; :: deftheorem defines <>* PDIFF_1:def_3_:_ for n being Nat for g being PartFunc of (REAL n),REAL holds <>* g = ((proj (1,1)) ") * g; definition let i, n be Nat; func Proj (i,n) -> Function of (REAL-NS n),(REAL-NS 1) means :Def4: :: PDIFF_1:def 4 for x being Point of (REAL-NS n) holds it . x = <*((proj (i,n)) . x)*>; existence ex b1 being Function of (REAL-NS n),(REAL-NS 1) st for x being Point of (REAL-NS n) holds b1 . x = <*((proj (i,n)) . x)*> proof deffunc H1( Point of (REAL-NS n)) -> FinSequence of REAL = <*((proj (i,n)) . \$1)*>; A1: for x being Point of (REAL-NS n) holds H1(x) is Element of (REAL-NS 1) proof let x be Point of (REAL-NS n); ::_thesis: H1(x) is Element of (REAL-NS 1) len H1(x) = 1 by FINSEQ_1:39; then H1(x) is Element of 1 -tuples_on REAL by FINSEQ_2:92; then H1(x) in REAL 1 ; hence H1(x) is Element of (REAL-NS 1) by REAL_NS1:def_4; ::_thesis: verum end; thus ex f being Function of (REAL-NS n),(REAL-NS 1) st for x being Point of (REAL-NS n) holds f . x = H1(x) from FUNCT_2:sch_9(A1); ::_thesis: verum end; uniqueness for b1, b2 being Function of (REAL-NS n),(REAL-NS 1) st ( for x being Point of (REAL-NS n) holds b1 . x = <*((proj (i,n)) . x)*> ) & ( for x being Point of (REAL-NS n) holds b2 . x = <*((proj (i,n)) . x)*> ) holds b1 = b2 proof let f, g be Function of (REAL-NS n),(REAL-NS 1); ::_thesis: ( ( for x being Point of (REAL-NS n) holds f . x = <*((proj (i,n)) . x)*> ) & ( for x being Point of (REAL-NS n) holds g . x = <*((proj (i,n)) . x)*> ) implies f = g ) assume that A2: for x being Point of (REAL-NS n) holds f . x = <*((proj (i,n)) . x)*> and A3: for x being Point of (REAL-NS n) holds g . x = <*((proj (i,n)) . x)*> ; ::_thesis: f = g now__::_thesis:_for_x_being_Point_of_(REAL-NS_n)_holds_f_._x_=_g_._x let x be Point of (REAL-NS n); ::_thesis: f . x = g . x f . x = <*((proj (i,n)) . x)*> by A2; hence f . x = g . x by A3; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines Proj PDIFF_1:def_4_:_ for i, n being Nat for b3 being Function of (REAL-NS n),(REAL-NS 1) holds ( b3 = Proj (i,n) iff for x being Point of (REAL-NS n) holds b3 . x = <*((proj (i,n)) . x)*> ); definition let i be Element of NAT ; let x be FinSequence of REAL ; func reproj (i,x) -> Function means :Def5: :: PDIFF_1:def 5 ( dom it = REAL & ( for r being Element of REAL holds it . r = Replace (x,i,r) ) ); existence ex b1 being Function st ( dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) ) proof deffunc H1( Element of REAL ) -> FinSequence of REAL = Replace (x,i,\$1); consider f being Function such that A1: ( dom f = REAL & ( for r being Element of REAL st r in REAL holds f . r = H1(r) ) ) from GRAPH_5:sch_1(); take f ; ::_thesis: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) ) thus ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace (x,i,r) ) & dom b2 = REAL & ( for r being Element of REAL holds b2 . r = Replace (x,i,r) ) holds b1 = b2 proof let f, g be Function; ::_thesis: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) & dom g = REAL & ( for r being Element of REAL holds g . r = Replace (x,i,r) ) implies f = g ) assume that A2: dom f = REAL and A3: for r being Element of REAL holds f . r = Replace (x,i,r) and A4: dom g = REAL and A5: for r being Element of REAL holds g . r = Replace (x,i,r) ; ::_thesis: f = g now__::_thesis:_for_p_being_set_st_p_in_dom_f_holds_ f_._p_=_g_._p let p be set ; ::_thesis: ( p in dom f implies f . p = g . p ) assume p in dom f ; ::_thesis: f . p = g . p then reconsider r = p as Element of REAL by A2; f . r = Replace (x,i,r) by A3; hence f . p = g . p by A5; ::_thesis: verum end; hence f = g by A2, A4, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines reproj PDIFF_1:def_5_:_ for i being Element of NAT for x being FinSequence of REAL for b3 being Function holds ( b3 = reproj (i,x) iff ( dom b3 = REAL & ( for r being Element of REAL holds b3 . r = Replace (x,i,r) ) ) ); definition let n, i be Element of NAT ; let x be Element of REAL n; :: original: reproj redefine func reproj (i,x) -> Function of REAL,(REAL n); correctness coherence reproj (i,x) is Function of REAL,(REAL n); proof A1: now__::_thesis:_for_p_being_set_st_p_in_REAL_holds_ (reproj_(i,x))_._p_in_REAL_n let p be set ; ::_thesis: ( p in REAL implies (reproj (i,x)) . p in REAL n ) assume p in REAL ; ::_thesis: (reproj (i,x)) . p in REAL n then reconsider r = p as Element of REAL ; A2: (reproj (i,x)) . r = Replace (x,i,r) by Def5; then reconsider IT = (reproj (i,x)) . r as FinSequence of REAL ; len IT = len x by A2, FINSEQ_7:5 .= n by CARD_1:def_7 ; then reconsider IT = IT as Element of n -tuples_on REAL by FINSEQ_2:92; IT is Element of REAL n ; hence (reproj (i,x)) . p in REAL n ; ::_thesis: verum end; dom (reproj (i,x)) = REAL by Def5; hence reproj (i,x) is Function of REAL,(REAL n) by A1, FUNCT_2:3; ::_thesis: verum end; end; definition let n, i be Element of NAT ; let x be Point of (REAL-NS n); func reproj (i,x) -> Function of (REAL-NS 1),(REAL-NS n) means :Def6: :: PDIFF_1:def 6 for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & it . r = (reproj (i,y)) . q ); existence ex b1 being Function of (REAL-NS 1),(REAL-NS n) st for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & b1 . r = (reproj (i,y)) . q ) proof defpred S1[ Element of (REAL-NS 1), Point of (REAL-NS n)] means ex q being Element of REAL ex z being Element of REAL n st ( \$1 = <*q*> & z = x & \$2 = (reproj (i,z)) . q ); A1: for r being Element of (REAL-NS 1) ex y being Element of (REAL-NS n) st S1[r,y] proof reconsider z = x as Element of REAL n by REAL_NS1:def_4; let r be Element of (REAL-NS 1); ::_thesis: ex y being Element of (REAL-NS n) st S1[r,y] r is Element of REAL 1 by REAL_NS1:def_4; then consider q being Element of REAL such that A2: r = <*q*> by FINSEQ_2:97; (reproj (i,z)) . q is Element of (REAL-NS n) by REAL_NS1:def_4; hence ex y being Element of (REAL-NS n) st S1[r,y] by A2; ::_thesis: verum end; thus ex f being Function of (REAL-NS 1),(REAL-NS n) st for r being Element of (REAL-NS 1) holds S1[r,f . r] from FUNCT_2:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being Function of (REAL-NS 1),(REAL-NS n) st ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & b1 . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & b2 . r = (reproj (i,y)) . q ) ) holds b1 = b2 proof let f, g be Function of (REAL-NS 1),(REAL-NS n); ::_thesis: ( ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ) implies f = g ) assume that A3: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) and A4: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ; ::_thesis: f = g now__::_thesis:_for_r_being_Point_of_(REAL-NS_1)_holds_f_._r_=_g_._r let r be Point of (REAL-NS 1); ::_thesis: f . r = g . r consider p being Element of REAL , y being Element of REAL n such that A5: r = <*p*> and A6: y = x and A7: f . r = (reproj (i,y)) . p by A3; A8: ex q being Element of REAL ex z being Element of REAL n st ( r = <*q*> & z = x & g . r = (reproj (i,z)) . q ) by A4; p = <*p*> . 1 by FINSEQ_1:def_8; hence f . r = g . r by A5, A6, A7, A8, FINSEQ_1:def_8; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines reproj PDIFF_1:def_6_:_ for n, i being Element of NAT for x being Point of (REAL-NS n) for b4 being Function of (REAL-NS 1),(REAL-NS n) holds ( b4 = reproj (i,x) iff for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st ( r = <*q*> & y = x & b4 . r = (reproj (i,y)) . q ) ); definition let m, n be non empty Element of NAT ; let f be PartFunc of (REAL m),(REAL n); let x be Element of REAL m; predf is_differentiable_in x means :Def7: :: PDIFF_1:def 7 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & g is_differentiable_in y ); end; :: deftheorem Def7 defines is_differentiable_in PDIFF_1:def_7_:_ for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m holds ( f is_differentiable_in x iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & g is_differentiable_in y ) ); definition let m, n be non empty Element of NAT ; let f be PartFunc of (REAL m),(REAL n); let x be Element of REAL m; assume A1: f is_differentiable_in x ; func diff (f,x) -> Function of (REAL m),(REAL n) means :Def8: :: PDIFF_1:def 8 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & it = diff (g,y) ); correctness existence ex b1 being Function of (REAL m),(REAL n) ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = diff (g,y) ); uniqueness for b1, b2 being Function of (REAL m),(REAL n) st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b2 = diff (g,y) ) holds b1 = b2; proof A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that A3: f = g and A4: x = y and g is_differentiable_in y by A1, Def7; the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4; then diff (g,y) is Function of (REAL m),(REAL n) by A2, LOPBAN_1:def_9; hence ( ex b1 being Function of (REAL m),(REAL n) ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = diff (g,y) ) & ( for b1, b2 being Function of (REAL m),(REAL n) st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b2 = diff (g,y) ) holds b1 = b2 ) ) by A3, A4; ::_thesis: verum end; end; :: deftheorem Def8 defines diff PDIFF_1:def_8_:_ for m, n being non empty Element of NAT for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_differentiable_in x holds for b5 being Function of (REAL m),(REAL n) holds ( b5 = diff (f,x) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b5 = diff (g,y) ) ); theorem Th3: :: PDIFF_1:3 for I being Function of REAL,(REAL 1) st I = (proj (1,1)) " holds ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL st x = I . y holds ||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st x = I . y holds a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st x = I . a holds - x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x - y = I . (a - b) ) ) proof let I be Function of REAL,(REAL 1); ::_thesis: ( I = (proj (1,1)) " implies ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL st x = I . y holds ||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st x = I . y holds a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st x = I . a holds - x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x - y = I . (a - b) ) ) ) assume A1: I = (proj (1,1)) " ; ::_thesis: ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL st x = I . y holds ||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st x = I . y holds a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st x = I . a holds - x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x - y = I . (a - b) ) ) hereby ::_thesis: ( ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x + y = I . (a + b) ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st x = I . y holds a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st x = I . a holds - x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x - y = I . (a - b) ) ) let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL st x = I . y holds ||.x.|| = abs y let y be Element of REAL ; ::_thesis: ( x = I . y implies ||.x.|| = abs y ) reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4; assume x = I . y ; ::_thesis: ||.x.|| = abs y then xx = <*y*> by A1, Lm1; then sqrt (Sum (sqr xx)) = sqrt (Sum <*(y ^2)*>) by RVSUM_1:55; then A2: sqrt (Sum (sqr xx)) = sqrt (y ^2) by RVSUM_1:73; ||.x.|| = |.xx.| by REAL_NS1:1; hence ||.x.|| = abs y by A2, COMPLEX1:72; ::_thesis: verum end; A3: now__::_thesis:_for_x,_y_being_VECTOR_of_(REAL-NS_1) for_a,_b_being_Element_of_REAL_st_x_=_I_._a_&_y_=_I_._b_holds_ x_-_y_=_I_._(a_-_b) let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st x = I . a & y = I . b holds x - y = I . (a - b) let a, b be Element of REAL ; ::_thesis: ( x = I . a & y = I . b implies x - y = I . (a - b) ) reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4; assume that A4: x = I . a and A5: y = I . b ; ::_thesis: x - y = I . (a - b) A6: <*b*> = yy by A1, A5, Lm1; <*a*> = xx by A1, A4, Lm1; then x - y = <*a*> - <*b*> by A6, REAL_NS1:5; then x - y = <*(a - b)*> by RVSUM_1:29; hence x - y = I . (a - b) by A1, Lm1; ::_thesis: verum end; hereby ::_thesis: ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st x = I . y holds a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st x = I . a holds - x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x - y = I . (a - b) ) ) let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st x = I . a & y = I . b holds x + y = I . (a + b) let a, b be Element of REAL ; ::_thesis: ( x = I . a & y = I . b implies x + y = I . (a + b) ) reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4; assume that A7: x = I . a and A8: y = I . b ; ::_thesis: x + y = I . (a + b) A9: <*b*> = yy by A1, A8, Lm1; <*a*> = xx by A1, A7, Lm1; then x + y = <*a*> + <*b*> by A9, REAL_NS1:2; then x + y = <*(a + b)*> by RVSUM_1:13; hence x + y = I . (a + b) by A1, Lm1; ::_thesis: verum end; A10: now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1) for_y_being_Element_of_REAL_ for_a_being_Real_st_x_=_I_._y_holds_ a_*_x_=_I_._(a_*_y) let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL for a being Real st x = I . y holds a * x = I . (a * y) let y be Element of REAL ; ::_thesis: for a being Real st x = I . y holds a * x = I . (a * y) let a be Real; ::_thesis: ( x = I . y implies a * x = I . (a * y) ) reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4; assume x = I . y ; ::_thesis: a * x = I . (a * y) then A11: xx = <*y*> by A1, Lm1; a * x = a * xx by REAL_NS1:3; then a * x = <*(a * y)*> by A11, RVSUM_1:47; hence a * x = I . (a * y) by A1, Lm1; ::_thesis: verum end; now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1) for_a_being_Element_of_REAL_st_x_=_I_._a_holds_ -_x_=_I_._(-_a) let x be VECTOR of (REAL-NS 1); ::_thesis: for a being Element of REAL st x = I . a holds - x = I . (- a) let a be Element of REAL ; ::_thesis: ( x = I . a implies - x = I . (- a) ) assume x = I . a ; ::_thesis: - x = I . (- a) then (- 1) * x = I . ((- 1) * a) by A10; hence - x = I . (- a) by RLVECT_1:16; ::_thesis: verum end; hence ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st x = I . y holds a * x = I . (a * y) ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st x = I . a holds - x = I . (- a) ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st x = I . a & y = I . b holds x - y = I . (a - b) ) ) by A10, A3; ::_thesis: verum end; reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2; theorem Th4: :: PDIFF_1:4 for J being Function of (REAL 1),REAL st J = proj (1,1) holds ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL st J . x = y holds ||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st J . x = y holds J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st J . x = a holds J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b ) ) proof let J be Function of (REAL 1),REAL; ::_thesis: ( J = proj (1,1) implies ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL st J . x = y holds ||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st J . x = y holds J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st J . x = a holds J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b ) ) ) assume A1: J = proj (1,1) ; ::_thesis: ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL st J . x = y holds ||.x.|| = abs y ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st J . x = y holds J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st J . x = a holds J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b ) ) hereby ::_thesis: ( ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x + y) = a + b ) & ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st J . x = y holds J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st J . x = a holds J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b ) ) let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL st J . x = y holds ||.x.|| = abs y let y be Element of REAL ; ::_thesis: ( J . x = y implies ||.x.|| = abs y ) reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4; assume J . x = y ; ::_thesis: ||.x.|| = abs y then I . (J . xx) = I . y ; then x = I . y by A1, Lm1, FUNCT_1:34; hence ||.x.|| = abs y by Th3; ::_thesis: verum end; hereby ::_thesis: ( ( for x being VECTOR of (REAL-NS 1) for y being Element of REAL for a being Real st J . x = y holds J . (a * x) = a * y ) & ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st J . x = a holds J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b ) ) let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st J . x = a & J . y = b holds J . (x + y) = a + b let a, b be Element of REAL ; ::_thesis: ( J . x = a & J . y = b implies J . (x + y) = a + b ) reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4; assume that A2: J . x = a and A3: J . y = b ; ::_thesis: J . (x + y) = a + b I . (J . yy) = I . b by A3; then A4: y = I . b by A1, Lm1, FUNCT_1:34; I . (J . xx) = I . a by A2; then x = I . a by A1, Lm1, FUNCT_1:34; then J . (x + y) = J . (I . (a + b)) by A4, Th3; hence J . (x + y) = a + b by A1, Lm1, FUNCT_1:35; ::_thesis: verum end; hereby ::_thesis: ( ( for x being VECTOR of (REAL-NS 1) for a being Element of REAL st J . x = a holds J . (- x) = - a ) & ( for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b ) ) let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL for a being Real st J . x = y holds J . (a * x) = a * y let y be Element of REAL ; ::_thesis: for a being Real st J . x = y holds J . (a * x) = a * y let a be Real; ::_thesis: ( J . x = y implies J . (a * x) = a * y ) reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4; assume J . x = y ; ::_thesis: J . (a * x) = a * y then I . (J . xx) = I . y ; then x = I . y by A1, Lm1, FUNCT_1:34; then J . (a * x) = J . (I . (a * y)) by Th3; hence J . (a * x) = a * y by A1, Lm1, FUNCT_1:35; ::_thesis: verum end; hereby ::_thesis: for x, y being VECTOR of (REAL-NS 1) for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b let x be VECTOR of (REAL-NS 1); ::_thesis: for y being Element of REAL st J . x = y holds J . (- x) = - y let y be Element of REAL ; ::_thesis: ( J . x = y implies J . (- x) = - y ) reconsider xx = x as Element of REAL 1 by REAL_NS1:def_4; assume J . x = y ; ::_thesis: J . (- x) = - y then I . y = I . (J . xx) ; then x = I . y by A1, Lm1, FUNCT_1:34; then J . (- x) = J . (I . (- y)) by Th3; hence J . (- x) = - y by A1, Lm1, FUNCT_1:35; ::_thesis: verum end; let x, y be VECTOR of (REAL-NS 1); ::_thesis: for a, b being Element of REAL st J . x = a & J . y = b holds J . (x - y) = a - b let a, b be Element of REAL ; ::_thesis: ( J . x = a & J . y = b implies J . (x - y) = a - b ) reconsider xx = x, yy = y as Element of REAL 1 by REAL_NS1:def_4; assume that A5: J . x = a and A6: J . y = b ; ::_thesis: J . (x - y) = a - b I . (J . yy) = I . b by A6; then A7: y = I . b by A1, Lm1, FUNCT_1:34; I . (J . xx) = I . a by A5; then x = I . a by A1, Lm1, FUNCT_1:34; then J . (x - y) = J . (I . (a - b)) by A7, Th3; hence J . (x - y) = a - b by A1, Lm1, FUNCT_1:35; ::_thesis: verum end; theorem Th5: :: PDIFF_1:5 for I being Function of REAL,(REAL 1) for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) proof let I be Function of REAL,(REAL 1); ::_thesis: for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) let J be Function of (REAL 1),REAL; ::_thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) ) assume that A1: I = (proj (1,1)) " and A2: J = proj (1,1) ; ::_thesis: ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) thus for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ::_thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc proof let R be RestFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: (J * R) * I is RestFunc A3: R is total by NDIFF_1:def_5; the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider R0 = R as Function of (REAL 1),(REAL 1) by A3; reconsider R1 = (J * R) * I as PartFunc of REAL,REAL ; A4: (J * R0) * I is Function of REAL,REAL ; then A5: dom R1 = REAL by FUNCT_2:def_1; A6: for r being Real st r > 0 holds ex d being Real st ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds ((abs z1) ") * (abs (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 & abs z1 < d holds ((abs z1) ") * (abs (R1 . z1)) < r ) ) ) assume r > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds ((abs z1) ") * (abs (R1 . z1)) < r ) ) then consider d being Real such that A7: d > 0 and A8: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds (||.z.|| ") * ||.(R /. z).|| < r by A3, NDIFF_1:23; take d ; ::_thesis: ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds ((abs z1) ") * (abs (R1 . z1)) < r ) ) for z1 being Real st z1 <> 0 & abs z1 < d holds ((abs z1) ") * (abs (R1 . z1)) < r proof let z1 be Real; ::_thesis: ( z1 <> 0 & abs z1 < d implies ((abs z1) ") * (abs (R1 . z1)) < r ) assume that A9: z1 <> 0 and A10: abs z1 < d ; ::_thesis: ((abs z1) ") * (abs (R1 . z1)) < r reconsider z = I . z1 as Point of (REAL-NS 1) by REAL_NS1:def_4; z1 in REAL ; then reconsider z1r = z1 as R_eal by NUMBERS:31; 0 < |.z1r.| by A9, EXTREAL2:4; then abs z1 > 0 by EXTREAL2:1; then ||.z.|| <> 0 by A1, Th3; then A11: z <> 0. (REAL-NS 1) by NORMSP_0:def_6; I * J = id (dom (proj (1,1))) by A1, A2, FUNCT_1:39; then A12: I * J = id (REAL 1) by FUNCT_2:def_1; A13: dom (J * R0) = REAL 1 by FUNCT_2:def_1; R is total by NDIFF_1:def_5; then A14: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2; then R /. z = R . z by PARTFUN1:def_6; then R /. z = ((id the carrier of (REAL-NS 1)) * R) . (I . z1) by FUNCT_2:17; then R /. z = ((I * J) * R) . (I . z1) by A12, REAL_NS1:def_4; then A15: R /. z = (I * J) . (R . (I . z1)) by A14, FUNCT_1:13; dom J = REAL 1 by FUNCT_2:def_1; then R /. z = I . (J . (R0 . z)) by A15, FUNCT_1:13, FUNCT_2:5; then R /. z = I . ((J * R0) . (I . z1)) by A13, FUNCT_1:12; then R /. z = I . (R1 . z1) by A5, FUNCT_1:12; then A16: ||.(R /. z).|| = abs (R1 . z1) by A1, Th3; A17: ||.z.|| " = (abs z1) " by A1, Th3; ||.z.|| < d by A1, A10, Th3; hence ((abs z1) ") * (abs (R1 . z1)) < r by A8, A11, A17, A16; ::_thesis: verum end; hence ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds ((abs z1) ") * (abs (R1 . z1)) < r ) ) by A7; ::_thesis: verum end; for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) proof let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) A18: now__::_thesis:_for_r0_being_real_number_st_r0_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ abs_((((h_")_(#)_(R1_/*_h))_._n)_-_0)_<_r0 let r0 be real number ; ::_thesis: ( r0 > 0 implies ex m being Element of NAT st for n being Element of NAT st m <= n holds abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 ) reconsider r = r0 as Real by XREAL_0:def_1; A19: lim h = 0 ; assume r0 > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 then consider d being Real such that A20: d > 0 and A21: for z1 being Real st z1 <> 0 & abs z1 < d holds ((abs z1) ") * (abs (R1 . z1)) < r by A6; reconsider d1 = d as real number ; consider m being Element of NAT such that A22: for n being Element of NAT st m <= n holds abs ((h . n) - 0) < d1 by A20, A19, SEQ_2:def_7; take m = m; ::_thesis: for n being Element of NAT st m <= n holds abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( m <= n implies abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 ) A23: h . n <> 0 by SEQ_1:5; rng h c= dom R1 by A5; then A24: ((abs (h . n)) ") * (abs (R1 . (h . n))) = ((abs (h . n)) ") * (abs ((R1 /* h) . n)) by FUNCT_2:108 .= (((abs h) . n) ") * (abs ((R1 /* h) . n)) by SEQ_1:12 .= (((abs h) ") . n) * (abs ((R1 /* h) . n)) by VALUED_1:10 .= ((abs (h ")) . n) * (abs ((R1 /* h) . n)) by SEQ_1:54 .= (abs ((h ") . n)) * (abs ((R1 /* h) . n)) by SEQ_1:12 .= abs (((h ") . n) * ((R1 /* h) . n)) by COMPLEX1:65 .= abs ((((h ") (#) (R1 /* h)) . n) - 0) by SEQ_1:8 ; assume m <= n ; ::_thesis: abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 then abs ((h . n) - 0) < d by A22; hence abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 by A21, A23, A24; ::_thesis: verum end; end; hence (h ") (#) (R1 /* h) is convergent by SEQ_2:def_6; ::_thesis: lim ((h ") (#) (R1 /* h)) = 0 hence lim ((h ") (#) (R1 /* h)) = 0 by A18, SEQ_2:def_7; ::_thesis: verum end; hence (J * R) * I is RestFunc by A4, FDIFF_1:def_2; ::_thesis: verum end; thus for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ::_thesis: verum proof let L be LinearOperator of (REAL-NS 1),(REAL-NS 1); ::_thesis: (J * L) * I is LinearFunc A25: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider L0 = L as Function of (REAL 1),(REAL 1) ; reconsider L1 = (J * L0) * I as PartFunc of REAL,REAL ; A26: dom (J * L0) = REAL 1 by FUNCT_2:def_1; consider r being Real such that A27: r = L1 . 1 ; A28: dom ((J * L0) * I) = REAL by FUNCT_2:def_1; A29: dom L0 = REAL 1 by FUNCT_2:def_1; for p being Real holds L1 . p = r * p proof reconsider 1p = I . 1 as VECTOR of (REAL-NS 1) by REAL_NS1:def_4; let p be Real; ::_thesis: L1 . p = r * p dom I = REAL by FUNCT_2:def_1; then L1 . p = (J * L) . (I . (p * 1)) by FUNCT_1:13; then L1 . p = (J * L) . (p * 1p) by A1, Th3; then L1 . p = J . (L . (p * 1p)) by A25, A29, FUNCT_1:13; then L1 . p = J . (p * (L . 1p)) by LOPBAN_1:def_5; then L1 . p = p * (J . (L . 1p)) by A2, Th4; then L1 . p = p * ((J * L0) . (I . 1)) by A26, FUNCT_1:12; hence L1 . p = r * p by A28, A27, FUNCT_1:12; ::_thesis: verum end; hence (J * L) * I is LinearFunc by FDIFF_1:def_3; ::_thesis: verum end; end; theorem Th6: :: PDIFF_1:6 for I being Function of REAL,(REAL 1) for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) ) proof let I be Function of REAL,(REAL 1); ::_thesis: for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) ) let J be Function of (REAL 1),REAL; ::_thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) ) ) assume that A1: I = (proj (1,1)) " and A2: J = proj (1,1) ; ::_thesis: ( ( for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ) & ( for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ) ) thus for R being RestFunc holds (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) ::_thesis: for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) proof let R be RestFunc; ::_thesis: (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) R is total by FDIFF_1:def_2; then reconsider R0 = R as Function of REAL,REAL ; A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider R1 = (I * R0) * J as PartFunc of (REAL-NS 1),(REAL-NS 1) ; 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 1) ) 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 1) ) A4: 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 A5: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1(); A6: h is convergent by NDIFF_1:def_4; A7: 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 ) A8: 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 A9: for n being Element of NAT st m <= n holds ||.((h . n) - (0. (REAL-NS 1))).|| < p by A6, A4, A8, 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 A9; then A10: ||.(h . n).|| < p by RLVECT_1:13; s . n = J . (h . n) by A5; hence abs ((s . n) - 0) < p by A2, A10, Th4; ::_thesis: verum end; hence for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p ; ::_thesis: verum end; then A11: s is convergent by SEQ_2:def_6; then A12: lim s = 0 by A7, 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 ; A13: 0 <= abs (s . n) by COMPLEX1:46; h . n <> 0. (REAL-NS 1) by NDIFF_1:6; then A14: ||.(h . n).|| <> 0 by NORMSP_0:def_5; s . n = J . (h . n) by A5; then abs (s . n) <> 0 by A2, A14, Th4; hence s . x <> 0 by A13, 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 A11, A12, FDIFF_1:def_1; A15: J * I = id REAL by A1, A2, Lm1, FUNCT_1:39; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((||.h.||_")_(#)_(R1_/*_h)).||_._n_=_(abs_((s_")_(#)_(R_/*_s)))_._n reconsider f1 = R1 as Function ; let n be Element of NAT ; ::_thesis: ||.((||.h.|| ") (#) (R1 /* h)).|| . n = (abs ((s ") (#) (R /* s))) . n A16: rng h c= the carrier of (REAL-NS 1) ; h . n in the carrier of (REAL-NS 1) ; then A17: h . n in REAL 1 by REAL_NS1:def_4; R1 is total by A3; then (R /* s) . n = R . (s . n) by FUNCT_2:115; then (R /* s) . n = R . (J . (h . n)) by A5; then (R /* s) . n = (J * I) . (R0 . (J . (h . n))) by A15, FUNCT_1:18; then (R /* s) . n = (J * I) . ((R0 * J) . (h . n)) by A17, FUNCT_2:15; then (R /* s) . n = J . (I . ((R0 * J) . (h . n))) by FUNCT_2:15; then A18: (R /* s) . n = J . ((I * (R0 * J)) . (h . n)) by A17, FUNCT_2:15; NAT = dom h by FUNCT_2:def_1; then A19: R1 . (h . n) = (f1 * h) . n by FUNCT_1:13; dom R1 = REAL 1 by FUNCT_2:def_1; then rng h c= dom R1 by A16, REAL_NS1:def_4; then R1 . (h . n) = (R1 /* h) . n by A19, FUNCT_2:def_11; then A20: (R /* s) . n = J . ((R1 /* h) . n) by A18, RELAT_1:36; A21: ||.(h . n).|| >= 0 by NORMSP_1:4; A22: s . n = J . (h . n) by A5; ||.((||.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 A21, ABSVALUE:def_1 .= ((abs (s . n)) ") * ||.((R1 /* h) . n).|| by A2, A22, Th4 .= ((abs (s . n)) ") * (abs ((R /* s) . n)) by A2, A20, Th4 .= ((abs (s . n)) ") * ((abs (R /* s)) . n) by SEQ_1:12 .= (((abs s) . n) ") * ((abs (R /* s)) . n) by SEQ_1:12 .= (((abs s) ") . n) * ((abs (R /* s)) . n) by VALUED_1:10 .= (((abs s) ") (#) (abs (R /* s))) . n by SEQ_1:8 .= ((abs (s ")) (#) (abs (R /* s))) . n by SEQ_1:54 ; hence ||.((||.h.|| ") (#) (R1 /* h)).|| . n = (abs ((s ") (#) (R /* s))) . n by SEQ_1:52; ::_thesis: verum end; then A23: ||.((||.h.|| ") (#) (R1 /* h)).|| = abs ((s ") (#) (R /* s)) by FUNCT_2:63; A24: lim ((s ") (#) (R /* s)) = 0 by FDIFF_1:def_2; A25: (s ") (#) (R /* s) is convergent by FDIFF_1:def_2; then lim (abs ((s ") (#) (R /* s))) = abs (lim ((s ") (#) (R /* s))) by SEQ_4:14; then A26: lim (abs ((s ") (#) (R /* s))) = 0 by A24, ABSVALUE:2; A27: abs ((s ") (#) (R /* s)) is convergent by A25, SEQ_4:13; A28: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ ||.((((||.h.||_")_(#)_(R1_/*_h))_._n)_-_(0._(REAL-NS_1))).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p ) assume 0 < p ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p then consider m being Element of NAT such that A29: for n being Element of NAT st m <= n holds abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0) < p by A23, A27, A26, SEQ_2:def_7; take m = m; ::_thesis: for n being Element of NAT st m <= n holds ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p ) assume m <= n ; ::_thesis: ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p then abs ((||.((||.h.|| ") (#) (R1 /* h)).|| . n) - 0) < p by A29; then A30: abs ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| < p by NORMSP_0:def_4; 0 <= ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| by NORMSP_1:4; then ||.(((||.h.|| ") (#) (R1 /* h)) . n).|| < p by A30, ABSVALUE:def_1; hence ||.((((||.h.|| ") (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < 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 1) ) by A28, NORMSP_1:def_7; ::_thesis: verum end; hence (I * R) * J is RestFunc of (REAL-NS 1),(REAL-NS 1) by A3, NDIFF_1:def_5; ::_thesis: verum end; thus for L being LinearFunc holds (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) ::_thesis: verum proof let L be LinearFunc; ::_thesis: (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) consider r being Real such that A31: for p being Real holds L . p = r * p by FDIFF_1:def_3; L is total by FDIFF_1:def_3; then reconsider L0 = L as Function of REAL,REAL ; set K = abs r; A32: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; (I * L0) * J is Function of (REAL 1),(REAL 1) ; then reconsider L1 = (I * L) * J as Function of (REAL-NS 1),(REAL-NS 1) by A32; A33: dom L1 = REAL 1 by A32, FUNCT_2:def_1; A34: dom L0 = REAL by FUNCT_2:def_1; A35: now__::_thesis:_for_x,_y_being_VECTOR_of_(REAL-NS_1)_holds_L1_._(x_+_y)_=_(L1_._x)_+_(L1_._y) let x, y be VECTOR of (REAL-NS 1); ::_thesis: L1 . (x + y) = (L1 . x) + (L1 . y) I . (L . (J . y)) = (I * L) . (J . y) by A34, FUNCT_1:13; then A36: I . (L . (J . y)) = L1 . y by A32, A33, FUNCT_1:12; L1 . (x + y) = (I * L) . (J . (x + y)) by A32, A33, FUNCT_1:12; then L1 . (x + y) = (I * L) . ((J . x) + (J . y)) by A2, Th4; then L1 . (x + y) = I . (L . ((J . x) + (J . y))) by A34, FUNCT_1:13; then L1 . (x + y) = I . (r * ((J . x) + (J . y))) by A31; then L1 . (x + y) = I . ((r * (J . x)) + (r * (J . y))) ; then L1 . (x + y) = I . ((L . (J . x)) + (r * (J . y))) by A31; then A37: L1 . (x + y) = I . ((L . (J . x)) + (L . (J . y))) by A31; I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13; then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12; hence L1 . (x + y) = (L1 . x) + (L1 . y) by A1, A36, A37, Th3; ::_thesis: verum end; now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1) for_a_being_Real_holds_L1_._(a_*_x)_=_a_*_(L1_._x) let x be VECTOR 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) = (I * L) . (J . (a * x)) by A32, A33, FUNCT_1:12; then L1 . (a * x) = (I * L) . (a * (J . x)) by A2, Th4; then L1 . (a * x) = I . (L . (a * (J . x))) by A34, FUNCT_1:13; then L1 . (a * x) = I . (r * (a * (J . x))) by A31; then L1 . (a * x) = I . (a * (r * (J . x))) ; then A38: L1 . (a * x) = I . (a * (L . (J . x))) by A31; I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13; then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12; hence L1 . (a * x) = a * (L1 . x) by A1, A38, Th3; ::_thesis: verum end; then reconsider L1 = L1 as LinearOperator of (REAL-NS 1),(REAL-NS 1) by A35, VECTSP_1:def_20, LOPBAN_1:def_5; A39: now__::_thesis:_for_x_being_VECTOR_of_(REAL-NS_1)_holds_||.(L1_._x).||_<=_(abs_r)_*_||.x.|| let x be VECTOR of (REAL-NS 1); ::_thesis: ||.(L1 . x).|| <= (abs r) * ||.x.|| I . (L . (J . x)) = (I * L) . (J . x) by A34, FUNCT_1:13; then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:12; then ||.(L1 . x).|| = abs (L . (J . x)) by A1, Th3; then ||.(L1 . x).|| = abs (r * (J . x)) by A31; then ||.(L1 . x).|| = (abs r) * (abs (J . x)) by COMPLEX1:65; hence ||.(L1 . x).|| <= (abs r) * ||.x.|| by A2, Th4; ::_thesis: verum end; 0 <= abs r by COMPLEX1:46; hence (I * L) * J is Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by A39, LOPBAN_1:def_8; ::_thesis: verum end; end; theorem Th7: :: PDIFF_1:7 for f being PartFunc of (REAL-NS 1),(REAL-NS 1) for g being PartFunc of REAL,REAL for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 ) proof let f be PartFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: for g being PartFunc of REAL,REAL for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 ) let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 ) let x be Point of (REAL-NS 1); ::_thesis: for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 ) let y be Element of REAL ; ::_thesis: ( f = <>* g & x = <*y*> & f is_differentiable_in x implies ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 ) ) set J = proj (1,1); reconsider L = diff (f,x) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def_9; A1: rng g c= dom I by Th2; reconsider L0 = ((proj (1,1)) * L) * I as LinearFunc by Th5; assume that A2: f = <>* g and A3: x = <*y*> and A4: f is_differentiable_in x ; ::_thesis: ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 ) consider NN being Neighbourhood of x such that A5: NN c= dom f and A6: ex R being RestFunc of (REAL-NS 1),(REAL-NS 1) st for y being Point of (REAL-NS 1) st y in NN holds (f /. y) - (f /. x) = ((diff (f,x)) . (y - x)) + (R /. (y - x)) by A4, NDIFF_1:def_7; consider e being Real such that A7: 0 < e and A8: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= NN by NFCONT_1:def_1; consider R being RestFunc of (REAL-NS 1),(REAL-NS 1) such that A9: for x9 being Point of (REAL-NS 1) st x9 in NN holds (f /. x9) - (f /. x) = ((diff (f,x)) . (x9 - x)) + (R /. (x9 - x)) by A6; set N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; A10: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < 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 - x).|| < e } or y in the carrier of (REAL-NS 1) ) assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: y in the carrier of (REAL-NS 1) then ex z being Point of (REAL-NS 1) st ( y = z & ||.(z - x).|| < 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 - x).|| < e } as Neighbourhood of x by A7, NFCONT_1:def_1; set N0 = { z where z is Element of REAL : abs (z - y) < e } ; A11: N c= dom f by A5, A8, XBOOLE_1:1; now__::_thesis:_for_z_being_set_holds_ (_(_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y)_<_e__}__implies_z_in_(proj_(1,1))_.:_N_)_&_(_z_in_(proj_(1,1))_.:_N_implies_z_in__{__z_where_z_is_Element_of_REAL_:_abs_(z_-_y)_<_e__}__)_) let z be set ; ::_thesis: ( ( z in { z where z is Element of REAL : abs (z - y) < e } implies z in (proj (1,1)) .: N ) & ( z in (proj (1,1)) .: N implies z in { z where z is Element of REAL : abs (z - y) < e } ) ) hereby ::_thesis: ( z in (proj (1,1)) .: N implies z in { z where z is Element of REAL : abs (z - y) < e } ) assume z in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: z in (proj (1,1)) .: N then consider y9 being Element of REAL such that A12: z = y9 and A13: abs (y9 - y) < e ; reconsider w = I . y9 as Point of (REAL-NS 1) by REAL_NS1:def_4; x = I . y by A3, Lm1; then w - x = I . (y9 - y) by Th3; then ||.(w - x).|| = abs (y9 - y) by Th3; then w in { z0 where z0 is Point of (REAL-NS 1) : ||.(z0 - x).|| < e } by A13; then (proj (1,1)) . w in (proj (1,1)) .: N by FUNCT_2:35; hence z in (proj (1,1)) .: N by A12, Lm1, FUNCT_1:35; ::_thesis: verum end; assume z in (proj (1,1)) .: N ; ::_thesis: z in { z where z is Element of REAL : abs (z - y) < e } then consider ww being set such that ww in REAL 1 and A14: ww in N and A15: z = (proj (1,1)) . ww by FUNCT_2:64; consider w being Point of (REAL-NS 1) such that A16: ww = w and A17: ||.(w - x).|| < e by A14; reconsider y9 = (proj (1,1)) . w as Element of REAL ; (proj (1,1)) . x = y by A3, Lm1; then (proj (1,1)) . (w - x) = y9 - y by Th4; then abs (y9 - y) < e by A17, Th4; hence z in { z where z is Element of REAL : abs (z - y) < e } by A15, A16; ::_thesis: verum end; then A18: { z where z is Element of REAL : abs (z - y) < e } = (proj (1,1)) .: N by TARSKI:1; dom f = (proj (1,1)) " (dom (I * g)) by A2, RELAT_1:147; then (proj (1,1)) .: (dom f) = (proj (1,1)) .: ((proj (1,1)) " (dom g)) by A1, RELAT_1:27; then A19: (proj (1,1)) .: (dom f) = dom g by Lm1, FUNCT_1:77; A20: I * (proj (1,1)) = id (REAL 1) by Lm1, FUNCT_1:39; reconsider R0 = ((proj (1,1)) * R) * I as RestFunc by Th5; A21: (proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39; N c= dom f by A5, A8, XBOOLE_1:1; then A22: { z where z is Element of REAL : abs (z - y) < e } c= dom g by A19, A18, RELAT_1:123; A23: ].(y - e),(y + e).[ c= { z where z is Element of REAL : abs (z - y) < e } proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in ].(y - e),(y + e).[ or d in { z where z is Element of REAL : abs (z - y) < e } ) assume A24: d in ].(y - e),(y + e).[ ; ::_thesis: d in { z where z is Element of REAL : abs (z - y) < e } reconsider y0 = d as Element of REAL by A24; abs (y0 - y) < e by A24, RCOMP_1:1; hence d in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: verum end; { z where z is Element of REAL : abs (z - y) < e } c= ].(y - e),(y + e).[ proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in { z where z is Element of REAL : abs (z - y) < e } or d in ].(y - e),(y + e).[ ) assume d in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: d in ].(y - e),(y + e).[ then ex r being Element of REAL st ( d = r & abs (r - y) < e ) ; hence d in ].(y - e),(y + e).[ by RCOMP_1:1; ::_thesis: verum end; then { z where z is Element of REAL : abs (z - y) < e } = ].(y - e),(y + e).[ by A23, XBOOLE_0:def_10; then A25: { z where z is Element of REAL : abs (z - y) < e } is Neighbourhood of y by A7, RCOMP_1:def_6; N c= REAL 1 by A10, REAL_NS1:def_4; then (I * (proj (1,1))) .: N = N by A20, FRECHET:13; then A26: I .: { z where z is Element of REAL : abs (z - y) < e } = N by A18, RELAT_1:126; A27: for y0 being Real st y0 in { z where z is Element of REAL : abs (z - y) < e } holds (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) proof let y0 be Real; ::_thesis: ( y0 in { z where z is Element of REAL : abs (z - y) < e } implies (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) ) reconsider y9 = I . y0 as Point of (REAL-NS 1) by REAL_NS1:def_4; R is total by NDIFF_1:def_5; then A28: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def_2; R0 is total by FDIFF_1:def_2; then dom (((proj (1,1)) * R) * I) = REAL by PARTFUN1:def_2; then y0 - y in dom (((proj (1,1)) * R) * I) ; then A29: y0 - y in dom ((proj (1,1)) * (R * I)) by RELAT_1:36; I . (y0 - y) in REAL 1 ; then I . (y0 - y) in dom R by A28, REAL_NS1:def_4; then (proj (1,1)) . (R /. (I . (y0 - y))) = (proj (1,1)) . (R . (I . (y0 - y))) by PARTFUN1:def_6; then (proj (1,1)) . (R /. (I . (y0 - y))) = (proj (1,1)) . ((R * I) . (y0 - y)) by Th2, FUNCT_1:13; then (proj (1,1)) . (R /. (I . (y0 - y))) = ((proj (1,1)) * (R * I)) . (y0 - y) by A29, FUNCT_1:12; then A30: (proj (1,1)) . (R /. (I . (y0 - y))) = R0 . (y0 - y) by RELAT_1:36; L0 is total by FDIFF_1:def_3; then dom (((proj (1,1)) * L) * I) = REAL by PARTFUN1:def_2; then y0 - y in dom (((proj (1,1)) * L) * I) ; then A31: y0 - y in dom ((proj (1,1)) * (L * I)) by RELAT_1:36; assume A32: y0 in { z where z is Element of REAL : abs (z - y) < e } ; ::_thesis: (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) then A33: I . y0 in N by A26, FUNCT_2:35; then (proj (1,1)) . (f /. (I . y0)) = (proj (1,1)) . (f . (I . y0)) by A11, PARTFUN1:def_6; then A34: (proj (1,1)) . (f /. (I . y0)) = (proj (1,1)) . ((f * I) . y0) by Th2, FUNCT_1:13; (proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1)))) by A2, RELAT_1:36; then A35: (proj (1,1)) * f = (id REAL) * (g * (proj (1,1))) by A21, RELAT_1:36; rng (g * (proj (1,1))) c= REAL ; then ((proj (1,1)) * f) * I = (g * (proj (1,1))) * I by A35, RELAT_1:53; then A36: ((proj (1,1)) * f) * I = g * (id REAL) by A21, RELAT_1:36; dom g c= REAL ; then A37: g = ((proj (1,1)) * f) * I by A36, RELAT_1:51; y0 in dom g by A22, A32; then y0 in dom ((proj (1,1)) * (f * I)) by A37, RELAT_1:36; then (proj (1,1)) . (f /. (I . y0)) = ((proj (1,1)) * (f * I)) . y0 by A34, FUNCT_1:12; then A38: (proj (1,1)) . (f /. (I . y0)) = g . y0 by A37, RELAT_1:36; A39: x = I . y by A3, Lm1; x in N by NFCONT_1:4; then (proj (1,1)) . (f /. (I . y)) = (proj (1,1)) . (f . (I . y)) by A11, A39, PARTFUN1:def_6; then A40: (proj (1,1)) . (f /. (I . y)) = (proj (1,1)) . ((f * I) . y) by Th2, FUNCT_1:13; y in { z where z is Element of REAL : abs (z - y) < e } by A25, RCOMP_1:16; then y in dom g by A22; then y in dom ((proj (1,1)) * (f * I)) by A37, RELAT_1:36; then (proj (1,1)) . (f /. (I . y)) = ((proj (1,1)) * (f * I)) . y by A40, FUNCT_1:12; then A41: (proj (1,1)) . (f /. (I . y)) = g . y by A37, RELAT_1:36; (proj (1,1)) . ((f /. y9) - (f /. x)) = (proj (1,1)) . ((L . (y9 - x)) + (R /. (y9 - x))) by A9, A8, A33; then ((proj (1,1)) . (f /. y9)) - ((proj (1,1)) . (f /. x)) = (proj (1,1)) . ((L . (y9 - x)) + (R /. (y9 - x))) by Th4; then ((proj (1,1)) . (f /. (I . y0))) - ((proj (1,1)) . (f /. (I . y))) = ((proj (1,1)) . (L . (y9 - x))) + ((proj (1,1)) . (R /. (y9 - x))) by A39, Th4; then A42: ((proj (1,1)) . (f /. (I . y0))) - ((proj (1,1)) . (f /. (I . y))) = ((proj (1,1)) . (L . (I . (y0 - y)))) + ((proj (1,1)) . (R /. (y9 - x))) by A39, Th3; (proj (1,1)) . (L . (I . (y0 - y))) = (proj (1,1)) . ((L * I) . (y0 - y)) by Th2, FUNCT_1:13; then (proj (1,1)) . (L . (I . (y0 - y))) = ((proj (1,1)) * (L * I)) . (y0 - y) by A31, FUNCT_1:12; then (proj (1,1)) . (L . (I . (y0 - y))) = L0 . (y0 - y) by RELAT_1:36; hence (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) by A39, A42, A38, A41, A30, Th3; ::_thesis: verum end; hence g is_differentiable_in y by A25, A22, FDIFF_1:def_4; ::_thesis: diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 hence diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 by A25, A22, A27, FDIFF_1:def_5; ::_thesis: verum end; theorem Th8: :: PDIFF_1:8 for f being PartFunc of (REAL-NS 1),(REAL-NS 1) for g being PartFunc of REAL,REAL for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) proof let f be PartFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: for g being PartFunc of REAL,REAL for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) let x be Point of (REAL-NS 1); ::_thesis: for y being Element of REAL st f = <>* g & x = <*y*> & g is_differentiable_in y holds ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) let y be Element of REAL ; ::_thesis: ( f = <>* g & x = <*y*> & g is_differentiable_in y implies ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) ) set J = proj (1,1); assume that A1: f = <>* g and A2: x = <*y*> and A3: g is_differentiable_in y ; ::_thesis: ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) reconsider x0 = y as Real ; consider N0 being Neighbourhood of x0 such that A4: N0 c= dom g and A5: ex L0 being LinearFunc ex R0 being RestFunc st ( diff (g,x0) = L0 . 1 & ( for y0 being Real st y0 in N0 holds (g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) ) ) by A3, FDIFF_1:def_5; consider e0 being real number such that A6: 0 < e0 and A7: N0 = ].(x0 - e0),(x0 + 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 - x).|| < e } ; A8: rng (g * (proj (1,1))) c= REAL ; consider L0 being LinearFunc, R0 being RestFunc such that A9: diff (g,x0) = L0 . 1 and A10: for y0 being Real st y0 in N0 holds (g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) by A5; reconsider R = (I * R0) * (proj (1,1)) as RestFunc of (REAL-NS 1),(REAL-NS 1) by Th6; reconsider L = (I * L0) * (proj (1,1)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by Th6; A11: dom g c= REAL ; dom f c= the carrier of (REAL-NS 1) ; then A12: dom f c= rng I by Th2, REAL_NS1:def_4; A13: (proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39; now__::_thesis:_for_z_being_set_holds_ (_(_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x).||_<_e__}__implies_z_in_I_.:_N0_)_&_(_z_in_I_.:_N0_implies_z_in__{__z_where_z_is_Point_of_(REAL-NS_1)_:_||.(z_-_x).||_<_e__}__)_) let z be set ; ::_thesis: ( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ) ) hereby ::_thesis: ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ) assume z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: z in I .: N0 then consider w being Point of (REAL-NS 1) such that A14: z = w and A15: ||.(w - x).|| < e ; reconsider y = (proj (1,1)) . w as Element of REAL ; (proj (1,1)) . x = x0 by A2, Lm1; then (proj (1,1)) . (w - x) = y - x0 by Th4; then abs (y - x0) < e by A15, Th4; then A16: y in N0 by A7, RCOMP_1:1; w in the carrier of (REAL-NS 1) ; then w in dom (proj (1,1)) by Lm1, REAL_NS1:def_4; then w = I . y by FUNCT_1:34; hence z in I .: N0 by A14, A16, FUNCT_2:35; ::_thesis: verum end; assume z in I .: N0 ; ::_thesis: z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } then consider yy being set such that A17: yy in REAL and A18: yy in N0 and A19: z = I . yy by FUNCT_2:64; reconsider y = yy as Element of REAL by A17; reconsider w = I . y as Point of (REAL-NS 1) by REAL_NS1:def_4; I . x0 = x by A2, Lm1; then A20: w - x = I . (y - x0) by Th3; abs (y - x0) < e by A7, A18, RCOMP_1:1; then ||.(w - x).|| < e by A20, Th3; hence z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A19; ::_thesis: verum end; then A21: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = I .: N0 by TARSKI:1; (proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1)))) by A1, RELAT_1:36; then (proj (1,1)) * f = (id REAL) * (g * (proj (1,1))) by A13, RELAT_1:36; then ((proj (1,1)) * f) * I = (g * (proj (1,1))) * I by A8, RELAT_1:53; then ((proj (1,1)) * f) * I = g * (id REAL) by A13, RELAT_1:36; then g = ((proj (1,1)) * f) * I by A11, RELAT_1:51; then A22: dom g = I " (dom ((proj (1,1)) * f)) by RELAT_1:147; rng f c= the carrier of (REAL-NS 1) ; then rng f c= dom (proj (1,1)) by Lm1, REAL_NS1:def_4; then I .: (dom g) = I .: (I " (dom f)) by A22, RELAT_1:27; then I .: (dom g) = dom f by A12, FUNCT_1:77; then A23: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= dom f by A4, A21, RELAT_1:123; { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < 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 - x).|| < e } or y in the carrier of (REAL-NS 1) ) assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: y in the carrier of (REAL-NS 1) then ex z being Point of (REAL-NS 1) st ( y = z & ||.(z - x).|| < e ) ; hence y in the carrier of (REAL-NS 1) ; ::_thesis: verum end; then A24: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } is Neighbourhood of x by A6, NFCONT_1:def_1; (proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39; then ((proj (1,1)) * I) .: N0 = N0 by FRECHET:13; then A25: (proj (1,1)) .: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = N0 by A21, RELAT_1:126; A26: for y being Point of (REAL-NS 1) st y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } holds (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) proof x in the carrier of (REAL-NS 1) ; then x in dom (proj (1,1)) by Lm1, REAL_NS1:def_4; then A27: I . (g . ((proj (1,1)) . x)) = I . ((g * (proj (1,1))) . x) by FUNCT_1:13; A28: x in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A24, NFCONT_1:4; then x in dom f by A23; then x in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36; then I . (g . ((proj (1,1)) . x)) = (I * (g * (proj (1,1)))) . x by A27, FUNCT_1:12; then I . (g . ((proj (1,1)) . x)) = f . x by A1, RELAT_1:36; then A29: I . (g . ((proj (1,1)) . x)) = f /. x by A23, A28, PARTFUN1:def_6; let y be Point of (REAL-NS 1); ::_thesis: ( y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } implies (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) ) assume A30: y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; ::_thesis: (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) reconsider y0 = (proj (1,1)) . y as Element of REAL ; reconsider p1 = I . (g . y0), p2 = I . (g . x0), q1 = I . (L0 . (y0 - x0)), q2 = I . (R0 . (y0 - x0)) as VECTOR of (REAL-NS 1) by REAL_NS1:def_4; A31: (proj (1,1)) . x = x0 by A2, Lm1; y in the carrier of (REAL-NS 1) ; then y in REAL 1 by REAL_NS1:def_4; then I . ((g . y0) - (g . x0)) = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by A10, A25, A30, FUNCT_2:35; then p1 - p2 = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by Th3; then p1 - p2 = q1 + q2 by Th3; then (I . (g . y0)) - (I . (g . x0)) = q1 + q2 by REAL_NS1:5; then (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (I . (L0 . (y0 - x0))) + (I . (R0 . (y0 - x0))) by A31, REAL_NS1:2; then (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (I . (L0 . ((proj (1,1)) . (y - x)))) + (I . (R0 . (y0 - x0))) by A31, Th4; then A32: (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (I . (L0 . ((proj (1,1)) . (y - x)))) + (I . (R0 . ((proj (1,1)) . (y - x)))) by A31, Th4; dom L = the carrier of (REAL-NS 1) by FUNCT_2:def_1; then y - x in dom ((I * L0) * (proj (1,1))) ; then A33: y - x in dom (I * (L0 * (proj (1,1)))) by RELAT_1:36; y - x in the carrier of (REAL-NS 1) ; then A34: y - x in dom (proj (1,1)) by Lm1, REAL_NS1:def_4; then A35: I . (R0 . ((proj (1,1)) . (y - x))) = I . ((R0 * (proj (1,1))) . (y - x)) by FUNCT_1:13; R is total by NDIFF_1:def_5; then A36: dom ((I * R0) * (proj (1,1))) = the carrier of (REAL-NS 1) by PARTFUN1:def_2; then y - x in dom ((I * R0) * (proj (1,1))) ; then y - x in dom (I * (R0 * (proj (1,1)))) by RELAT_1:36; then I . (R0 . ((proj (1,1)) . (y - x))) = (I * (R0 * (proj (1,1)))) . (y - x) by A35, FUNCT_1:12; then I . (R0 . ((proj (1,1)) . (y - x))) = ((I * R0) * (proj (1,1))) . (y - x) by RELAT_1:36; then A37: I . (R0 . ((proj (1,1)) . (y - x))) = R /. (y - x) by A36, PARTFUN1:def_6; y in the carrier of (REAL-NS 1) ; then y in dom (proj (1,1)) by Lm1, REAL_NS1:def_4; then A38: I . (g . ((proj (1,1)) . y)) = I . ((g * (proj (1,1))) . y) by FUNCT_1:13; I . (L0 . ((proj (1,1)) . (y - x))) = I . ((L0 * (proj (1,1))) . (y - x)) by A34, FUNCT_1:13; then I . (L0 . ((proj (1,1)) . (y - x))) = (I * (L0 * (proj (1,1)))) . (y - x) by A33, FUNCT_1:12; then A39: I . (L0 . ((proj (1,1)) . (y - x))) = L . (y - x) by RELAT_1:36; y in dom f by A23, A30; then y in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36; then I . (g . ((proj (1,1)) . y)) = (I * (g * (proj (1,1)))) . y by A38, FUNCT_1:12; then I . (g . ((proj (1,1)) . y)) = f . y by A1, RELAT_1:36; then I . (g . ((proj (1,1)) . y)) = f /. y by A23, A30, PARTFUN1:def_6; then (I . (g . ((proj (1,1)) . y))) - (I . (g . ((proj (1,1)) . x))) = (f /. y) - (f /. x) by A29, REAL_NS1:5; hence (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) by A32, A37, A39, REAL_NS1:2; ::_thesis: verum end; L0 is total by FDIFF_1:def_3; then A40: dom L0 = REAL by PARTFUN1:def_2; A41: L is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) by LOPBAN_1:def_9; then f is_differentiable_in x by A24, A23, A26, NDIFF_1:def_6; then diff (f,x) = (I * L0) * (proj (1,1)) by A24, A23, A41, A26, NDIFF_1:def_7; then (diff (f,x)) . <*1*> = ((I * L0) * (proj (1,1))) . (I . 1) by Lm1; then (diff (f,x)) . <*1*> = (I * L0) . ((proj (1,1)) . (I . 1)) by Lm1, FUNCT_1:13; then (diff (f,x)) . <*1*> = I . (L0 . ((proj (1,1)) . (I . 1))) by A40, FUNCT_1:13; then (diff (f,x)) . <*1*> = I . (L0 . 1) by Lm1, FUNCT_1:35; hence ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) by A24, A23, A9, A41, A26, Lm1, NDIFF_1:def_6; ::_thesis: verum end; theorem :: PDIFF_1:9 for f being PartFunc of (REAL-NS 1),(REAL-NS 1) for g being PartFunc of REAL,REAL for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> holds ( f is_differentiable_in x iff g is_differentiable_in y ) by Th7, Th8; theorem Th10: :: PDIFF_1:10 for f being PartFunc of (REAL-NS 1),(REAL-NS 1) for g being PartFunc of REAL,REAL for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds (diff (f,x)) . <*1*> = <*(diff (g,y))*> proof let f be PartFunc of (REAL-NS 1),(REAL-NS 1); ::_thesis: for g being PartFunc of REAL,REAL for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds (diff (f,x)) . <*1*> = <*(diff (g,y))*> let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of (REAL-NS 1) for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds (diff (f,x)) . <*1*> = <*(diff (g,y))*> let x be Point of (REAL-NS 1); ::_thesis: for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds (diff (f,x)) . <*1*> = <*(diff (g,y))*> let y be Element of REAL ; ::_thesis: ( f = <>* g & x = <*y*> & f is_differentiable_in x implies (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) assume that A1: f = <>* g and A2: x = <*y*> and A3: f is_differentiable_in x ; ::_thesis: (diff (f,x)) . <*1*> = <*(diff (g,y))*> g is_differentiable_in y by A1, A2, A3, Th7; hence (diff (f,x)) . <*1*> = <*(diff (g,y))*> by A1, A2, Th8; ::_thesis: verum end; begin definition let n, m be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL-NS m),(REAL-NS n); let x be Point of (REAL-NS m); predf is_partial_differentiable_in x,i means :Def9: :: PDIFF_1:def 9 f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x; end; :: deftheorem Def9 defines is_partial_differentiable_in PDIFF_1:def_9_:_ for n, m being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds ( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x ); definition let m, n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL-NS m),(REAL-NS n); let x be Point of (REAL-NS m); func partdiff (f,x,i) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) equals :: PDIFF_1:def 10 diff ((f * (reproj (i,x))),((Proj (i,m)) . x)); coherence diff ((f * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ; end; :: deftheorem defines partdiff PDIFF_1:def_10_:_ for m, n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((Proj (i,m)) . x)); definition let n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL n),REAL; let x be Element of REAL n; predf is_partial_differentiable_in x,i means :Def11: :: PDIFF_1:def 11 f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x; end; :: deftheorem Def11 defines is_partial_differentiable_in PDIFF_1:def_11_:_ for n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL n),REAL for x being Element of REAL n holds ( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x ); definition let n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL n),REAL; let x be Element of REAL n; func partdiff (f,x,i) -> real number equals :: PDIFF_1:def 12 diff ((f * (reproj (i,x))),((proj (i,n)) . x)); coherence diff ((f * (reproj (i,x))),((proj (i,n)) . x)) is real number ; end; :: deftheorem defines partdiff PDIFF_1:def_12_:_ for n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL n),REAL for x being Element of REAL n holds partdiff (f,x,i) = diff ((f * (reproj (i,x))),((proj (i,n)) . x)); definition let n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL n),REAL; let x be Element of REAL n; :: original: partdiff redefine func partdiff (f,x,i) -> Real; coherence partdiff (f,x,i) is Real ; end; theorem Th11: :: PDIFF_1:11 for n being non empty Element of NAT for i being Element of NAT holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n)) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n)) let i be Element of NAT ; ::_thesis: Proj (i,n) = ((proj (1,1)) ") * (proj (i,n)) reconsider h = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2; A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; A2: now__::_thesis:_for_x_being_Element_of_REAL_n_holds_ (_(h_*_(proj_(i,n)))_._x_=_<*((proj_(i,n))_._x)*>_&_(Proj_(i,n))_._x_=_(h_*_(proj_(i,n)))_._x_) let x be Element of REAL n; ::_thesis: ( (h * (proj (i,n))) . x = <*((proj (i,n)) . x)*> & (Proj (i,n)) . x = (h * (proj (i,n))) . x ) reconsider z = x as Point of (REAL-NS n) by REAL_NS1:def_4; A3: (h * (proj (i,n))) . x = h . ((proj (i,n)) . x) by FUNCT_2:15; hence (h * (proj (i,n))) . x = <*((proj (i,n)) . x)*> by Lm1; ::_thesis: (Proj (i,n)) . x = (h * (proj (i,n))) . x (Proj (i,n)) . x = (Proj (i,n)) . z ; then (Proj (i,n)) . x = <*((proj (i,n)) . x)*> by Def4; hence (Proj (i,n)) . x = (h * (proj (i,n))) . x by A3, Lm1; ::_thesis: verum end; the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; hence Proj (i,n) = ((proj (1,1)) ") * (proj (i,n)) by A1, A2, FUNCT_2:63; ::_thesis: verum end; theorem Th12: :: PDIFF_1:12 for n being non empty Element of NAT for i being Element of NAT for x being Point of (REAL-NS n) for y being Element of REAL n st x = y holds (reproj (i,y)) * (proj (1,1)) = reproj (i,x) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for x being Point of (REAL-NS n) for y being Element of REAL n st x = y holds (reproj (i,y)) * (proj (1,1)) = reproj (i,x) let i be Element of NAT ; ::_thesis: for x being Point of (REAL-NS n) for y being Element of REAL n st x = y holds (reproj (i,y)) * (proj (1,1)) = reproj (i,x) let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st x = y holds (reproj (i,y)) * (proj (1,1)) = reproj (i,x) let y be Element of REAL n; ::_thesis: ( x = y implies (reproj (i,y)) * (proj (1,1)) = reproj (i,x) ) reconsider k = proj (1,1) as Function of (REAL 1),REAL ; A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; assume A2: x = y ; ::_thesis: (reproj (i,y)) * (proj (1,1)) = reproj (i,x) A3: now__::_thesis:_for_s_being_Element_of_REAL_1_holds_(reproj_(i,x))_._s_=_((reproj_(i,y))_*_k)_._s let s be Element of REAL 1; ::_thesis: (reproj (i,x)) . s = ((reproj (i,y)) * k) . s reconsider r = s as Point of (REAL-NS 1) by REAL_NS1:def_4; A4: ((reproj (i,y)) * k) . s = (reproj (i,y)) . (k . s) by FUNCT_2:15; ex q being Element of REAL ex z being Element of REAL n st ( r = <*q*> & z = x & (reproj (i,x)) . r = (reproj (i,z)) . q ) by Def6; hence (reproj (i,x)) . s = ((reproj (i,y)) * k) . s by A2, A4, Lm1; ::_thesis: verum end; the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; hence (reproj (i,y)) * (proj (1,1)) = reproj (i,x) by A1, A3, FUNCT_2:63; ::_thesis: verum end; theorem Th13: :: PDIFF_1:13 for n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds <>* (g * (reproj (i,y))) = f * (reproj (i,x)) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds <>* (g * (reproj (i,y))) = f * (reproj (i,x)) let i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds <>* (g * (reproj (i,y))) = f * (reproj (i,x)) let f be PartFunc of (REAL-NS n),(REAL-NS 1); ::_thesis: for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds <>* (g * (reproj (i,y))) = f * (reproj (i,x)) let g be PartFunc of (REAL n),REAL; ::_thesis: for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds <>* (g * (reproj (i,y))) = f * (reproj (i,x)) let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st f = <>* g & x = y holds <>* (g * (reproj (i,y))) = f * (reproj (i,x)) let y be Element of REAL n; ::_thesis: ( f = <>* g & x = y implies <>* (g * (reproj (i,y))) = f * (reproj (i,x)) ) reconsider h = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2; assume that A1: f = <>* g and A2: x = y ; ::_thesis: <>* (g * (reproj (i,y))) = f * (reproj (i,x)) (reproj (i,y)) * (proj (1,1)) = reproj (i,x) by A2, Th12; then ((h * g) * (reproj (i,y))) * (proj (1,1)) = f * (reproj (i,x)) by A1, RELAT_1:36; hence <>* (g * (reproj (i,y))) = f * (reproj (i,x)) by RELAT_1:36; ::_thesis: verum end; theorem Th14: :: PDIFF_1:14 for n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) let i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) let f be PartFunc of (REAL-NS n),(REAL-NS 1); ::_thesis: for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) let g be PartFunc of (REAL n),REAL; ::_thesis: for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y holds ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st f = <>* g & x = y holds ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) let y be Element of REAL n; ::_thesis: ( f = <>* g & x = y implies ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) ) assume that A1: f = <>* g and A2: x = y ; ::_thesis: ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) A3: <*((proj (i,n)) . y)*> = (Proj (i,n)) . x by A2, Def4; A4: f * (reproj (i,x)) = <>* (g * (reproj (i,y))) by A1, A2, Th13; hereby ::_thesis: ( g is_partial_differentiable_in y,i implies f is_partial_differentiable_in x,i ) assume f is_partial_differentiable_in x,i ; ::_thesis: g is_partial_differentiable_in y,i then f * (reproj (i,x)) is_differentiable_in (Proj (i,n)) . x by Def9; then g * (reproj (i,y)) is_differentiable_in (proj (i,n)) . y by A4, A3, Th7; hence g is_partial_differentiable_in y,i by Def11; ::_thesis: verum end; assume g is_partial_differentiable_in y,i ; ::_thesis: f is_partial_differentiable_in x,i then g * (reproj (i,y)) is_differentiable_in (proj (i,n)) . y by Def11; then f * (reproj (i,x)) is_differentiable_in (Proj (i,n)) . x by A4, A3, Th8; hence f is_partial_differentiable_in x,i by Def9; ::_thesis: verum end; theorem Th15: :: PDIFF_1:15 for n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> let i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1) for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> let f be PartFunc of (REAL-NS n),(REAL-NS 1); ::_thesis: for g being PartFunc of (REAL n),REAL for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> let g be PartFunc of (REAL n),REAL; ::_thesis: for x being Point of (REAL-NS n) for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> let x be Point of (REAL-NS n); ::_thesis: for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> let y be Element of REAL n; ::_thesis: ( f = <>* g & x = y & f is_partial_differentiable_in x,i implies (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> ) assume that A1: f = <>* g and A2: x = y and A3: f is_partial_differentiable_in x,i ; ::_thesis: (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> A4: f * (reproj (i,x)) is_differentiable_in (Proj (i,n)) . x by A3, Def9; A5: <*((proj (i,n)) . y)*> = (Proj (i,n)) . x by A2, Def4; f * (reproj (i,x)) = <>* (g * (reproj (i,y))) by A1, A2, Th13; hence (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> by A4, A5, Th10; ::_thesis: verum end; definition let m, n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL m),(REAL n); let x be Element of REAL m; predf is_partial_differentiable_in x,i means :Def13: :: PDIFF_1:def 13 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & g is_partial_differentiable_in y,i ); end; :: deftheorem Def13 defines is_partial_differentiable_in PDIFF_1:def_13_:_ for m, n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m holds ( f is_partial_differentiable_in x,i iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & g is_partial_differentiable_in y,i ) ); definition let m, n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL m),(REAL n); let x be Element of REAL m; assume A1: f is_partial_differentiable_in x,i ; func partdiff (f,x,i) -> Element of REAL n means :Def14: :: PDIFF_1:def 14 ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & it = (partdiff (g,y,i)) . <*1*> ); correctness existence ex b1 being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ); uniqueness for b1, b2 being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b2 = (partdiff (g,y,i)) . <*1*> ) holds b1 = b2; proof A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; consider g being PartFunc of (REAL-NS m),(REAL-NS n), y being Point of (REAL-NS m) such that A3: f = g and A4: x = y and g is_partial_differentiable_in y,i by A1, Def13; the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then partdiff (g,y,i) is Function of (REAL 1),(REAL n) by A2, LOPBAN_1:def_9; then (partdiff (g,y,i)) . <*1*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5; hence ( ex b1 being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ( for b1, b2 being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b2 = (partdiff (g,y,i)) . <*1*> ) holds b1 = b2 ) ) by A3, A4; ::_thesis: verum end; end; :: deftheorem Def14 defines partdiff PDIFF_1:def_14_:_ for m, n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL m),(REAL n) for x being Element of REAL m st f is_partial_differentiable_in x,i holds for b6 being Element of REAL n holds ( b6 = partdiff (f,x,i) iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st ( f = g & x = y & b6 = (partdiff (g,y,i)) . <*1*> ) ); theorem Th16: :: PDIFF_1:16 for i being Element of NAT for m, n being non empty Element of NAT for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) proof let i be Element of NAT ; ::_thesis: for m, n being non empty Element of NAT for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y holds ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) let y be Element of REAL m; ::_thesis: ( F = G & x = y implies ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) ) assume that A1: F = G and A2: x = y ; ::_thesis: ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) now__::_thesis:_(_G_is_partial_differentiable_in_y,i_implies_F_is_partial_differentiable_in_x,i_) assume G is_partial_differentiable_in y,i ; ::_thesis: F is_partial_differentiable_in x,i then ex f1 being PartFunc of (REAL-NS m),(REAL-NS n) ex y1 being Point of (REAL-NS m) st ( G = f1 & y = y1 & f1 is_partial_differentiable_in y1,i ) by Def13; hence F is_partial_differentiable_in x,i by A1, A2; ::_thesis: verum end; hence ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) by A1, A2, Def13; ::_thesis: verum end; theorem Th17: :: PDIFF_1:17 for i being Element of NAT for m, n being non empty Element of NAT for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) proof let i be Element of NAT ; ::_thesis: for m, n being non empty Element of NAT for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) let y be Element of REAL m; ::_thesis: ( F = G & x = y & F is_partial_differentiable_in x,i implies (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) ) assume that A1: F = G and A2: x = y and A3: F is_partial_differentiable_in x,i ; ::_thesis: (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) A4: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then partdiff (F,x,i) is Function of (REAL 1),(REAL n) by A4, LOPBAN_1:def_9; then A5: (partdiff (F,x,i)) . <*1*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5; G is_partial_differentiable_in y,i by A1, A2, A3, Th16; hence (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) by A1, A2, A5, Def14; ::_thesis: verum end; theorem :: PDIFF_1:18 for n being non empty Element of NAT for i being Element of NAT for g being PartFunc of (REAL n),REAL for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for g being PartFunc of (REAL n),REAL for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) let i be Element of NAT ; ::_thesis: for g being PartFunc of (REAL n),REAL for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) let g be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) let y be Element of REAL n; ::_thesis: for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g holds ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) let g1 be PartFunc of (REAL n),(REAL 1); ::_thesis: ( g1 = <>* g implies ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) ) assume A1: g1 = <>* g ; ::_thesis: ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) reconsider y9 = y as Point of (REAL-NS n) by REAL_NS1:def_4; the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4; ( h is_partial_differentiable_in y9,i iff g1 is_partial_differentiable_in y,i ) by Th16; hence ( g1 is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i ) by A1, Th14; ::_thesis: verum end; theorem :: PDIFF_1:19 for n being non empty Element of NAT for i being Element of NAT for g being PartFunc of (REAL n),REAL for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds partdiff (g1,y,i) = <*(partdiff (g,y,i))*> proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for g being PartFunc of (REAL n),REAL for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds partdiff (g1,y,i) = <*(partdiff (g,y,i))*> let i be Element of NAT ; ::_thesis: for g being PartFunc of (REAL n),REAL for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds partdiff (g1,y,i) = <*(partdiff (g,y,i))*> let g be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds partdiff (g1,y,i) = <*(partdiff (g,y,i))*> let y be Element of REAL n; ::_thesis: for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds partdiff (g1,y,i) = <*(partdiff (g,y,i))*> let g1 be PartFunc of (REAL n),(REAL 1); ::_thesis: ( g1 = <>* g & g1 is_partial_differentiable_in y,i implies partdiff (g1,y,i) = <*(partdiff (g,y,i))*> ) assume that A1: g1 = <>* g and A2: g1 is_partial_differentiable_in y,i ; ::_thesis: partdiff (g1,y,i) = <*(partdiff (g,y,i))*> reconsider y9 = y as Point of (REAL-NS n) by REAL_NS1:def_4; the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider h = g1 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4; A3: h is_partial_differentiable_in y9,i by A2, Th16; then (partdiff (h,y9,i)) . <*1*> = partdiff (g1,y,i) by Th17; hence partdiff (g1,y,i) = <*(partdiff (g,y,i))*> by A1, A3, Th15; ::_thesis: verum end; begin definition let m, n be non empty Element of NAT ; let i, j be Element of NAT ; let f be PartFunc of (REAL-NS m),(REAL-NS n); let x be Point of (REAL-NS m); predf is_partial_differentiable_in x,i,j means :Def15: :: PDIFF_1:def 15 ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x; end; :: deftheorem Def15 defines is_partial_differentiable_in PDIFF_1:def_15_:_ for m, n being non empty Element of NAT for i, j being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds ( f is_partial_differentiable_in x,i,j iff ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x ); definition let m, n be non empty Element of NAT ; let i, j be Element of NAT ; let f be PartFunc of (REAL-NS m),(REAL-NS n); let x be Point of (REAL-NS m); func partdiff (f,x,i,j) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) equals :: PDIFF_1:def 16 diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x)); correctness coherence diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))); ; end; :: deftheorem defines partdiff PDIFF_1:def_16_:_ for m, n being non empty Element of NAT for i, j being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds partdiff (f,x,i,j) = diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x)); definition let m, n be non empty Element of NAT ; let i, j be Element of NAT ; let h be PartFunc of (REAL m),(REAL n); let z be Element of REAL m; predh is_partial_differentiable_in z,i,j means :Def17: :: PDIFF_1:def 17 ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z; end; :: deftheorem Def17 defines is_partial_differentiable_in PDIFF_1:def_17_:_ for m, n being non empty Element of NAT for i, j being Element of NAT for h being PartFunc of (REAL m),(REAL n) for z being Element of REAL m holds ( h is_partial_differentiable_in z,i,j iff ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z ); definition let m, n be non empty Element of NAT ; let i, j be Element of NAT ; let h be PartFunc of (REAL m),(REAL n); let z be Element of REAL m; func partdiff (h,z,i,j) -> real number equals :: PDIFF_1:def 18 diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z)); correctness coherence diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z)) is real number ; ; end; :: deftheorem defines partdiff PDIFF_1:def_18_:_ for m, n being non empty Element of NAT for i, j being Element of NAT for h being PartFunc of (REAL m),(REAL n) for z being Element of REAL m holds partdiff (h,z,i,j) = diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z)); theorem Th20: :: PDIFF_1:20 for m, n being non empty Element of NAT for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_differentiable_in x iff G is_differentiable_in y ) proof let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_differentiable_in x iff G is_differentiable_in y ) let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_differentiable_in x iff G is_differentiable_in y ) let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y holds ( F is_differentiable_in x iff G is_differentiable_in y ) let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y holds ( F is_differentiable_in x iff G is_differentiable_in y ) let y be Element of REAL m; ::_thesis: ( F = G & x = y implies ( F is_differentiable_in x iff G is_differentiable_in y ) ) assume that A1: F = G and A2: x = y ; ::_thesis: ( F is_differentiable_in x iff G is_differentiable_in y ) now__::_thesis:_(_G_is_differentiable_in_y_implies_F_is_differentiable_in_x_) assume G is_differentiable_in y ; ::_thesis: F is_differentiable_in x then ex f1 being PartFunc of (REAL-NS m),(REAL-NS n) ex y1 being Point of (REAL-NS m) st ( G = f1 & y = y1 & f1 is_differentiable_in y1 ) by Def7; hence F is_differentiable_in x by A1, A2; ::_thesis: verum end; hence ( F is_differentiable_in x iff G is_differentiable_in y ) by A1, A2, Def7; ::_thesis: verum end; theorem :: PDIFF_1:21 for m, n being non empty Element of NAT for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds diff (F,x) = diff (G,y) proof let m, n be non empty Element of NAT ; ::_thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n) for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds diff (F,x) = diff (G,y) let F be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for G being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds diff (F,x) = diff (G,y) let G be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m) for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds diff (F,x) = diff (G,y) let x be Point of (REAL-NS m); ::_thesis: for y being Element of REAL m st F = G & x = y & F is_differentiable_in x holds diff (F,x) = diff (G,y) let y be Element of REAL m; ::_thesis: ( F = G & x = y & F is_differentiable_in x implies diff (F,x) = diff (G,y) ) assume that A1: F = G and A2: x = y and A3: F is_differentiable_in x ; ::_thesis: diff (F,x) = diff (G,y) A4: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4; then A5: diff (F,x) is Function of (REAL m),(REAL n) by A4, LOPBAN_1:def_9; G is_differentiable_in y by A1, A2, A3, Th20; hence diff (F,x) = diff (G,y) by A1, A2, A5, Def8; ::_thesis: verum end; theorem Th22: :: PDIFF_1:22 for m, n being non empty Element of NAT for j, i being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) proof let m, n be non empty Element of NAT ; ::_thesis: for j, i being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) let j, i be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) let h be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) let x be Point of (REAL-NS m); ::_thesis: for z being Element of REAL m st f = h & x = z holds ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) let z be Element of REAL m; ::_thesis: ( f = h & x = z implies ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) ) reconsider h1 = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2; assume that A1: f = h and A2: x = z ; ::_thesis: ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) <>* (((proj (j,n)) * h) * (reproj (i,z))) = (h1 * ((proj (j,n)) * (h * (reproj (i,z))))) * (proj (1,1)) by RELAT_1:36 .= ((h1 * (proj (j,n))) * (h * (reproj (i,z)))) * (proj (1,1)) by RELAT_1:36 .= (h1 * (proj (j,n))) * ((h * (reproj (i,z))) * (proj (1,1))) by RELAT_1:36 .= (h1 * (proj (j,n))) * (h * ((reproj (i,z)) * (proj (1,1)))) by RELAT_1:36 .= (Proj (j,n)) * (h * ((reproj (i,z)) * (proj (1,1)))) by Th11 .= (Proj (j,n)) * (h * (reproj (i,x))) by A2, Th12 ; hence ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, RELAT_1:36; ::_thesis: verum end; theorem :: PDIFF_1:23 for n, m being non empty Element of NAT for i, j being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) proof let n, m be non empty Element of NAT ; ::_thesis: for i, j being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) let i, j be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) let h be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z holds ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) let x be Point of (REAL-NS m); ::_thesis: for z being Element of REAL m st f = h & x = z holds ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) let z be Element of REAL m; ::_thesis: ( f = h & x = z implies ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) ) assume that A1: f = h and A2: x = z ; ::_thesis: ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) A3: (Proj (i,m)) . x = <*((proj (i,m)) . z)*> by A2, Def4; A4: ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, A2, Th22; hereby ::_thesis: ( h is_partial_differentiable_in z,i,j implies f is_partial_differentiable_in x,i,j ) assume f is_partial_differentiable_in x,i,j ; ::_thesis: h is_partial_differentiable_in z,i,j then ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by Def15; then ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z by A4, A3, Th7; hence h is_partial_differentiable_in z,i,j by Def17; ::_thesis: verum end; assume h is_partial_differentiable_in z,i,j ; ::_thesis: f is_partial_differentiable_in x,i,j then ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z by Def17; then ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A4, A3, Th8; hence f is_partial_differentiable_in x,i,j by Def15; ::_thesis: verum end; theorem :: PDIFF_1:24 for n, m being non empty Element of NAT for i, j being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> proof let n, m be non empty Element of NAT ; ::_thesis: for i, j being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> let i, j be Element of NAT ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for h being PartFunc of (REAL m),(REAL n) for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> let h be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Point of (REAL-NS m) for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> let x be Point of (REAL-NS m); ::_thesis: for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> let z be Element of REAL m; ::_thesis: ( f = h & x = z & f is_partial_differentiable_in x,i,j implies (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> ) assume that A1: f = h and A2: x = z and A3: f is_partial_differentiable_in x,i,j ; ::_thesis: (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> A4: (Proj (i,m)) . x = <*((proj (i,m)) . z)*> by A2, Def4; A5: ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A3, Def15; ((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, A2, Th22; hence (partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*> by A4, A5, Th10; ::_thesis: verum end; definition let m, n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL-NS m),(REAL-NS n); let X be set ; predf is_partial_differentiable_on X,i means :Def19: :: PDIFF_1:def 19 ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds f | X is_partial_differentiable_in x,i ) ); end; :: deftheorem Def19 defines is_partial_differentiable_on PDIFF_1:def_19_:_ for m, n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for X being set holds ( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (REAL-NS m) st x in X holds f | X is_partial_differentiable_in x,i ) ) ); theorem Th25: :: PDIFF_1:25 for n, m being non empty Element of NAT for i being Element of NAT for X being set for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds X is Subset of (REAL-NS m) proof let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT for X being set for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds X is Subset of (REAL-NS m) let i be Element of NAT ; ::_thesis: for X being set for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds X is Subset of (REAL-NS m) let X be set ; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds X is Subset of (REAL-NS m) let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f is_partial_differentiable_on X,i implies X is Subset of (REAL-NS m) ) assume f is_partial_differentiable_on X,i ; ::_thesis: X is Subset of (REAL-NS m) then X c= dom f by Def19; hence X is Subset of (REAL-NS m) by XBOOLE_1:1; ::_thesis: verum end; definition let m, n be non empty Element of NAT ; let i be Element of NAT ; let f be PartFunc of (REAL-NS m),(REAL-NS n); let X be set ; assume A1: f is_partial_differentiable_on X,i ; funcf `partial| (X,i) -> PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) means :: PDIFF_1:def 20 ( dom it = X & ( for x being Point of (REAL-NS m) st x in X holds it /. x = partdiff (f,x,i) ) ); existence ex b1 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st ( dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds b1 /. x = partdiff (f,x,i) ) ) proof deffunc H1( Element of (REAL-NS m)) -> Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) = partdiff (f,\$1,i); defpred S1[ Element of (REAL-NS m)] means \$1 in X; consider F being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) such that A2: ( ( for x being Point of (REAL-NS m) holds ( x in dom F iff S1[x] ) ) & ( for x being Point of (REAL-NS m) st x in dom F holds F . x = H1(x) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds F /. x = partdiff (f,x,i) ) ) now__::_thesis:_for_y_being_set_st_y_in_X_holds_ y_in_dom_F A3: X is Subset of (REAL-NS m) by A1, Th25; let y be set ; ::_thesis: ( y in X implies y in dom F ) assume y in X ; ::_thesis: y in dom F hence y in dom F by A2, A3; ::_thesis: verum end; then A4: X c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in X by A2; then dom F c= X by TARSKI:def_3; hence dom F = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Point of (REAL-NS m) st x in X holds F /. x = partdiff (f,x,i) hereby ::_thesis: verum let x be Point of (REAL-NS m); ::_thesis: ( x in X implies F /. x = partdiff (f,x,i) ) assume x in X ; ::_thesis: F /. x = partdiff (f,x,i) then A5: x in dom F by A2; then F . x = partdiff (f,x,i) by A2; hence F /. x = partdiff (f,x,i) by A5, PARTFUN1:def_6; ::_thesis: verum end; end; uniqueness for b1, b2 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds b1 /. x = partdiff (f,x,i) ) & dom b2 = X & ( for x being Point of (REAL-NS m) st x in X holds b2 /. x = partdiff (f,x,i) ) holds b1 = b2 proof let F, G be PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))); ::_thesis: ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds F /. x = partdiff (f,x,i) ) & dom G = X & ( for x being Point of (REAL-NS m) st x in X holds G /. x = partdiff (f,x,i) ) implies F = G ) assume that A6: dom F = X and A7: for x being Point of (REAL-NS m) st x in X holds F /. x = partdiff (f,x,i) and A8: dom G = X and A9: for x being Point of (REAL-NS m) st x in X holds G /. x = partdiff (f,x,i) ; ::_thesis: F = G now__::_thesis:_for_x_being_Point_of_(REAL-NS_m)_st_x_in_dom_F_holds_ F_/._x_=_G_/._x let x be Point of (REAL-NS m); ::_thesis: ( x in dom F implies F /. x = G /. x ) assume A10: x in dom F ; ::_thesis: F /. x = G /. x then F /. x = partdiff (f,x,i) by A6, A7; hence F /. x = G /. x by A6, A9, A10; ::_thesis: verum end; hence F = G by A6, A8, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem defines `partial| PDIFF_1:def_20_:_ for m, n being non empty Element of NAT for i being Element of NAT for f being PartFunc of (REAL-NS m),(REAL-NS n) for X being set st f is_partial_differentiable_on X,i holds for b6 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) holds ( b6 = f `partial| (X,i) iff ( dom b6 = X & ( for x being Point of (REAL-NS m) st x in X holds b6 /. x = partdiff (f,x,i) ) ) ); theorem Th26: :: PDIFF_1:26 for n, m being non empty Element of NAT for i being Element of NAT for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) ) proof let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) ) let i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) ) let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) holds ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) ) let x be Point of (REAL-NS m); ::_thesis: ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) ) A1: dom (reproj (i,x)) = the carrier of (REAL-NS 1) by FUNCT_2:def_1; A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1; for s being Element of (REAL-NS 1) holds ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) ) proof let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) ) ( s in dom ((f1 + f2) * (reproj (i,x))) iff (reproj (i,x)) . s in (dom f1) /\ (dom f2) ) by A2, A1, FUNCT_1:11; then ( s in dom ((f1 + f2) * (reproj (i,x))) iff ( (reproj (i,x)) . s in dom f1 & (reproj (i,x)) . s in dom f2 ) ) by XBOOLE_0:def_4; then ( s in dom ((f1 + f2) * (reproj (i,x))) iff ( s in dom (f1 * (reproj (i,x))) & s in dom (f2 * (reproj (i,x))) ) ) by A1, FUNCT_1:11; then ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in (dom (f1 * (reproj (i,x)))) /\ (dom (f2 * (reproj (i,x)))) ) by XBOOLE_0:def_4; hence ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) ) by VFUNCT_1:def_1; ::_thesis: verum end; then for s being set holds ( s in dom ((f1 + f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) ) ; then A3: dom ((f1 + f2) * (reproj (i,x))) = dom ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) by TARSKI:1; A4: for z being Element of (REAL-NS 1) st z in dom ((f1 + f2) * (reproj (i,x))) holds ((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z proof let z be Element of (REAL-NS 1); ::_thesis: ( z in dom ((f1 + f2) * (reproj (i,x))) implies ((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z ) assume A5: z in dom ((f1 + f2) * (reproj (i,x))) ; ::_thesis: ((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z then A6: (reproj (i,x)) . z in dom (f1 + f2) by FUNCT_1:11; A7: (reproj (i,x)) . z in (dom f1) /\ (dom f2) by A2, A5, FUNCT_1:11; then A8: (reproj (i,x)) . z in dom f1 by XBOOLE_0:def_4; then A9: z in dom (f1 * (reproj (i,x))) by A1, FUNCT_1:11; A10: (reproj (i,x)) . z in dom f2 by A7, XBOOLE_0:def_4; then A11: z in dom (f2 * (reproj (i,x))) by A1, FUNCT_1:11; A12: f2 /. ((reproj (i,x)) . z) = f2 . ((reproj (i,x)) . z) by A10, PARTFUN1:def_6 .= (f2 * (reproj (i,x))) . z by A11, FUNCT_1:12 .= (f2 * (reproj (i,x))) /. z by A11, PARTFUN1:def_6 ; A13: f1 /. ((reproj (i,x)) . z) = f1 . ((reproj (i,x)) . z) by A8, PARTFUN1:def_6 .= (f1 * (reproj (i,x))) . z by A9, FUNCT_1:12 .= (f1 * (reproj (i,x))) /. z by A9, PARTFUN1:def_6 ; ((f1 + f2) * (reproj (i,x))) . z = (f1 + f2) . ((reproj (i,x)) . z) by A5, FUNCT_1:12 .= (f1 + f2) /. ((reproj (i,x)) . z) by A6, PARTFUN1:def_6 .= (f1 /. ((reproj (i,x)) . z)) + (f2 /. ((reproj (i,x)) . z)) by A6, VFUNCT_1:def_1 .= ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) /. z by A3, A5, A13, A12, VFUNCT_1:def_1 ; hence ((f1 + f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))) . z by A3, A5, PARTFUN1:def_6; ::_thesis: verum end; A14: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2; for s being Element of (REAL-NS 1) holds ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) ) proof let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) ) ( s in dom ((f1 - f2) * (reproj (i,x))) iff (reproj (i,x)) . s in (dom f1) /\ (dom f2) ) by A14, A1, FUNCT_1:11; then ( s in dom ((f1 - f2) * (reproj (i,x))) iff ( (reproj (i,x)) . s in dom f1 & (reproj (i,x)) . s in dom f2 ) ) by XBOOLE_0:def_4; then ( s in dom ((f1 - f2) * (reproj (i,x))) iff ( s in dom (f1 * (reproj (i,x))) & s in dom (f2 * (reproj (i,x))) ) ) by A1, FUNCT_1:11; then ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in (dom (f1 * (reproj (i,x)))) /\ (dom (f2 * (reproj (i,x)))) ) by XBOOLE_0:def_4; hence ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) ) by VFUNCT_1:def_2; ::_thesis: verum end; then for s being set holds ( s in dom ((f1 - f2) * (reproj (i,x))) iff s in dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) ) ; then A15: dom ((f1 - f2) * (reproj (i,x))) = dom ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) by TARSKI:1; for z being Element of (REAL-NS 1) st z in dom ((f1 - f2) * (reproj (i,x))) holds ((f1 - f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z proof let z be Element of (REAL-NS 1); ::_thesis: ( z in dom ((f1 - f2) * (reproj (i,x))) implies ((f1 - f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z ) assume A16: z in dom ((f1 - f2) * (reproj (i,x))) ; ::_thesis: ((f1 - f2) * (reproj (i,x))) . z = ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z then A17: (reproj (i,x)) . z in dom (f1 - f2) by FUNCT_1:11; A18: (reproj (i,x)) . z in (dom f1) /\ (dom f2) by A14, A16, FUNCT_1:11; then A19: (reproj (i,x)) . z in dom f1 by XBOOLE_0:def_4; then A20: z in dom (f1 * (reproj (i,x))) by A1, FUNCT_1:11; A21: (reproj (i,x)) . z in dom f2 by A18, XBOOLE_0:def_4; then A22: z in dom (f2 * (reproj (i,x))) by A1, FUNCT_1:11; A23: f2 /. ((reproj (i,x)) . z) = f2 . ((reproj (i,x)) . z) by A21, PARTFUN1:def_6 .= (f2 * (reproj (i,x))) . z by A22, FUNCT_1:12 .= (f2 * (reproj (i,x))) /. z by A22, PARTFUN1:def_6 ; A24: f1 /. ((reproj (i,x)) . z) = f1 . ((reproj (i,x)) . z) by A19, PARTFUN1:def_6 .= (f1 * (reproj (i,x))) . z by A20, FUNCT_1:12 .= (f1 * (reproj (i,x))) /. z by A20, PARTFUN1:def_6 ; thus ((f1 - f2) * (reproj (i,x))) . z = (f1 - f2) . ((reproj (i,x)) . z) by A16, FUNCT_1:12 .= (f1 - f2) /. ((reproj (i,x)) . z) by A17, PARTFUN1:def_6 .= (f1 /. ((reproj (i,x)) . z)) - (f2 /. ((reproj (i,x)) . z)) by A17, VFUNCT_1:def_2 .= ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) /. z by A15, A16, A24, A23, VFUNCT_1:def_2 .= ((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))) . z by A15, A16, PARTFUN1:def_6 ; ::_thesis: verum end; hence ( (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) & (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) ) by A3, A15, A4, PARTFUN1:5; ::_thesis: verum end; theorem Th27: :: PDIFF_1:27 for n, m being non empty Element of NAT for i being Element of NAT for r being Real for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) proof let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT for r being Real for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) let i be Element of NAT ; ::_thesis: for r being Real for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) let r be Real; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) holds r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) let x be Point of (REAL-NS m); ::_thesis: r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) A1: dom (r (#) f) = dom f by VFUNCT_1:def_4; A2: dom (r (#) (f * (reproj (i,x)))) = dom (f * (reproj (i,x))) by VFUNCT_1:def_4; A3: dom (reproj (i,x)) = the carrier of (REAL-NS 1) by FUNCT_2:def_1; for s being Element of (REAL-NS 1) holds ( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) ) proof let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) ) ( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) ) by A3, FUNCT_1:11; hence ( s in dom ((r (#) f) * (reproj (i,x))) iff s in dom (f * (reproj (i,x))) ) by A1, A3, FUNCT_1:11; ::_thesis: verum end; then for s being set holds ( s in dom (r (#) (f * (reproj (i,x)))) iff s in dom ((r (#) f) * (reproj (i,x))) ) by A2; then A4: dom (r (#) (f * (reproj (i,x)))) = dom ((r (#) f) * (reproj (i,x))) by TARSKI:1; A5: for s being Element of (REAL-NS 1) holds ( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) ) proof let s be Element of (REAL-NS 1); ::_thesis: ( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) ) dom (reproj (i,x)) = the carrier of (REAL-NS 1) by FUNCT_2:def_1; hence ( s in dom ((r (#) f) * (reproj (i,x))) iff (reproj (i,x)) . s in dom (r (#) f) ) by FUNCT_1:11; ::_thesis: verum end; for z being Element of (REAL-NS 1) st z in dom (r (#) (f * (reproj (i,x)))) holds (r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z proof let z be Element of (REAL-NS 1); ::_thesis: ( z in dom (r (#) (f * (reproj (i,x)))) implies (r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z ) assume A6: z in dom (r (#) (f * (reproj (i,x)))) ; ::_thesis: (r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z then A7: z in dom (f * (reproj (i,x))) by VFUNCT_1:def_4; A8: (reproj (i,x)) . z in dom f by A1, A5, A4, A6; then A9: f /. ((reproj (i,x)) . z) = f . ((reproj (i,x)) . z) by PARTFUN1:def_6 .= (f * (reproj (i,x))) . z by A7, FUNCT_1:12 .= (f * (reproj (i,x))) /. z by A7, PARTFUN1:def_6 ; A10: (r (#) (f * (reproj (i,x)))) . z = (r (#) (f * (reproj (i,x)))) /. z by A6, PARTFUN1:def_6 .= r * (f /. ((reproj (i,x)) . z)) by A6, A9, VFUNCT_1:def_4 ; ((r (#) f) * (reproj (i,x))) . z = (r (#) f) . ((reproj (i,x)) . z) by A4, A6, FUNCT_1:12 .= (r (#) f) /. ((reproj (i,x)) . z) by A1, A8, PARTFUN1:def_6 .= r * (f /. ((reproj (i,x)) . z)) by A1, A8, VFUNCT_1:def_4 ; hence (r (#) (f * (reproj (i,x)))) . z = ((r (#) f) * (reproj (i,x))) . z by A10; ::_thesis: verum end; hence r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) by A4, PARTFUN1:5; ::_thesis: verum end; theorem Th28: :: PDIFF_1:28 for n, m being non empty Element of NAT for i being Element of NAT for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) ) proof let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) ) let i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) ) let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) ) let x be Point of (REAL-NS m); ::_thesis: ( f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i implies ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) ) ) assume that A1: f1 is_partial_differentiable_in x,i and A2: f2 is_partial_differentiable_in x,i ; ::_thesis: ( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) ) A3: f1 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A1, Def9; A4: f2 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A2, Def9; (f1 + f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) + (f2 * (reproj (i,x))) by Th26; then (f1 + f2) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A3, A4, NDIFF_1:35; hence f1 + f2 is_partial_differentiable_in x,i by Def9; ::_thesis: partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) diff (((f1 * (reproj (i,x))) + (f2 * (reproj (i,x)))),((Proj (i,m)) . x)) = partdiff ((f1 + f2),x,i) by Th26; hence partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) by A3, A4, NDIFF_1:35; ::_thesis: verum end; theorem :: PDIFF_1:29 for n being non empty Element of NAT for i being Element of NAT for g1, g2 being PartFunc of (REAL n),REAL for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for g1, g2 being PartFunc of (REAL n),REAL for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) let i be Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL n),REAL for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) let g1, g2 be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) let y be Element of REAL n; ::_thesis: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i implies ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) ) assume that A1: g1 is_partial_differentiable_in y,i and A2: g2 is_partial_differentiable_in y,i ; ::_thesis: ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def_4; A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider f1 = <>* g1, f2 = <>* g2 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4; reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:98; A4: f1 is_partial_differentiable_in x,i by A1, Th14; then A5: (partdiff (f1,x,i)) . One = <*(partdiff (g1,y,i))*> by Th15; reconsider Pd2 = <*(partdiff (g2,y,i))*> as Element of REAL 1 by FINSEQ_2:98; reconsider Pd1 = <*(partdiff (g1,y,i))*> as Element of REAL 1 by FINSEQ_2:98; A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; rng g2 c= dom ((proj (1,1)) ") by Th2; then A7: dom (((proj (1,1)) ") * g2) = dom g2 by RELAT_1:27; rng g1 c= dom ((proj (1,1)) ") by Th2; then A8: dom (((proj (1,1)) ") * g1) = dom g1 by RELAT_1:27; then dom (f1 + f2) = (dom g1) /\ (dom g2) by A7, VFUNCT_1:def_1; then A9: dom (f1 + f2) = dom (g1 + g2) by VALUED_1:def_1; A10: rng (g1 + g2) c= dom ((proj (1,1)) ") by Th2; then A11: dom (((proj (1,1)) ") * (g1 + g2)) = dom (g1 + g2) by RELAT_1:27; A12: now__::_thesis:_for_x_being_Element_of_(REAL-NS_n)_st_x_in_dom_(f1_+_f2)_holds_ (f1_+_f2)_._x_=_(<>*_(g1_+_g2))_._x let x be Element of (REAL-NS n); ::_thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (<>* (g1 + g2)) . x ) assume A13: x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x = (<>* (g1 + g2)) . x then (f1 + f2) . x = (f1 + f2) /. x by PARTFUN1:def_6; then A14: (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A13, VFUNCT_1:def_1; A15: x in (dom f1) /\ (dom f2) by A13, VFUNCT_1:def_1; then x in dom f1 by XBOOLE_0:def_4; then A16: f1 /. x = (((proj (1,1)) ") * g1) . x by PARTFUN1:def_6; x in dom f2 by A15, XBOOLE_0:def_4; then A17: f2 /. x = (((proj (1,1)) ") * g2) . x by PARTFUN1:def_6; x in dom g2 by A7, A15, XBOOLE_0:def_4; then A18: f2 /. x = ((proj (1,1)) ") . (g2 . x) by A17, FUNCT_1:13; x in dom g1 by A8, A15, XBOOLE_0:def_4; then A19: f1 /. x = ((proj (1,1)) ") . (g1 . x) by A16, FUNCT_1:13; (<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 + g2) . x) by A9, A11, A13, FUNCT_1:12; then (<>* (g1 + g2)) . x = ((proj (1,1)) ") . ((g1 . x) + (g2 . x)) by A9, A13, VALUED_1:def_1; hence (f1 + f2) . x = (<>* (g1 + g2)) . x by A14, A19, A18, Th2, Th3; ::_thesis: verum end; A20: f2 is_partial_differentiable_in x,i by A2, Th14; then A21: (partdiff (f2,x,i)) . One = <*(partdiff (g2,y,i))*> by Th15; A22: f1 + f2 is_partial_differentiable_in x,i by A4, A20, Th28; dom (f1 + f2) = dom (<>* (g1 + g2)) by A9, A10, RELAT_1:27; then A23: f1 + f2 = <>* (g1 + g2) by A6, A3, A12, PARTFUN1:5; then <*(partdiff ((g1 + g2),y,i))*> = (partdiff ((f1 + f2),x,i)) . <*1*> by A4, A20, Th15, Th28 .= ((partdiff (f1,x,i)) + (partdiff (f2,x,i))) . <*1*> by A4, A20, Th28 .= ((partdiff (f1,x,i)) . One) + ((partdiff (f2,x,i)) . One) by LOPBAN_1:35 .= Pd1 + Pd2 by A5, A21, REAL_NS1:2 .= <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> by RVSUM_1:13 ; then partdiff ((g1 + g2),y,i) = <*((partdiff (g1,y,i)) + (partdiff (g2,y,i)))*> . 1 by FINSEQ_1:40; hence ( g1 + g2 is_partial_differentiable_in y,i & partdiff ((g1 + g2),y,i) = (partdiff (g1,y,i)) + (partdiff (g2,y,i)) ) by A23, A22, Th14, FINSEQ_1:40; ::_thesis: verum end; theorem Th30: :: PDIFF_1:30 for n, m being non empty Element of NAT for i being Element of NAT for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) ) proof let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) ) let i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) ) let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) ) let x be Point of (REAL-NS m); ::_thesis: ( f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i implies ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) ) ) assume that A1: f1 is_partial_differentiable_in x,i and A2: f2 is_partial_differentiable_in x,i ; ::_thesis: ( f1 - f2 is_partial_differentiable_in x,i & partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) ) A3: f1 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A1, Def9; A4: f2 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A2, Def9; (f1 - f2) * (reproj (i,x)) = (f1 * (reproj (i,x))) - (f2 * (reproj (i,x))) by Th26; then (f1 - f2) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A3, A4, NDIFF_1:36; hence f1 - f2 is_partial_differentiable_in x,i by Def9; ::_thesis: partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) diff (((f1 * (reproj (i,x))) - (f2 * (reproj (i,x)))),((Proj (i,m)) . x)) = partdiff ((f1 - f2),x,i) by Th26; hence partdiff ((f1 - f2),x,i) = (partdiff (f1,x,i)) - (partdiff (f2,x,i)) by A3, A4, NDIFF_1:36; ::_thesis: verum end; theorem :: PDIFF_1:31 for n being non empty Element of NAT for i being Element of NAT for g1, g2 being PartFunc of (REAL n),REAL for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for g1, g2 being PartFunc of (REAL n),REAL for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) let i be Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL n),REAL for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) let g1, g2 be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n st g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i holds ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) let y be Element of REAL n; ::_thesis: ( g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in y,i implies ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) ) assume that A1: g1 is_partial_differentiable_in y,i and A2: g2 is_partial_differentiable_in y,i ; ::_thesis: ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def_4; A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider f1 = <>* g1, f2 = <>* g2 as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4; reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A3, FINSEQ_2:98; A4: f1 is_partial_differentiable_in x,i by A1, Th14; then A5: (partdiff (f1,x,i)) . One = <*(partdiff (g1,y,i))*> by Th15; reconsider Pd2 = <*(partdiff (g2,y,i))*> as Element of REAL 1 by FINSEQ_2:98; reconsider Pd1 = <*(partdiff (g1,y,i))*> as Element of REAL 1 by FINSEQ_2:98; A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; rng g2 c= dom ((proj (1,1)) ") by Th2; then A7: dom (((proj (1,1)) ") * g2) = dom g2 by RELAT_1:27; rng g1 c= dom ((proj (1,1)) ") by Th2; then A8: dom (((proj (1,1)) ") * g1) = dom g1 by RELAT_1:27; then dom (f1 - f2) = (dom g1) /\ (dom g2) by A7, VFUNCT_1:def_2; then A9: dom (f1 - f2) = dom (g1 - g2) by VALUED_1:12; A10: rng (g1 - g2) c= dom ((proj (1,1)) ") by Th2; then A11: dom (((proj (1,1)) ") * (g1 - g2)) = dom (g1 - g2) by RELAT_1:27; A12: now__::_thesis:_for_x_being_Element_of_(REAL-NS_n)_st_x_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_._x_=_(<>*_(g1_-_g2))_._x let x be Element of (REAL-NS n); ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (<>* (g1 - g2)) . x ) assume A13: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (<>* (g1 - g2)) . x then (f1 - f2) . x = (f1 - f2) /. x by PARTFUN1:def_6; then A14: (f1 - f2) . x = (f1 /. x) - (f2 /. x) by A13, VFUNCT_1:def_2; A15: x in (dom f1) /\ (dom f2) by A13, VFUNCT_1:def_2; then x in dom f1 by XBOOLE_0:def_4; then A16: f1 /. x = (((proj (1,1)) ") * g1) . x by PARTFUN1:def_6; x in dom f2 by A15, XBOOLE_0:def_4; then A17: f2 /. x = (((proj (1,1)) ") * g2) . x by PARTFUN1:def_6; x in dom g2 by A7, A15, XBOOLE_0:def_4; then A18: f2 /. x = ((proj (1,1)) ") . (g2 . x) by A17, FUNCT_1:13; x in dom g1 by A8, A15, XBOOLE_0:def_4; then A19: f1 /. x = ((proj (1,1)) ") . (g1 . x) by A16, FUNCT_1:13; (<>* (g1 - g2)) . x = ((proj (1,1)) ") . ((g1 - g2) . x) by A9, A11, A13, FUNCT_1:12; then (<>* (g1 - g2)) . x = ((proj (1,1)) ") . ((g1 . x) - (g2 . x)) by A9, A13, VALUED_1:13; hence (f1 - f2) . x = (<>* (g1 - g2)) . x by A14, A19, A18, Th2, Th3; ::_thesis: verum end; A20: f2 is_partial_differentiable_in x,i by A2, Th14; then A21: (partdiff (f2,x,i)) . One = <*(partdiff (g2,y,i))*> by Th15; A22: f1 - f2 is_partial_differentiable_in x,i by A4, A20, Th30; dom (f1 - f2) = dom (<>* (g1 - g2)) by A9, A10, RELAT_1:27; then A23: f1 - f2 = <>* (g1 - g2) by A6, A3, A12, PARTFUN1:5; then <*(partdiff ((g1 - g2),y,i))*> = (partdiff ((f1 - f2),x,i)) . <*1*> by A4, A20, Th15, Th30 .= ((partdiff (f1,x,i)) - (partdiff (f2,x,i))) . <*1*> by A4, A20, Th30 .= ((partdiff (f1,x,i)) . One) - ((partdiff (f2,x,i)) . One) by LOPBAN_1:40 .= Pd1 - Pd2 by A5, A21, REAL_NS1:5 .= <*((partdiff (g1,y,i)) - (partdiff (g2,y,i)))*> by RVSUM_1:29 ; then partdiff ((g1 - g2),y,i) = <*((partdiff (g1,y,i)) - (partdiff (g2,y,i)))*> . 1 by FINSEQ_1:40; hence ( g1 - g2 is_partial_differentiable_in y,i & partdiff ((g1 - g2),y,i) = (partdiff (g1,y,i)) - (partdiff (g2,y,i)) ) by A23, A22, Th14, FINSEQ_1:40; ::_thesis: verum end; theorem Th32: :: PDIFF_1:32 for n, m being non empty Element of NAT for i being Element of NAT for r being Real for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) proof let n, m be non empty Element of NAT ; ::_thesis: for i being Element of NAT for r being Real for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) let i be Element of NAT ; ::_thesis: for r being Real for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) let r be Real; ::_thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) let f be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) let x be Point of (REAL-NS m); ::_thesis: ( f is_partial_differentiable_in x,i implies ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) ) assume f is_partial_differentiable_in x,i ; ::_thesis: ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) then A1: f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by Def9; r (#) (f * (reproj (i,x))) = (r (#) f) * (reproj (i,x)) by Th27; then (r (#) f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A1, NDIFF_1:37; hence r (#) f is_partial_differentiable_in x,i by Def9; ::_thesis: partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) diff ((r (#) (f * (reproj (i,x)))),((Proj (i,m)) . x)) = partdiff ((r (#) f),x,i) by Th27; hence partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) by A1, NDIFF_1:37; ::_thesis: verum end; theorem :: PDIFF_1:33 for n being non empty Element of NAT for i being Element of NAT for r being Real for g being PartFunc of (REAL n),REAL for y being Element of REAL n st g is_partial_differentiable_in y,i holds ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) proof let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT for r being Real for g being PartFunc of (REAL n),REAL for y being Element of REAL n st g is_partial_differentiable_in y,i holds ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) let i be Element of NAT ; ::_thesis: for r being Real for g being PartFunc of (REAL n),REAL for y being Element of REAL n st g is_partial_differentiable_in y,i holds ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) let r be Real; ::_thesis: for g being PartFunc of (REAL n),REAL for y being Element of REAL n st g is_partial_differentiable_in y,i holds ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) let g be PartFunc of (REAL n),REAL; ::_thesis: for y being Element of REAL n st g is_partial_differentiable_in y,i holds ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) let y be Element of REAL n; ::_thesis: ( g is_partial_differentiable_in y,i implies ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) ) A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; A2: rng g c= dom ((proj (1,1)) ") by Th2; then A3: dom (((proj (1,1)) ") * g) = dom g by RELAT_1:27; reconsider Pd = <*(partdiff (g,y,i))*> as Element of REAL 1 by FINSEQ_2:98; reconsider x = y as Point of (REAL-NS n) by REAL_NS1:def_4; A4: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def_4; then reconsider f = <>* g as PartFunc of (REAL-NS n),(REAL-NS 1) by REAL_NS1:def_4; reconsider One = <*1*> as VECTOR of (REAL-NS 1) by A4, FINSEQ_2:98; assume g is_partial_differentiable_in y,i ; ::_thesis: ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) then A5: f is_partial_differentiable_in x,i by Th14; then A6: r (#) f is_partial_differentiable_in x,i by Th32; dom (r (#) f) = dom (((proj (1,1)) ") * g) by VFUNCT_1:def_4; then dom (r (#) f) = dom g by A2, RELAT_1:27; then A7: dom (r (#) f) = dom (r (#) g) by VALUED_1:def_5; A8: rng (r (#) g) c= dom ((proj (1,1)) ") by Th2; then A9: dom (((proj (1,1)) ") * (r (#) g)) = dom (r (#) g) by RELAT_1:27; A10: now__::_thesis:_for_x_being_Element_of_(REAL-NS_n)_st_x_in_dom_(r_(#)_f)_holds_ (r_(#)_f)_._x_=_(<>*_(r_(#)_g))_._x let x be Element of (REAL-NS n); ::_thesis: ( x in dom (r (#) f) implies (r (#) f) . x = (<>* (r (#) g)) . x ) consider I being Function of REAL,(REAL 1) such that I is bijective and A11: (proj (1,1)) " = I by Th2; assume A12: x in dom (r (#) f) ; ::_thesis: (r (#) f) . x = (<>* (r (#) g)) . x then A13: (<>* (r (#) g)) . x = ((proj (1,1)) ") . ((r (#) g) . x) by A7, A9, FUNCT_1:12; (r (#) f) . x = (r (#) f) /. x by A12, PARTFUN1:def_6; then A14: (r (#) f) . x = r * (f /. x) by A12, VFUNCT_1:def_4; A15: x in dom g by A3, A12, VFUNCT_1:def_4; then A16: x in dom (r (#) g) by VALUED_1:def_5; x in dom f by A12, VFUNCT_1:def_4; then f /. x = (((proj (1,1)) ") * g) . x by PARTFUN1:def_6; then f /. x = ((proj (1,1)) ") . (g . x) by A15, FUNCT_1:13; then r * (f /. x) = I . (r * (g . x)) by A11, Th3; hence (r (#) f) . x = (<>* (r (#) g)) . x by A16, A14, A13, A11, VALUED_1:def_5; ::_thesis: verum end; A17: (partdiff (f,x,i)) . One = <*(partdiff (g,y,i))*> by A5, Th15; dom (r (#) f) = dom (<>* (r (#) g)) by A7, A8, RELAT_1:27; then A18: r (#) f = <>* (r (#) g) by A1, A4, A10, PARTFUN1:5; then <*(partdiff ((r (#) g),y,i))*> = (partdiff ((r (#) f),x,i)) . <*1*> by A5, Th15, Th32 .= (r * (partdiff (f,x,i))) . <*1*> by A5, Th32 .= r * ((partdiff (f,x,i)) . One) by LOPBAN_1:36 .= r * Pd by A17, REAL_NS1:3 .= <*(r * (partdiff (g,y,i)))*> by RVSUM_1:47 ; then partdiff ((r (#) g),y,i) = <*(r * (partdiff (g,y,i)))*> . 1 by FINSEQ_1:40; hence ( r (#) g is_partial_differentiable_in y,i & partdiff ((r (#) g),y,i) = r * (partdiff (g,y,i)) ) by A18, A6, Th14, FINSEQ_1:40; ::_thesis: verum end;