:: PDIFF_3 semantic presentation begin registration clusterV21() RestFunc-like -> total for Element of K6(K7(REAL,REAL)); coherence for b1 being RestFunc holds b1 is total by FDIFF_1:def_2; end; definition let i be Element of NAT ; let n be non empty Element of NAT ; let f be PartFunc of (REAL n),REAL; func pdiff1 (f,i) -> Function of (REAL n),REAL means :: PDIFF_3:def 1 for z being Element of REAL n holds it . z = partdiff (f,z,i); existence ex b1 being Function of (REAL n),REAL st for z being Element of REAL n holds b1 . z = partdiff (f,z,i) proof deffunc H1( Element of REAL n) -> Element of REAL = partdiff (f,\$1,i); consider g being Function of (REAL n),REAL such that A1: for z being Element of REAL n holds g . z = H1(z) from FUNCT_2:sch_4(); take g ; ::_thesis: for z being Element of REAL n holds g . z = partdiff (f,z,i) thus for z being Element of REAL n holds g . z = partdiff (f,z,i) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of (REAL n),REAL st ( for z being Element of REAL n holds b1 . z = partdiff (f,z,i) ) & ( for z being Element of REAL n holds b2 . z = partdiff (f,z,i) ) holds b1 = b2 proof let F, G be Function of (REAL n),REAL; ::_thesis: ( ( for z being Element of REAL n holds F . z = partdiff (f,z,i) ) & ( for z being Element of REAL n holds G . z = partdiff (f,z,i) ) implies F = G ) assume that A2: for z being Element of REAL n holds F . z = partdiff (f,z,i) and A3: for z being Element of REAL n holds G . z = partdiff (f,z,i) ; ::_thesis: F = G now__::_thesis:_for_z_being_Element_of_REAL_n_holds_F_._z_=_G_._z let z be Element of REAL n; ::_thesis: F . z = G . z F . z = partdiff (f,z,i) by A2; hence F . z = G . z by A3; ::_thesis: verum end; hence F = G by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines pdiff1 PDIFF_3:def_1_:_ for i being Element of NAT for n being non empty Element of NAT for f being PartFunc of (REAL n),REAL for b4 being Function of (REAL n),REAL holds ( b4 = pdiff1 (f,i) iff for z being Element of REAL n holds b4 . z = partdiff (f,z,i) ); definition let f be PartFunc of (REAL 2),REAL; let z be Element of REAL 2; predf is_hpartial_differentiable`11_in z means :Def2: :: PDIFF_3:def 2 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ); predf is_hpartial_differentiable`12_in z means :Def3: :: PDIFF_3:def 3 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ); predf is_hpartial_differentiable`21_in z means :Def4: :: PDIFF_3:def 4 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ); predf is_hpartial_differentiable`22_in z means :Def5: :: PDIFF_3:def 5 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ); end; :: deftheorem Def2 defines is_hpartial_differentiable`11_in PDIFF_3:def_2_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 holds ( f is_hpartial_differentiable`11_in z iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ); :: deftheorem Def3 defines is_hpartial_differentiable`12_in PDIFF_3:def_3_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 holds ( f is_hpartial_differentiable`12_in z iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ); :: deftheorem Def4 defines is_hpartial_differentiable`21_in PDIFF_3:def_4_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 holds ( f is_hpartial_differentiable`21_in z iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ); :: deftheorem Def5 defines is_hpartial_differentiable`22_in PDIFF_3:def_5_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 holds ( f is_hpartial_differentiable`22_in z iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ); definition let f be PartFunc of (REAL 2),REAL; let z be Element of REAL 2; assume A1: f is_hpartial_differentiable`11_in z ; func hpartdiff11 (f,z) -> Real means :Def6: :: PDIFF_3:def 6 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( it = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ); existence ex b1, x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) proof consider x0, y0 being Real such that A2: z = <*x0,y0*> and A3: ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Def2; consider N being Neighbourhood of x0 such that A4: N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and A5: ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3; consider L being LinearFunc, R being RestFunc such that A6: for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5; consider r being Real such that A7: for p being Real holds L . p = r * p by FDIFF_1:def_3; take r ; ::_thesis: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) L . 1 = r * 1 by A7 .= r ; hence ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b2 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds b1 = b2 proof let r, s be Real; ::_thesis: ( ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = s ) assume that A8: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) and A9: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ; ::_thesis: r = s consider x1, y1 being Real such that A10: z = <*x1,y1*> and A11: ex N being Neighbourhood of x1 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) by A9; consider N1 being Neighbourhood of x1 such that N1 c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and A12: ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N1 holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) by A11; consider L1 being LinearFunc, R1 being RestFunc such that A13: s = L1 . 1 and A14: for x being Real st x in N1 holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L1 . (x - x1)) + (R1 . (x - x1)) by A12; consider p1 being Real such that A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3; A16: s = p1 * 1 by A13, A15; consider x0, y0 being Real such that A17: z = <*x0,y0*> and A18: ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A8; consider N being Neighbourhood of x0 such that N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and A19: ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A18; consider L being LinearFunc, R being RestFunc such that A20: r = L . 1 and A21: for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A19; consider r1 being Real such that A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3; A23: x0 = x1 by A17, A10, FINSEQ_1:77; then consider N0 being Neighbourhood of x0 such that A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17; consider g being real number such that A25: 0 < g and A26: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6; deffunc H1( Element of NAT ) -> Element of REAL = g / (\$1 + 2); consider s1 being Real_Sequence such that A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0 let n be Element of NAT ; ::_thesis: s1 . n <> 0 g / (n + 2) <> 0 by A25, XREAL_1:139; hence s1 . n <> 0 by A27; ::_thesis: verum end; then A28: s1 is non-zero by SEQ_1:5; ( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31; then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1; A29: for n being Element of NAT ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) proof let n be Element of NAT ; ::_thesis: ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) take x0 + (g / (n + 2)) ; ::_thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) 0 + 1 < (n + 1) + 1 by XREAL_1:6; then g / (n + 2) < g / 1 by A25, XREAL_1:76; then A30: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6; g / (n + 2) > 0 by A25, XREAL_1:139; then x0 + (- g) < x0 + (g / (n + 2)) by A25, XREAL_1:6; then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A30; hence ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A24, A26, A27; ::_thesis: verum end; A31: r = r1 * 1 by A20, A22; A32: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_ (r_*_(x_-_x0))_+_(R_._(x_-_x0))_=_(s_*_(x_-_x0))_+_(R1_._(x_-_x0)) let x be Real; ::_thesis: ( x in N & x in N1 implies (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) ) assume that A33: x in N and A34: x in N1 ; ::_thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A21, A33; then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A14, A23, A34; then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A22; hence (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) by A15, A31, A16; ::_thesis: verum end; for n being Nat holds r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n proof dom R1 = REAL by PARTFUN1:def_2; then A35: rng h c= dom R1 ; let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n dom R = REAL by PARTFUN1:def_2; then A36: rng h c= dom R ; A37: n in NAT by ORDINAL1:def_12; then ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) by A29; then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32; then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62; A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108 .= ((h ") (#) (R /* h)) . n by VALUED_1:5 ; A40: h . n <> 0 by A37, SEQ_1:5; A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108 .= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ; A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74 .= s * 1 by A40, XCMPLX_1:60 .= s ; (r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74 .= r * 1 by A40, XCMPLX_1:60 .= r ; then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62; then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41; hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, RFUNCT_2:1; ::_thesis: verum end; then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18; then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25; A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2; ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2; then r - s = 0 - 0 by A43, A44, SEQ_2:12; hence r = s ; ::_thesis: verum end; end; :: deftheorem Def6 defines hpartdiff11 PDIFF_3:def_6_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 st f is_hpartial_differentiable`11_in z holds for b3 being Real holds ( b3 = hpartdiff11 (f,z) iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b3 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ); definition let f be PartFunc of (REAL 2),REAL; let z be Element of REAL 2; assume A1: f is_hpartial_differentiable`12_in z ; func hpartdiff12 (f,z) -> Real means :Def7: :: PDIFF_3:def 7 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( it = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ); existence ex b1, x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) proof consider x0, y0 being Real such that A2: z = <*x0,y0*> and A3: ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A1, Def3; consider N being Neighbourhood of y0 such that A4: N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and A5: ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A3; consider L being LinearFunc, R being RestFunc such that A6: for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5; consider r being Real such that A7: for p being Real holds L . p = r * p by FDIFF_1:def_3; take r ; ::_thesis: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) L . 1 = r * 1 by A7 .= r ; hence ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b2 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds b1 = b2 proof let r, s be Real; ::_thesis: ( ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = s ) assume that A8: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) and A9: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ; ::_thesis: r = s consider x1, y1 being Real such that A10: z = <*x1,y1*> and A11: ex N being Neighbourhood of y1 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) by A9; consider N1 being Neighbourhood of y1 such that N1 c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and A12: ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N1 holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) by A11; consider L1 being LinearFunc, R1 being RestFunc such that A13: s = L1 . 1 and A14: for y being Real st y in N1 holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L1 . (y - y1)) + (R1 . (y - y1)) by A12; consider p1 being Real such that A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3; A16: s = p1 * 1 by A13, A15; consider x0, y0 being Real such that A17: z = <*x0,y0*> and A18: ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) by A8; consider N being Neighbourhood of y0 such that N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and A19: ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A18; consider L being LinearFunc, R being RestFunc such that A20: r = L . 1 and A21: for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A19; consider r1 being Real such that A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3; A23: y0 = y1 by A17, A10, FINSEQ_1:77; then consider N0 being Neighbourhood of y0 such that A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17; consider g being real number such that A25: 0 < g and A26: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def_6; deffunc H1( Element of NAT ) -> Element of REAL = g / (\$1 + 2); consider s1 being Real_Sequence such that A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0 let n be Element of NAT ; ::_thesis: s1 . n <> 0 g / (n + 2) <> 0 by A25, XREAL_1:139; hence s1 . n <> 0 by A27; ::_thesis: verum end; then A28: s1 is non-zero by SEQ_1:5; ( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31; then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1; A29: for n being Element of NAT ex y being Real st ( y in N & y in N1 & h . n = y - y0 ) proof let n be Element of NAT ; ::_thesis: ex y being Real st ( y in N & y in N1 & h . n = y - y0 ) take y0 + (g / (n + 2)) ; ::_thesis: ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) 0 + 1 < (n + 1) + 1 by XREAL_1:6; then g / (n + 2) < g / 1 by A25, XREAL_1:76; then A30: y0 + (g / (n + 2)) < y0 + g by XREAL_1:6; g / (n + 2) > 0 by A25, XREAL_1:139; then y0 + (- g) < y0 + (g / (n + 2)) by A25, XREAL_1:6; then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A30; hence ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) by A24, A26, A27; ::_thesis: verum end; A31: r = r1 * 1 by A20, A22; A32: now__::_thesis:_for_y_being_Real_st_y_in_N_&_y_in_N1_holds_ (r_*_(y_-_y0))_+_(R_._(y_-_y0))_=_(s_*_(y_-_y0))_+_(R1_._(y_-_y0)) let y be Real; ::_thesis: ( y in N & y in N1 implies (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) ) assume that A33: y in N and A34: y in N1 ; ::_thesis: (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A21, A33; then (L . (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A14, A23, A34; then (r1 * (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A22; hence (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) by A15, A31, A16; ::_thesis: verum end; now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n dom R1 = REAL by PARTFUN1:def_2; then A35: rng h c= dom R1 ; let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n dom R = REAL by PARTFUN1:def_2; then A36: rng h c= dom R ; A37: n in NAT by ORDINAL1:def_12; then ex y being Real st ( y in N & y in N1 & h . n = y - y0 ) by A29; then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32; then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62; A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108 .= ((h ") (#) (R /* h)) . n by VALUED_1:5 ; A40: h . n <> 0 by A37, SEQ_1:5; A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108 .= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ; A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74 .= s * 1 by A40, XCMPLX_1:60 .= s ; (r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74 .= r * 1 by A40, XCMPLX_1:60 .= r ; then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62; then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41; hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, RFUNCT_2:1; ::_thesis: verum end; then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18; then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25; A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2; ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2; then r - s = 0 - 0 by A43, A44, SEQ_2:12; hence r = s ; ::_thesis: verum end; end; :: deftheorem Def7 defines hpartdiff12 PDIFF_3:def_7_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 st f is_hpartial_differentiable`12_in z holds for b3 being Real holds ( b3 = hpartdiff12 (f,z) iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st ( b3 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ); definition let f be PartFunc of (REAL 2),REAL; let z be Element of REAL 2; assume A1: f is_hpartial_differentiable`21_in z ; func hpartdiff21 (f,z) -> Real means :Def8: :: PDIFF_3:def 8 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( it = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ); existence ex b1, x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) proof consider x0, y0 being Real such that A2: z = <*x0,y0*> and A3: ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Def4; consider N being Neighbourhood of x0 such that A4: N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and A5: ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3; consider L being LinearFunc, R being RestFunc such that A6: for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5; consider r being Real such that A7: for p being Real holds L . p = r * p by FDIFF_1:def_3; take r ; ::_thesis: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) L . 1 = r * 1 by A7 .= r ; hence ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b2 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds b1 = b2 proof let r, s be Real; ::_thesis: ( ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = s ) assume that A8: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) and A9: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ; ::_thesis: r = s consider x1, y1 being Real such that A10: z = <*x1,y1*> and A11: ex N being Neighbourhood of x1 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) by A9; consider N1 being Neighbourhood of x1 such that N1 c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and A12: ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for x being Real st x in N1 holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) by A11; consider L1 being LinearFunc, R1 being RestFunc such that A13: s = L1 . 1 and A14: for x being Real st x in N1 holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L1 . (x - x1)) + (R1 . (x - x1)) by A12; consider p1 being Real such that A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3; A16: s = p1 * 1 by A13, A15; consider x0, y0 being Real such that A17: z = <*x0,y0*> and A18: ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A8; consider N being Neighbourhood of x0 such that N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and A19: ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A18; consider L being LinearFunc, R being RestFunc such that A20: r = L . 1 and A21: for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A19; consider r1 being Real such that A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3; A23: x0 = x1 by A17, A10, FINSEQ_1:77; then consider N0 being Neighbourhood of x0 such that A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17; consider g being real number such that A25: 0 < g and A26: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6; deffunc H1( Element of NAT ) -> Element of REAL = g / (\$1 + 2); consider s1 being Real_Sequence such that A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0 let n be Element of NAT ; ::_thesis: s1 . n <> 0 g / (n + 2) <> 0 by A25, XREAL_1:139; hence s1 . n <> 0 by A27; ::_thesis: verum end; then A28: s1 is non-zero by SEQ_1:5; ( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31; then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1; A29: for n being Element of NAT ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) proof let n be Element of NAT ; ::_thesis: ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) take x0 + (g / (n + 2)) ; ::_thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) 0 + 1 < (n + 1) + 1 by XREAL_1:6; then g / (n + 2) < g / 1 by A25, XREAL_1:76; then A30: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6; g / (n + 2) > 0 by A25, XREAL_1:139; then x0 + (- g) < x0 + (g / (n + 2)) by A25, XREAL_1:6; then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A30; hence ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A24, A26, A27; ::_thesis: verum end; A31: r = r1 * 1 by A20, A22; A32: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_ (r_*_(x_-_x0))_+_(R_._(x_-_x0))_=_(s_*_(x_-_x0))_+_(R1_._(x_-_x0)) let x be Real; ::_thesis: ( x in N & x in N1 implies (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) ) assume that A33: x in N and A34: x in N1 ; ::_thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A21, A33; then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A14, A23, A34; then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A22; hence (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) by A15, A31, A16; ::_thesis: verum end; now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n dom R1 = REAL by PARTFUN1:def_2; then A35: rng h c= dom R1 ; let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n dom R = REAL by PARTFUN1:def_2; then A36: rng h c= dom R ; A37: n in NAT by ORDINAL1:def_12; then ex x being Real st ( x in N & x in N1 & h . n = x - x0 ) by A29; then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32; then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62; A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108 .= ((h ") (#) (R /* h)) . n by VALUED_1:5 ; A40: h . n <> 0 by A37, SEQ_1:5; A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108 .= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ; A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74 .= s * 1 by A40, XCMPLX_1:60 .= s ; (r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74 .= r * 1 by A40, XCMPLX_1:60 .= r ; then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62; then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41; hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, VALUED_1:15; ::_thesis: verum end; then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18; then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25; A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2; ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2; then r - s = 0 - 0 by A43, A44, SEQ_2:12; hence r = s ; ::_thesis: verum end; end; :: deftheorem Def8 defines hpartdiff21 PDIFF_3:def_8_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 st f is_hpartial_differentiable`21_in z holds for b3 being Real holds ( b3 = hpartdiff21 (f,z) iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b3 = L . 1 & ( for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ); definition let f be PartFunc of (REAL 2),REAL; let z be Element of REAL 2; assume A1: f is_hpartial_differentiable`22_in z ; func hpartdiff22 (f,z) -> Real means :Def9: :: PDIFF_3:def 9 ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( it = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ); existence ex b1, x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) proof consider x0, y0 being Real such that A2: z = <*x0,y0*> and A3: ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A1, Def5; consider N being Neighbourhood of y0 such that A4: N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and A5: ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A3; consider L being LinearFunc, R being RestFunc such that A6: for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5; consider r being Real such that A7: for p being Real holds L . p = r * p by FDIFF_1:def_3; take r ; ::_thesis: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) L . 1 = r * 1 by A7 .= r ; hence ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b2 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds b1 = b2 proof let r, s be Real; ::_thesis: ( ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = s ) assume that A8: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) and A9: ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ; ::_thesis: r = s consider x1, y1 being Real such that A10: z = <*x1,y1*> and A11: ex N being Neighbourhood of y1 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) by A9; consider N1 being Neighbourhood of y1 such that N1 c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and A12: ex L being LinearFunc ex R being RestFunc st ( s = L . 1 & ( for y being Real st y in N1 holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) by A11; consider L1 being LinearFunc, R1 being RestFunc such that A13: s = L1 . 1 and A14: for y being Real st y in N1 holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L1 . (y - y1)) + (R1 . (y - y1)) by A12; consider p1 being Real such that A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3; A16: s = p1 * 1 by A13, A15; consider x0, y0 being Real such that A17: z = <*x0,y0*> and A18: ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) by A8; consider N being Neighbourhood of y0 such that N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and A19: ex L being LinearFunc ex R being RestFunc st ( r = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A18; consider L being LinearFunc, R being RestFunc such that A20: r = L . 1 and A21: for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A19; consider r1 being Real such that A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3; A23: y0 = y1 by A17, A10, FINSEQ_1:77; then consider N0 being Neighbourhood of y0 such that A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17; consider g being real number such that A25: 0 < g and A26: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def_6; deffunc H1( Element of NAT ) -> Element of REAL = g / (\$1 + 2); consider s1 being Real_Sequence such that A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0 let n be Element of NAT ; ::_thesis: s1 . n <> 0 g / (n + 2) <> 0 by A25, XREAL_1:139; hence s1 . n <> 0 by A27; ::_thesis: verum end; then A28: s1 is non-zero by SEQ_1:5; ( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31; then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1; A29: for n being Element of NAT ex y being Real st ( y in N & y in N1 & h . n = y - y0 ) proof let n be Element of NAT ; ::_thesis: ex y being Real st ( y in N & y in N1 & h . n = y - y0 ) take y0 + (g / (n + 2)) ; ::_thesis: ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) 0 + 1 < (n + 1) + 1 by XREAL_1:6; then g / (n + 2) < g / 1 by A25, XREAL_1:76; then A30: y0 + (g / (n + 2)) < y0 + g by XREAL_1:6; g / (n + 2) > 0 by A25, XREAL_1:139; then y0 + (- g) < y0 + (g / (n + 2)) by A25, XREAL_1:6; then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A30; hence ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) by A24, A26, A27; ::_thesis: verum end; A31: r = r1 * 1 by A20, A22; A32: now__::_thesis:_for_y_being_Real_st_y_in_N_&_y_in_N1_holds_ (r_*_(y_-_y0))_+_(R_._(y_-_y0))_=_(s_*_(y_-_y0))_+_(R1_._(y_-_y0)) let y be Real; ::_thesis: ( y in N & y in N1 implies (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) ) assume that A33: y in N and A34: y in N1 ; ::_thesis: (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A21, A33; then (L . (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A14, A23, A34; then (r1 * (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A22; hence (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) by A15, A31, A16; ::_thesis: verum end; now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n dom R1 = REAL by PARTFUN1:def_2; then A35: rng h c= dom R1 ; let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n dom R = REAL by PARTFUN1:def_2; then A36: rng h c= dom R ; A37: n in NAT by ORDINAL1:def_12; then ex y being Real st ( y in N & y in N1 & h . n = y - y0 ) by A29; then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32; then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62; A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108 .= ((h ") (#) (R /* h)) . n by VALUED_1:5 ; A40: h . n <> 0 by A37, SEQ_1:5; A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9 .= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10 .= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108 .= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ; A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74 .= s * 1 by A40, XCMPLX_1:60 .= s ; (r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74 .= r * 1 by A40, XCMPLX_1:60 .= r ; then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62; then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41; hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, RFUNCT_2:1; ::_thesis: verum end; then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18; then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25; A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2; ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2; then r - s = 0 - 0 by A43, A44, SEQ_2:12; hence r = s ; ::_thesis: verum end; end; :: deftheorem Def9 defines hpartdiff22 PDIFF_3:def_9_:_ for f being PartFunc of (REAL 2),REAL for z being Element of REAL 2 st f is_hpartial_differentiable`22_in z holds for b3 being Real holds ( b3 = hpartdiff22 (f,z) iff ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st ( b3 = L . 1 & ( for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ); theorem :: PDIFF_3:1 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 ) assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`11_in z ; ::_thesis: SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of x1 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def2; x0 = x1 by A1, A3, FINSEQ_1:77; hence SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 by A4, FDIFF_1:def_4; ::_thesis: verum end; theorem :: PDIFF_3:2 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 ) assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`12_in z ; ::_thesis: SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of y1 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def3; y0 = y1 by A1, A3, FINSEQ_1:77; hence SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 by A4, FDIFF_1:def_4; ::_thesis: verum end; theorem :: PDIFF_3:3 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 ) assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`21_in z ; ::_thesis: SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of x1 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def4; x0 = x1 by A1, A3, FINSEQ_1:77; hence SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 by A4, FDIFF_1:def_4; ::_thesis: verum end; theorem :: PDIFF_3:4 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 ) assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`22_in z ; ::_thesis: SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of y1 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def5; y0 = y1 by A1, A3, FINSEQ_1:77; hence SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 by A4, FDIFF_1:def_4; ::_thesis: verum end; theorem Th5: :: PDIFF_3:5 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) ) set r = hpartdiff11 (f,z); assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`11_in z ; ::_thesis: hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of x1 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def2; consider N being Neighbourhood of x1 such that A5: N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and A6: ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A4; A7: x0 = x1 by A1, A3, FINSEQ_1:77; then A8: SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 by A5, A6, FDIFF_1:def_4; consider L being LinearFunc, R being RestFunc such that A9: for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A6; hpartdiff11 (f,z) = L . 1 by A2, A3, A5, A9, Def6; hence hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum end; theorem Th6: :: PDIFF_3:6 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) ) set r = hpartdiff12 (f,z); assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`12_in z ; ::_thesis: hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of y1 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def3; consider N being Neighbourhood of y1 such that A5: N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and A6: ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A4; A7: y0 = y1 by A1, A3, FINSEQ_1:77; then A8: SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 by A5, A6, FDIFF_1:def_4; consider L being LinearFunc, R being RestFunc such that A9: for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A6; hpartdiff12 (f,z) = L . 1 by A2, A3, A5, A9, Def7; hence hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum end; theorem Th7: :: PDIFF_3:7 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) ) set r = hpartdiff21 (f,z); assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`21_in z ; ::_thesis: hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of x1 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def4; consider N being Neighbourhood of x1 such that A5: N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and A6: ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A4; A7: x0 = x1 by A1, A3, FINSEQ_1:77; then A8: SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 by A5, A6, FDIFF_1:def_4; consider L being LinearFunc, R being RestFunc such that A9: for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A6; hpartdiff21 (f,z) = L . 1 by A2, A3, A5, A9, Def8; hence hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum end; theorem Th8: :: PDIFF_3:8 for x0, y0 being Real for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) proof let x0, y0 be Real; ::_thesis: for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) ) set r = hpartdiff22 (f,z); assume that A1: z = <*x0,y0*> and A2: f is_hpartial_differentiable`22_in z ; ::_thesis: hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) consider x1, y1 being Real such that A3: z = <*x1,y1*> and A4: ex N being Neighbourhood of y1 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def5; consider N being Neighbourhood of y1 such that A5: N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and A6: ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A4; A7: y0 = y1 by A1, A3, FINSEQ_1:77; then A8: SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 by A5, A6, FDIFF_1:def_4; consider L being LinearFunc, R being RestFunc such that A9: for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A6; hpartdiff22 (f,z) = L . 1 by A2, A3, A5, A9, Def9; hence hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum end; definition let f be PartFunc of (REAL 2),REAL; let Z be set ; predf is_hpartial_differentiable`11_on Z means :Def10: :: PDIFF_3:def 10 ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`11_in z ) ); predf is_hpartial_differentiable`12_on Z means :Def11: :: PDIFF_3:def 11 ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`12_in z ) ); predf is_hpartial_differentiable`21_on Z means :Def12: :: PDIFF_3:def 12 ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`21_in z ) ); predf is_hpartial_differentiable`22_on Z means :Def13: :: PDIFF_3:def 13 ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`22_in z ) ); end; :: deftheorem Def10 defines is_hpartial_differentiable`11_on PDIFF_3:def_10_:_ for f being PartFunc of (REAL 2),REAL for Z being set holds ( f is_hpartial_differentiable`11_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`11_in z ) ) ); :: deftheorem Def11 defines is_hpartial_differentiable`12_on PDIFF_3:def_11_:_ for f being PartFunc of (REAL 2),REAL for Z being set holds ( f is_hpartial_differentiable`12_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`12_in z ) ) ); :: deftheorem Def12 defines is_hpartial_differentiable`21_on PDIFF_3:def_12_:_ for f being PartFunc of (REAL 2),REAL for Z being set holds ( f is_hpartial_differentiable`21_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`21_in z ) ) ); :: deftheorem Def13 defines is_hpartial_differentiable`22_on PDIFF_3:def_13_:_ for f being PartFunc of (REAL 2),REAL for Z being set holds ( f is_hpartial_differentiable`22_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds f | Z is_hpartial_differentiable`22_in z ) ) ); definition let f be PartFunc of (REAL 2),REAL; let Z be set ; assume A1: f is_hpartial_differentiable`11_on Z ; funcf `hpartial11| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 14 ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds it . z = hpartdiff11 (f,z) ) ); existence ex b1 being PartFunc of (REAL 2),REAL st ( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff11 (f,z) ) ) proof deffunc H1( Element of REAL 2) -> Real = hpartdiff11 (f,\$1); defpred S1[ Element of REAL 2] means \$1 in Z; consider F being PartFunc of (REAL 2),REAL such that A2: ( ( for z being Element of REAL 2 holds ( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds F . z = H1(z) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff11 (f,z) ) ) now__::_thesis:_for_y_being_set_st_y_in_Z_holds_ y_in_dom_F Z c= dom f by A1, Def10; then A3: Z is Subset of (REAL 2) by XBOOLE_1:1; let y be set ; ::_thesis: ( y in Z implies y in dom F ) assume y in Z ; ::_thesis: y in dom F hence y in dom F by A2, A3; ::_thesis: verum end; then A4: Z c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in Z by A2; then dom F c= Z by TARSKI:def_3; hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff11 (f,z) hereby ::_thesis: verum let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff11 (f,z) ) assume z in Z ; ::_thesis: F . z = hpartdiff11 (f,z) then z in dom F by A2; hence F . z = hpartdiff11 (f,z) by A2; ::_thesis: verum end; end; uniqueness for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff11 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds b2 . z = hpartdiff11 (f,z) ) holds b1 = b2 proof let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff11 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds G . z = hpartdiff11 (f,z) ) implies F = G ) assume that A5: dom F = Z and A6: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff11 (f,z) and A7: dom G = Z and A8: for z being Element of REAL 2 st z in Z holds G . z = hpartdiff11 (f,z) ; ::_thesis: F = G now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_ F_._z_=_G_._z let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z ) assume A9: z in dom F ; ::_thesis: F . z = G . z then F . z = hpartdiff11 (f,z) by A5, A6; hence F . z = G . z by A5, A8, A9; ::_thesis: verum end; hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem defines `hpartial11| PDIFF_3:def_14_:_ for f being PartFunc of (REAL 2),REAL for Z being set st f is_hpartial_differentiable`11_on Z holds for b3 being PartFunc of (REAL 2),REAL holds ( b3 = f `hpartial11| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds b3 . z = hpartdiff11 (f,z) ) ) ); definition let f be PartFunc of (REAL 2),REAL; let Z be set ; assume A1: f is_hpartial_differentiable`12_on Z ; funcf `hpartial12| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 15 ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds it . z = hpartdiff12 (f,z) ) ); existence ex b1 being PartFunc of (REAL 2),REAL st ( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff12 (f,z) ) ) proof deffunc H1( Element of REAL 2) -> Real = hpartdiff12 (f,\$1); defpred S1[ Element of REAL 2] means \$1 in Z; consider F being PartFunc of (REAL 2),REAL such that A2: ( ( for z being Element of REAL 2 holds ( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds F . z = H1(z) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff12 (f,z) ) ) now__::_thesis:_for_y_being_set_st_y_in_Z_holds_ y_in_dom_F Z c= dom f by A1, Def11; then A3: Z is Subset of (REAL 2) by XBOOLE_1:1; let y be set ; ::_thesis: ( y in Z implies y in dom F ) assume y in Z ; ::_thesis: y in dom F hence y in dom F by A2, A3; ::_thesis: verum end; then A4: Z c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in Z by A2; then dom F c= Z by TARSKI:def_3; hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff12 (f,z) hereby ::_thesis: verum let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff12 (f,z) ) assume z in Z ; ::_thesis: F . z = hpartdiff12 (f,z) then z in dom F by A2; hence F . z = hpartdiff12 (f,z) by A2; ::_thesis: verum end; end; uniqueness for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff12 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds b2 . z = hpartdiff12 (f,z) ) holds b1 = b2 proof let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff12 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds G . z = hpartdiff12 (f,z) ) implies F = G ) assume that A5: dom F = Z and A6: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff12 (f,z) and A7: dom G = Z and A8: for z being Element of REAL 2 st z in Z holds G . z = hpartdiff12 (f,z) ; ::_thesis: F = G now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_ F_._z_=_G_._z let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z ) assume A9: z in dom F ; ::_thesis: F . z = G . z then F . z = hpartdiff12 (f,z) by A5, A6; hence F . z = G . z by A5, A8, A9; ::_thesis: verum end; hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem defines `hpartial12| PDIFF_3:def_15_:_ for f being PartFunc of (REAL 2),REAL for Z being set st f is_hpartial_differentiable`12_on Z holds for b3 being PartFunc of (REAL 2),REAL holds ( b3 = f `hpartial12| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds b3 . z = hpartdiff12 (f,z) ) ) ); definition let f be PartFunc of (REAL 2),REAL; let Z be set ; assume A1: f is_hpartial_differentiable`21_on Z ; funcf `hpartial21| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 16 ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds it . z = hpartdiff21 (f,z) ) ); existence ex b1 being PartFunc of (REAL 2),REAL st ( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff21 (f,z) ) ) proof deffunc H1( Element of REAL 2) -> Real = hpartdiff21 (f,\$1); defpred S1[ Element of REAL 2] means \$1 in Z; consider F being PartFunc of (REAL 2),REAL such that A2: ( ( for z being Element of REAL 2 holds ( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds F . z = H1(z) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff21 (f,z) ) ) now__::_thesis:_for_y_being_set_st_y_in_Z_holds_ y_in_dom_F Z c= dom f by A1, Def12; then A3: Z is Subset of (REAL 2) by XBOOLE_1:1; let y be set ; ::_thesis: ( y in Z implies y in dom F ) assume y in Z ; ::_thesis: y in dom F hence y in dom F by A2, A3; ::_thesis: verum end; then A4: Z c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in Z by A2; then dom F c= Z by TARSKI:def_3; hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff21 (f,z) hereby ::_thesis: verum let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff21 (f,z) ) assume z in Z ; ::_thesis: F . z = hpartdiff21 (f,z) then z in dom F by A2; hence F . z = hpartdiff21 (f,z) by A2; ::_thesis: verum end; end; uniqueness for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff21 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds b2 . z = hpartdiff21 (f,z) ) holds b1 = b2 proof let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff21 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds G . z = hpartdiff21 (f,z) ) implies F = G ) assume that A5: dom F = Z and A6: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff21 (f,z) and A7: dom G = Z and A8: for z being Element of REAL 2 st z in Z holds G . z = hpartdiff21 (f,z) ; ::_thesis: F = G now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_ F_._z_=_G_._z let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z ) assume A9: z in dom F ; ::_thesis: F . z = G . z then F . z = hpartdiff21 (f,z) by A5, A6; hence F . z = G . z by A5, A8, A9; ::_thesis: verum end; hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem defines `hpartial21| PDIFF_3:def_16_:_ for f being PartFunc of (REAL 2),REAL for Z being set st f is_hpartial_differentiable`21_on Z holds for b3 being PartFunc of (REAL 2),REAL holds ( b3 = f `hpartial21| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds b3 . z = hpartdiff21 (f,z) ) ) ); definition let f be PartFunc of (REAL 2),REAL; let Z be set ; assume A1: f is_hpartial_differentiable`22_on Z ; funcf `hpartial22| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 17 ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds it . z = hpartdiff22 (f,z) ) ); existence ex b1 being PartFunc of (REAL 2),REAL st ( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff22 (f,z) ) ) proof deffunc H1( Element of REAL 2) -> Real = hpartdiff22 (f,\$1); defpred S1[ Element of REAL 2] means \$1 in Z; consider F being PartFunc of (REAL 2),REAL such that A2: ( ( for z being Element of REAL 2 holds ( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds F . z = H1(z) ) ) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff22 (f,z) ) ) now__::_thesis:_for_y_being_set_st_y_in_Z_holds_ y_in_dom_F Z c= dom f by A1, Def13; then A3: Z is Subset of (REAL 2) by XBOOLE_1:1; let y be set ; ::_thesis: ( y in Z implies y in dom F ) assume y in Z ; ::_thesis: y in dom F hence y in dom F by A2, A3; ::_thesis: verum end; then A4: Z c= dom F by TARSKI:def_3; for y being set st y in dom F holds y in Z by A2; then dom F c= Z by TARSKI:def_3; hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff22 (f,z) hereby ::_thesis: verum let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff22 (f,z) ) assume z in Z ; ::_thesis: F . z = hpartdiff22 (f,z) then z in dom F by A2; hence F . z = hpartdiff22 (f,z) by A2; ::_thesis: verum end; end; uniqueness for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds b1 . z = hpartdiff22 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds b2 . z = hpartdiff22 (f,z) ) holds b1 = b2 proof let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds F . z = hpartdiff22 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds G . z = hpartdiff22 (f,z) ) implies F = G ) assume that A5: dom F = Z and A6: for z being Element of REAL 2 st z in Z holds F . z = hpartdiff22 (f,z) and A7: dom G = Z and A8: for z being Element of REAL 2 st z in Z holds G . z = hpartdiff22 (f,z) ; ::_thesis: F = G now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_ F_._z_=_G_._z let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z ) assume A9: z in dom F ; ::_thesis: F . z = G . z then F . z = hpartdiff22 (f,z) by A5, A6; hence F . z = G . z by A5, A8, A9; ::_thesis: verum end; hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem defines `hpartial22| PDIFF_3:def_17_:_ for f being PartFunc of (REAL 2),REAL for Z being set st f is_hpartial_differentiable`22_on Z holds for b3 being PartFunc of (REAL 2),REAL holds ( b3 = f `hpartial22| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds b3 . z = hpartdiff22 (f,z) ) ) ); begin theorem Th9: :: PDIFF_3:9 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 ) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 ) thus ( f is_hpartial_differentiable`11_in z implies pdiff1 (f,1) is_partial_differentiable_in z,1 ) ::_thesis: ( pdiff1 (f,1) is_partial_differentiable_in z,1 implies f is_hpartial_differentiable`11_in z ) proof assume f is_hpartial_differentiable`11_in z ; ::_thesis: pdiff1 (f,1) is_partial_differentiable_in z,1 then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by Def2; hence pdiff1 (f,1) is_partial_differentiable_in z,1 by PDIFF_2:9; ::_thesis: verum end; assume pdiff1 (f,1) is_partial_differentiable_in z,1 ; ::_thesis: f is_hpartial_differentiable`11_in z then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by PDIFF_2:9; hence f is_hpartial_differentiable`11_in z by Def2; ::_thesis: verum end; theorem Th10: :: PDIFF_3:10 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 ) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 ) thus ( f is_hpartial_differentiable`12_in z implies pdiff1 (f,1) is_partial_differentiable_in z,2 ) ::_thesis: ( pdiff1 (f,1) is_partial_differentiable_in z,2 implies f is_hpartial_differentiable`12_in z ) proof assume f is_hpartial_differentiable`12_in z ; ::_thesis: pdiff1 (f,1) is_partial_differentiable_in z,2 then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by Def3; hence pdiff1 (f,1) is_partial_differentiable_in z,2 by PDIFF_2:10; ::_thesis: verum end; assume pdiff1 (f,1) is_partial_differentiable_in z,2 ; ::_thesis: f is_hpartial_differentiable`12_in z then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by PDIFF_2:10; hence f is_hpartial_differentiable`12_in z by Def3; ::_thesis: verum end; theorem Th11: :: PDIFF_3:11 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 ) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 ) thus ( f is_hpartial_differentiable`21_in z implies pdiff1 (f,2) is_partial_differentiable_in z,1 ) ::_thesis: ( pdiff1 (f,2) is_partial_differentiable_in z,1 implies f is_hpartial_differentiable`21_in z ) proof assume f is_hpartial_differentiable`21_in z ; ::_thesis: pdiff1 (f,2) is_partial_differentiable_in z,1 then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by Def4; hence pdiff1 (f,2) is_partial_differentiable_in z,1 by PDIFF_2:9; ::_thesis: verum end; assume pdiff1 (f,2) is_partial_differentiable_in z,1 ; ::_thesis: f is_hpartial_differentiable`21_in z then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by PDIFF_2:9; hence f is_hpartial_differentiable`21_in z by Def4; ::_thesis: verum end; theorem Th12: :: PDIFF_3:12 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 ) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds ( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 ) thus ( f is_hpartial_differentiable`22_in z implies pdiff1 (f,2) is_partial_differentiable_in z,2 ) ::_thesis: ( pdiff1 (f,2) is_partial_differentiable_in z,2 implies f is_hpartial_differentiable`22_in z ) proof assume f is_hpartial_differentiable`22_in z ; ::_thesis: pdiff1 (f,2) is_partial_differentiable_in z,2 then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by Def5; hence pdiff1 (f,2) is_partial_differentiable_in z,2 by PDIFF_2:10; ::_thesis: verum end; assume pdiff1 (f,2) is_partial_differentiable_in z,2 ; ::_thesis: f is_hpartial_differentiable`22_in z then ex x0, y0 being Real st ( z = <*x0,y0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by PDIFF_2:10; hence f is_hpartial_differentiable`22_in z by Def5; ::_thesis: verum end; theorem Th13: :: PDIFF_3:13 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z holds hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z holds hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`11_in z implies hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1) ) consider x0, y0 being Real such that A1: z = <*x0,y0*> by FINSEQ_2:100; assume A2: f is_hpartial_differentiable`11_in z ; ::_thesis: hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1) then A3: pdiff1 (f,1) is_partial_differentiable_in z,1 by Th9; hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) by A2, A1, Th5 .= partdiff ((pdiff1 (f,1)),z,1) by A1, A3, PDIFF_2:13 ; hence hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1) ; ::_thesis: verum end; theorem Th14: :: PDIFF_3:14 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z holds hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z holds hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`12_in z implies hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2) ) consider x0, y0 being Real such that A1: z = <*x0,y0*> by FINSEQ_2:100; assume A2: f is_hpartial_differentiable`12_in z ; ::_thesis: hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2) then A3: pdiff1 (f,1) is_partial_differentiable_in z,2 by Th10; hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) by A2, A1, Th6 .= partdiff ((pdiff1 (f,1)),z,2) by A1, A3, PDIFF_2:14 ; hence hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2) ; ::_thesis: verum end; theorem Th15: :: PDIFF_3:15 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z holds hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z holds hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`21_in z implies hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1) ) consider x0, y0 being Real such that A1: z = <*x0,y0*> by FINSEQ_2:100; assume A2: f is_hpartial_differentiable`21_in z ; ::_thesis: hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1) then A3: pdiff1 (f,2) is_partial_differentiable_in z,1 by Th11; hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) by A2, A1, Th7 .= partdiff ((pdiff1 (f,2)),z,1) by A1, A3, PDIFF_2:13 ; hence hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1) ; ::_thesis: verum end; theorem Th16: :: PDIFF_3:16 for z being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z holds hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2) proof let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z holds hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`22_in z implies hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2) ) consider x0, y0 being Real such that A1: z = <*x0,y0*> by FINSEQ_2:100; assume A2: f is_hpartial_differentiable`22_in z ; ::_thesis: hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2) then A3: pdiff1 (f,2) is_partial_differentiable_in z,2 by Th12; hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) by A2, A1, Th8 .= partdiff ((pdiff1 (f,2)),z,2) by A1, A3, PDIFF_2:14 ; hence hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2) ; ::_thesis: verum end; theorem :: PDIFF_3:17 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) let N be Neighbourhood of (proj (1,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) implies for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) ) assume that A1: f is_hpartial_differentiable`11_in z0 and A2: N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) ) assume A3: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) consider x0, y0 being Real such that A4: z0 = <*x0,y0*> by FINSEQ_2:100; A5: pdiff1 (f,1) is_partial_differentiable_in z0,1 by A1, Th9; then partdiff ((pdiff1 (f,1)),z0,1) = diff ((SVF1 (1,(pdiff1 (f,1)),z0)),x0) by A4, PDIFF_2:13 .= hpartdiff11 (f,z0) by A1, A4, Th5 ; hence ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:17; ::_thesis: verum end; theorem :: PDIFF_3:18 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) let N be Neighbourhood of (proj (2,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) implies for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) ) assume that A1: f is_hpartial_differentiable`12_in z0 and A2: N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) ) assume A3: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) consider x0, y0 being Real such that A4: z0 = <*x0,y0*> by FINSEQ_2:100; A5: pdiff1 (f,1) is_partial_differentiable_in z0,2 by A1, Th10; then partdiff ((pdiff1 (f,1)),z0,2) = diff ((SVF1 (2,(pdiff1 (f,1)),z0)),y0) by A4, PDIFF_2:14 .= hpartdiff12 (f,z0) by A1, A4, Th6 ; hence ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:18; ::_thesis: verum end; theorem :: PDIFF_3:19 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) let N be Neighbourhood of (proj (1,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) implies for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) ) assume that A1: f is_hpartial_differentiable`21_in z0 and A2: N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) ) assume A3: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) consider x0, y0 being Real such that A4: z0 = <*x0,y0*> by FINSEQ_2:100; A5: pdiff1 (f,2) is_partial_differentiable_in z0,1 by A1, Th11; then partdiff ((pdiff1 (f,2)),z0,1) = diff ((SVF1 (1,(pdiff1 (f,2)),z0)),x0) by A4, PDIFF_2:13 .= hpartdiff21 (f,z0) by A1, A4, Th7 ; hence ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:17; ::_thesis: verum end; theorem :: PDIFF_3:20 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) let N be Neighbourhood of (proj (2,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) implies for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) ) assume that A1: f is_hpartial_differentiable`22_in z0 and A2: N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) ) assume A3: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) consider x0, y0 being Real such that A4: z0 = <*x0,y0*> by FINSEQ_2:100; A5: pdiff1 (f,2) is_partial_differentiable_in z0,2 by A1, Th12; then partdiff ((pdiff1 (f,2)),z0,2) = diff ((SVF1 (2,(pdiff1 (f,2)),z0)),y0) by A4, PDIFF_2:14 .= hpartdiff22 (f,z0) by A1, A4, Th8 ; hence ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:18; ::_thesis: verum end; theorem :: PDIFF_3:21 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`11_in z0 and A2: f2 is_hpartial_differentiable`11_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) ) A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,1 & pdiff1 (f2,1) is_partial_differentiable_in z0,1 ) by A1, A2, Th9; then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (partdiff ((pdiff1 (f1,1)),z0,1)) + (partdiff ((pdiff1 (f2,1)),z0,1)) by PDIFF_1:29; then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (partdiff ((pdiff1 (f2,1)),z0,1)) by A1, Th13 .= (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) by A2, Th13 ; hence ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum end; theorem :: PDIFF_3:22 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`12_in z0 and A2: f2 is_hpartial_differentiable`12_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) ) A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,2 & pdiff1 (f2,1) is_partial_differentiable_in z0,2 ) by A1, A2, Th10; then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (partdiff ((pdiff1 (f1,1)),z0,2)) + (partdiff ((pdiff1 (f2,1)),z0,2)) by PDIFF_1:29; then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (partdiff ((pdiff1 (f2,1)),z0,2)) by A1, Th14 .= (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) by A2, Th14 ; hence ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum end; theorem :: PDIFF_3:23 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`21_in z0 and A2: f2 is_hpartial_differentiable`21_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) ) A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,1 & pdiff1 (f2,2) is_partial_differentiable_in z0,1 ) by A1, A2, Th11; then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (partdiff ((pdiff1 (f1,2)),z0,1)) + (partdiff ((pdiff1 (f2,2)),z0,1)) by PDIFF_1:29; then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (partdiff ((pdiff1 (f2,2)),z0,1)) by A1, Th15 .= (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) by A2, Th15 ; hence ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum end; theorem :: PDIFF_3:24 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`22_in z0 and A2: f2 is_hpartial_differentiable`22_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) ) A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,2 & pdiff1 (f2,2) is_partial_differentiable_in z0,2 ) by A1, A2, Th12; then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (partdiff ((pdiff1 (f1,2)),z0,2)) + (partdiff ((pdiff1 (f2,2)),z0,2)) by PDIFF_1:29; then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (partdiff ((pdiff1 (f2,2)),z0,2)) by A1, Th16 .= (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) by A2, Th16 ; hence ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum end; theorem :: PDIFF_3:25 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`11_in z0 and A2: f2 is_hpartial_differentiable`11_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) ) A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,1 & pdiff1 (f2,1) is_partial_differentiable_in z0,1 ) by A1, A2, Th9; then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (partdiff ((pdiff1 (f1,1)),z0,1)) - (partdiff ((pdiff1 (f2,1)),z0,1)) by PDIFF_1:31; then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (partdiff ((pdiff1 (f2,1)),z0,1)) by A1, Th13 .= (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) by A2, Th13 ; hence ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum end; theorem :: PDIFF_3:26 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`12_in z0 and A2: f2 is_hpartial_differentiable`12_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) ) A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,2 & pdiff1 (f2,1) is_partial_differentiable_in z0,2 ) by A1, A2, Th10; then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (partdiff ((pdiff1 (f1,1)),z0,2)) - (partdiff ((pdiff1 (f2,1)),z0,2)) by PDIFF_1:31; then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (partdiff ((pdiff1 (f2,1)),z0,2)) by A1, Th14 .= (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) by A2, Th14 ; hence ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum end; theorem :: PDIFF_3:27 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`21_in z0 and A2: f2 is_hpartial_differentiable`21_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) ) A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,1 & pdiff1 (f2,2) is_partial_differentiable_in z0,1 ) by A1, A2, Th11; then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (partdiff ((pdiff1 (f1,2)),z0,1)) - (partdiff ((pdiff1 (f2,2)),z0,1)) by PDIFF_1:31; then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (partdiff ((pdiff1 (f2,2)),z0,1)) by A1, Th15 .= (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) by A2, Th15 ; hence ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum end; theorem :: PDIFF_3:28 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) ) proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) ) let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) ) ) assume that A1: f1 is_hpartial_differentiable`22_in z0 and A2: f2 is_hpartial_differentiable`22_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) ) A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,2 & pdiff1 (f2,2) is_partial_differentiable_in z0,2 ) by A1, A2, Th12; then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (partdiff ((pdiff1 (f1,2)),z0,2)) - (partdiff ((pdiff1 (f2,2)),z0,2)) by PDIFF_1:31; then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (partdiff ((pdiff1 (f2,2)),z0,2)) by A1, Th16 .= (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) by A2, Th16 ; hence ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum end; theorem :: PDIFF_3:29 for r being Real for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) proof let r be Real; ::_thesis: for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`11_in z0 implies ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) ) assume A1: f is_hpartial_differentiable`11_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) then A2: pdiff1 (f,1) is_partial_differentiable_in z0,1 by Th9; then partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (partdiff ((pdiff1 (f,1)),z0,1)) by PDIFF_1:33; hence ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) by A1, A2, Th13, PDIFF_1:33; ::_thesis: verum end; theorem :: PDIFF_3:30 for r being Real for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) proof let r be Real; ::_thesis: for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`12_in z0 implies ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) ) assume A1: f is_hpartial_differentiable`12_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) then A2: pdiff1 (f,1) is_partial_differentiable_in z0,2 by Th10; then partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (partdiff ((pdiff1 (f,1)),z0,2)) by PDIFF_1:33; hence ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) by A1, A2, Th14, PDIFF_1:33; ::_thesis: verum end; theorem :: PDIFF_3:31 for r being Real for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) proof let r be Real; ::_thesis: for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`21_in z0 implies ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) ) assume A1: f is_hpartial_differentiable`21_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) then A2: pdiff1 (f,2) is_partial_differentiable_in z0,1 by Th11; then partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (partdiff ((pdiff1 (f,2)),z0,1)) by PDIFF_1:33; hence ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) by A1, A2, Th15, PDIFF_1:33; ::_thesis: verum end; theorem :: PDIFF_3:32 for r being Real for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) proof let r be Real; ::_thesis: for z0 being Element of REAL 2 for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`22_in z0 implies ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) ) assume A1: f is_hpartial_differentiable`22_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) then A2: pdiff1 (f,2) is_partial_differentiable_in z0,2 by Th12; then partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (partdiff ((pdiff1 (f,2)),z0,2)) by PDIFF_1:33; hence ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) by A1, A2, Th16, PDIFF_1:33; ::_thesis: verum end; theorem :: PDIFF_3:33 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 ) assume ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 ) ; ::_thesis: (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 then ( pdiff1 (f1,1) is_partial_differentiable_in z0,1 & pdiff1 (f2,1) is_partial_differentiable_in z0,1 ) by Th9; hence (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 by PDIFF_2:19; ::_thesis: verum end; theorem :: PDIFF_3:34 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 ) assume ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 ) ; ::_thesis: (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 then ( pdiff1 (f1,1) is_partial_differentiable_in z0,2 & pdiff1 (f2,1) is_partial_differentiable_in z0,2 ) by Th10; hence (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 by PDIFF_2:20; ::_thesis: verum end; theorem :: PDIFF_3:35 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 ) assume ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 ) ; ::_thesis: (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 then ( pdiff1 (f1,2) is_partial_differentiable_in z0,1 & pdiff1 (f2,2) is_partial_differentiable_in z0,1 ) by Th11; hence (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 by PDIFF_2:19; ::_thesis: verum end; theorem :: PDIFF_3:36 for z0 being Element of REAL 2 for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 proof let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 ) assume ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 ) ; ::_thesis: (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 then ( pdiff1 (f1,2) is_partial_differentiable_in z0,2 & pdiff1 (f2,2) is_partial_differentiable_in z0,2 ) by Th12; hence (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 by PDIFF_2:20; ::_thesis: verum end; theorem :: PDIFF_3:37 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 st f is_hpartial_differentiable`11_in z0 holds SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0 proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`11_in z0 holds SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0 let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`11_in z0 implies SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0 ) assume f is_hpartial_differentiable`11_in z0 ; ::_thesis: SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0 then pdiff1 (f,1) is_partial_differentiable_in z0,1 by Th9; hence SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0 by PDIFF_2:21; ::_thesis: verum end; theorem :: PDIFF_3:38 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 st f is_hpartial_differentiable`12_in z0 holds SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0 proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`12_in z0 holds SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0 let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`12_in z0 implies SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0 ) assume f is_hpartial_differentiable`12_in z0 ; ::_thesis: SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0 then pdiff1 (f,1) is_partial_differentiable_in z0,2 by Th10; hence SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0 by PDIFF_2:22; ::_thesis: verum end; theorem :: PDIFF_3:39 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 st f is_hpartial_differentiable`21_in z0 holds SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0 proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`21_in z0 holds SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0 let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`21_in z0 implies SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0 ) assume f is_hpartial_differentiable`21_in z0 ; ::_thesis: SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0 then pdiff1 (f,2) is_partial_differentiable_in z0,1 by Th11; hence SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0 by PDIFF_2:21; ::_thesis: verum end; theorem :: PDIFF_3:40 for f being PartFunc of (REAL 2),REAL for z0 being Element of REAL 2 st f is_hpartial_differentiable`22_in z0 holds SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0 proof let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`22_in z0 holds SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0 let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`22_in z0 implies SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0 ) assume f is_hpartial_differentiable`22_in z0 ; ::_thesis: SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0 then pdiff1 (f,2) is_partial_differentiable_in z0,2 by Th12; hence SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0 by PDIFF_2:22; ::_thesis: verum end;