:: Second-order Partial Differentiation of Real Ternary Functions :: by Takao Inou\'e :: :: Received January 26, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; predf is_hpartial_differentiable`11_in u means :Def1: :: PDIFF_5:def 1 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ); predf is_hpartial_differentiable`12_in u means :Def2: :: PDIFF_5:def 2 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ); predf is_hpartial_differentiable`13_in u means :Def3: :: PDIFF_5:def 3 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ); predf is_hpartial_differentiable`21_in u means :Def4: :: PDIFF_5:def 4 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ); predf is_hpartial_differentiable`22_in u means :Def5: :: PDIFF_5:def 5 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ); predf is_hpartial_differentiable`23_in u means :Def6: :: PDIFF_5:def 6 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ); predf is_hpartial_differentiable`31_in u means :Def7: :: PDIFF_5:def 7 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ); predf is_hpartial_differentiable`32_in u means :Def8: :: PDIFF_5:def 8 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ); predf is_hpartial_differentiable`33_in u means :Def9: :: PDIFF_5:def 9 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ); end; :: deftheorem Def1 defines is_hpartial_differentiable`11_in PDIFF_5:def_1_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`11_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,1)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ); :: deftheorem Def2 defines is_hpartial_differentiable`12_in PDIFF_5:def_2_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`12_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,1)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ); :: deftheorem Def3 defines is_hpartial_differentiable`13_in PDIFF_5:def_3_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`13_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ); :: deftheorem Def4 defines is_hpartial_differentiable`21_in PDIFF_5:def_4_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`21_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,2)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ); :: deftheorem Def5 defines is_hpartial_differentiable`22_in PDIFF_5:def_5_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`22_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,2)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ); :: deftheorem Def6 defines is_hpartial_differentiable`23_in PDIFF_5:def_6_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`23_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ); :: deftheorem Def7 defines is_hpartial_differentiable`31_in PDIFF_5:def_7_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`31_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st for x being Real st x in N holds ((SVF1 (1,(pdiff1 (f,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ); :: deftheorem Def8 defines is_hpartial_differentiable`32_in PDIFF_5:def_8_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`32_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st for y being Real st y in N holds ((SVF1 (2,(pdiff1 (f,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ); :: deftheorem Def9 defines is_hpartial_differentiable`33_in PDIFF_5:def_9_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 holds ( f is_hpartial_differentiable`33_in u iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`11_in u ; func hpartdiff11 (f,u) -> Real means :Def10: :: PDIFF_5:def 10 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines hpartdiff11 PDIFF_5:def_10_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`11_in u holds for b3 being Real holds ( b3 = hpartdiff11 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,1)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`12_in u ; func hpartdiff12 (f,u) -> Real means :Def11: :: PDIFF_5:def 11 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines hpartdiff12 PDIFF_5:def_11_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`12_in u holds for b3 being Real holds ( b3 = hpartdiff12 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,1)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`13_in u ; func hpartdiff13 (f,u) -> Real means :Def12: :: PDIFF_5:def 12 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st ( it = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st ( b2 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines hpartdiff13 PDIFF_5:def_12_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`13_in u holds for b3 being Real holds ( b3 = hpartdiff13 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,1)),u)) & ex L being LinearFunc ex R being RestFunc st ( b3 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`21_in u ; func hpartdiff21 (f,u) -> Real means :Def13: :: PDIFF_5:def 13 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines hpartdiff21 PDIFF_5:def_13_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`21_in u holds for b3 being Real holds ( b3 = hpartdiff21 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,2)),u)) & 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)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`22_in u ; func hpartdiff22 (f,u) -> Real means :Def14: :: PDIFF_5:def 14 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def14 defines hpartdiff22 PDIFF_5:def_14_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`22_in u holds for b3 being Real holds ( b3 = hpartdiff22 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,2)),u)) & 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)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`23_in u ; func hpartdiff23 (f,u) -> Real means :Def15: :: PDIFF_5:def 15 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st ( it = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st ( b2 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def15 defines hpartdiff23 PDIFF_5:def_15_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`23_in u holds for b3 being Real holds ( b3 = hpartdiff23 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,2)),u)) & ex L being LinearFunc ex R being RestFunc st ( b3 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`31_in u ; func hpartdiff31 (f,u) -> Real means :Def16: :: PDIFF_5:def 16 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,3)),u)) & 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,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,3)),u)) & 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,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,3)),u)) & 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,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,3)),u)) & 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,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def16 defines hpartdiff31 PDIFF_5:def_16_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`31_in u holds for b3 being Real holds ( b3 = hpartdiff31 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st ( N c= dom (SVF1 (1,(pdiff1 (f,3)),u)) & 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,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`32_in u ; func hpartdiff32 (f,u) -> Real means :Def17: :: PDIFF_5:def 17 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,3)),u)) & 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,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,3)),u)) & 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,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,3)),u)) & 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,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,3)),u)) & 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,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def17 defines hpartdiff32 PDIFF_5:def_17_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`32_in u holds for b3 being Real holds ( b3 = hpartdiff32 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st ( N c= dom (SVF1 (2,(pdiff1 (f,3)),u)) & 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,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let u be Element of REAL 3; assume A1: f is_hpartial_differentiable`33_in u ; func hpartdiff33 (f,u) -> Real means :Def18: :: PDIFF_5:def 18 ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st ( it = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ); existence ex b1, x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) proofend; uniqueness for b1, b2 being Real st ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st ( b1 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) & ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st ( b2 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def18 defines hpartdiff33 PDIFF_5:def_18_:_ for f being PartFunc of (REAL 3),REAL for u being Element of REAL 3 st f is_hpartial_differentiable`33_in u holds for b3 being Real holds ( b3 = hpartdiff33 (f,u) iff ex x0, y0, z0 being Real st ( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st ( N c= dom (SVF1 (3,(pdiff1 (f,3)),u)) & ex L being LinearFunc ex R being RestFunc st ( b3 = L . 1 & ( for z being Real st z in N holds ((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) ); theorem :: PDIFF_5:1 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u holds SVF1 (1,(pdiff1 (f,1)),u) is_differentiable_in x0 proofend; theorem :: PDIFF_5:2 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u holds SVF1 (2,(pdiff1 (f,1)),u) is_differentiable_in y0 proofend; theorem :: PDIFF_5:3 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u holds SVF1 (3,(pdiff1 (f,1)),u) is_differentiable_in z0 proofend; theorem :: PDIFF_5:4 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u holds SVF1 (1,(pdiff1 (f,2)),u) is_differentiable_in x0 proofend; theorem :: PDIFF_5:5 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u holds SVF1 (2,(pdiff1 (f,2)),u) is_differentiable_in y0 proofend; theorem :: PDIFF_5:6 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u holds SVF1 (3,(pdiff1 (f,2)),u) is_differentiable_in z0 proofend; theorem :: PDIFF_5:7 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u holds SVF1 (1,(pdiff1 (f,3)),u) is_differentiable_in x0 proofend; theorem :: PDIFF_5:8 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u holds SVF1 (2,(pdiff1 (f,3)),u) is_differentiable_in y0 proofend; theorem :: PDIFF_5:9 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u holds SVF1 (3,(pdiff1 (f,3)),u) is_differentiable_in z0 proofend; theorem Th10: :: PDIFF_5:10 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u holds hpartdiff11 (f,u) = diff ((SVF1 (1,(pdiff1 (f,1)),u)),x0) proofend; theorem Th11: :: PDIFF_5:11 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u holds hpartdiff12 (f,u) = diff ((SVF1 (2,(pdiff1 (f,1)),u)),y0) proofend; theorem Th12: :: PDIFF_5:12 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u holds hpartdiff13 (f,u) = diff ((SVF1 (3,(pdiff1 (f,1)),u)),z0) proofend; theorem Th13: :: PDIFF_5:13 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u holds hpartdiff21 (f,u) = diff ((SVF1 (1,(pdiff1 (f,2)),u)),x0) proofend; theorem Th14: :: PDIFF_5:14 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u holds hpartdiff22 (f,u) = diff ((SVF1 (2,(pdiff1 (f,2)),u)),y0) proofend; theorem Th15: :: PDIFF_5:15 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u holds hpartdiff23 (f,u) = diff ((SVF1 (3,(pdiff1 (f,2)),u)),z0) proofend; theorem Th16: :: PDIFF_5:16 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u holds hpartdiff31 (f,u) = diff ((SVF1 (1,(pdiff1 (f,3)),u)),x0) proofend; theorem Th17: :: PDIFF_5:17 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u holds hpartdiff32 (f,u) = diff ((SVF1 (2,(pdiff1 (f,3)),u)),y0) proofend; theorem Th18: :: PDIFF_5:18 for x0, y0, z0 being Real for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u holds hpartdiff33 (f,u) = diff ((SVF1 (3,(pdiff1 (f,3)),u)),z0) proofend; definition let f be PartFunc of (REAL 3),REAL; let D be set ; predf is_hpartial_differentiable`11_on D means :Def19: :: PDIFF_5:def 19 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`11_in u ) ); predf is_hpartial_differentiable`12_on D means :Def20: :: PDIFF_5:def 20 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`12_in u ) ); predf is_hpartial_differentiable`13_on D means :Def21: :: PDIFF_5:def 21 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`13_in u ) ); predf is_hpartial_differentiable`21_on D means :Def22: :: PDIFF_5:def 22 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`21_in u ) ); predf is_hpartial_differentiable`22_on D means :Def23: :: PDIFF_5:def 23 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`22_in u ) ); predf is_hpartial_differentiable`23_on D means :Def24: :: PDIFF_5:def 24 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`23_in u ) ); predf is_hpartial_differentiable`31_on D means :Def25: :: PDIFF_5:def 25 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`31_in u ) ); predf is_hpartial_differentiable`32_on D means :Def26: :: PDIFF_5:def 26 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`32_in u ) ); predf is_hpartial_differentiable`33_on D means :Def27: :: PDIFF_5:def 27 ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`33_in u ) ); end; :: deftheorem Def19 defines is_hpartial_differentiable`11_on PDIFF_5:def_19_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`11_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`11_in u ) ) ); :: deftheorem Def20 defines is_hpartial_differentiable`12_on PDIFF_5:def_20_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`12_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`12_in u ) ) ); :: deftheorem Def21 defines is_hpartial_differentiable`13_on PDIFF_5:def_21_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`13_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`13_in u ) ) ); :: deftheorem Def22 defines is_hpartial_differentiable`21_on PDIFF_5:def_22_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`21_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`21_in u ) ) ); :: deftheorem Def23 defines is_hpartial_differentiable`22_on PDIFF_5:def_23_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`22_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`22_in u ) ) ); :: deftheorem Def24 defines is_hpartial_differentiable`23_on PDIFF_5:def_24_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`23_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`23_in u ) ) ); :: deftheorem Def25 defines is_hpartial_differentiable`31_on PDIFF_5:def_25_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`31_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`31_in u ) ) ); :: deftheorem Def26 defines is_hpartial_differentiable`32_on PDIFF_5:def_26_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`32_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`32_in u ) ) ); :: deftheorem Def27 defines is_hpartial_differentiable`33_on PDIFF_5:def_27_:_ for f being PartFunc of (REAL 3),REAL for D being set holds ( f is_hpartial_differentiable`33_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds f | D is_hpartial_differentiable`33_in u ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`11_on D ; funcf `hpartial11| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 28 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff11 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff11 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff11 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff11 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial11| PDIFF_5:def_28_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`11_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial11| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff11 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`12_on D ; funcf `hpartial12| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 29 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff12 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff12 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff12 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff12 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial12| PDIFF_5:def_29_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`12_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial12| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff12 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`13_on D ; funcf `hpartial13| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 30 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff13 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff13 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff13 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff13 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial13| PDIFF_5:def_30_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`13_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial13| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff13 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`21_on D ; funcf `hpartial21| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 31 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff21 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff21 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff21 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff21 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial21| PDIFF_5:def_31_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`21_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial21| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff21 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`22_on D ; funcf `hpartial22| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 32 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff22 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff22 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff22 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff22 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial22| PDIFF_5:def_32_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`22_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial22| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff22 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`23_on D ; funcf `hpartial23| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 33 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff23 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff23 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff23 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff23 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial23| PDIFF_5:def_33_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`23_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial23| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff23 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`31_on D ; funcf `hpartial31| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 34 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff31 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff31 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff31 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff31 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial31| PDIFF_5:def_34_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`31_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial31| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff31 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`32_on D ; funcf `hpartial32| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 35 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff32 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff32 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff32 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff32 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial32| PDIFF_5:def_35_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`32_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial32| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff32 (f,u) ) ) ); definition let f be PartFunc of (REAL 3),REAL; let D be set ; assume A1: f is_hpartial_differentiable`33_on D ; funcf `hpartial33| D -> PartFunc of (REAL 3),REAL means :: PDIFF_5:def 36 ( dom it = D & ( for u being Element of REAL 3 st u in D holds it . u = hpartdiff33 (f,u) ) ); existence ex b1 being PartFunc of (REAL 3),REAL st ( dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff33 (f,u) ) ) proofend; uniqueness for b1, b2 being PartFunc of (REAL 3),REAL st dom b1 = D & ( for u being Element of REAL 3 st u in D holds b1 . u = hpartdiff33 (f,u) ) & dom b2 = D & ( for u being Element of REAL 3 st u in D holds b2 . u = hpartdiff33 (f,u) ) holds b1 = b2 proofend; end; :: deftheorem defines `hpartial33| PDIFF_5:def_36_:_ for f being PartFunc of (REAL 3),REAL for D being set st f is_hpartial_differentiable`33_on D holds for b3 being PartFunc of (REAL 3),REAL holds ( b3 = f `hpartial33| D iff ( dom b3 = D & ( for u being Element of REAL 3 st u in D holds b3 . u = hpartdiff33 (f,u) ) ) ); begin theorem Th19: :: PDIFF_5:19 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`11_in u iff pdiff1 (f,1) is_partial_differentiable_in u,1 ) proofend; theorem Th20: :: PDIFF_5:20 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`12_in u iff pdiff1 (f,1) is_partial_differentiable_in u,2 ) proofend; theorem Th21: :: PDIFF_5:21 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`13_in u iff pdiff1 (f,1) is_partial_differentiable_in u,3 ) proofend; theorem Th22: :: PDIFF_5:22 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`21_in u iff pdiff1 (f,2) is_partial_differentiable_in u,1 ) proofend; theorem Th23: :: PDIFF_5:23 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`22_in u iff pdiff1 (f,2) is_partial_differentiable_in u,2 ) proofend; theorem Th24: :: PDIFF_5:24 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`23_in u iff pdiff1 (f,2) is_partial_differentiable_in u,3 ) proofend; theorem Th25: :: PDIFF_5:25 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`31_in u iff pdiff1 (f,3) is_partial_differentiable_in u,1 ) proofend; theorem Th26: :: PDIFF_5:26 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`32_in u iff pdiff1 (f,3) is_partial_differentiable_in u,2 ) proofend; theorem Th27: :: PDIFF_5:27 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL holds ( f is_hpartial_differentiable`33_in u iff pdiff1 (f,3) is_partial_differentiable_in u,3 ) proofend; theorem Th28: :: PDIFF_5:28 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`11_in u holds hpartdiff11 (f,u) = partdiff ((pdiff1 (f,1)),u,1) proofend; theorem Th29: :: PDIFF_5:29 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`12_in u holds hpartdiff12 (f,u) = partdiff ((pdiff1 (f,1)),u,2) proofend; theorem Th30: :: PDIFF_5:30 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`13_in u holds hpartdiff13 (f,u) = partdiff ((pdiff1 (f,1)),u,3) proofend; theorem Th31: :: PDIFF_5:31 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`21_in u holds hpartdiff21 (f,u) = partdiff ((pdiff1 (f,2)),u,1) proofend; theorem Th32: :: PDIFF_5:32 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`22_in u holds hpartdiff22 (f,u) = partdiff ((pdiff1 (f,2)),u,2) proofend; theorem Th33: :: PDIFF_5:33 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`23_in u holds hpartdiff23 (f,u) = partdiff ((pdiff1 (f,2)),u,3) proofend; theorem Th34: :: PDIFF_5:34 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`31_in u holds hpartdiff31 (f,u) = partdiff ((pdiff1 (f,3)),u,1) proofend; theorem Th35: :: PDIFF_5:35 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`32_in u holds hpartdiff32 (f,u) = partdiff ((pdiff1 (f,3)),u,2) proofend; theorem Th36: :: PDIFF_5:36 for u being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`33_in u holds hpartdiff33 (f,u) = partdiff ((pdiff1 (f,3)),u,3) proofend; theorem :: PDIFF_5:37 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (1,3)) . u0 st f is_hpartial_differentiable`11_in u0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),u0)) /* c)) is convergent & hpartdiff11 (f,u0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:38 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (2,3)) . u0 st f is_hpartial_differentiable`12_in u0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),u0)) /* c)) is convergent & hpartdiff12 (f,u0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:39 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (3,3)) . u0 st f is_hpartial_differentiable`13_in u0 & N c= dom (SVF1 (3,(pdiff1 (f,1)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (3,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,1)),u0)) /* c)) is convergent & hpartdiff13 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,1)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:40 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (1,3)) . u0 st f is_hpartial_differentiable`21_in u0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),u0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),u0)) /* c)) is convergent & hpartdiff21 (f,u0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),u0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:41 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (2,3)) . u0 st f is_hpartial_differentiable`22_in u0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),u0)) /* c)) is convergent & hpartdiff22 (f,u0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:42 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (3,3)) . u0 st f is_hpartial_differentiable`23_in u0 & N c= dom (SVF1 (3,(pdiff1 (f,2)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (3,(pdiff1 (f,2)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,2)),u0)) /* c)) is convergent & hpartdiff23 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,2)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,2)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:43 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (1,3)) . u0 st f is_hpartial_differentiable`31_in u0 & N c= dom (SVF1 (1,(pdiff1 (f,3)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (1,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (1,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff31 (f,u0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,3)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:44 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (2,3)) . u0 st f is_hpartial_differentiable`32_in u0 & N c= dom (SVF1 (2,(pdiff1 (f,3)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (2,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (2,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff32 (f,u0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,3)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:45 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 for N being Neighbourhood of (proj (3,3)) . u0 st f is_hpartial_differentiable`33_in u0 & N c= dom (SVF1 (3,(pdiff1 (f,3)),u0)) holds for h being non-zero 0 -convergent Real_Sequence for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds ( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) ) proofend; theorem :: PDIFF_5:46 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`11_in u0 & f2 is_hpartial_differentiable`11_in u0 holds ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in u0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),u0,1) = (hpartdiff11 (f1,u0)) + (hpartdiff11 (f2,u0)) ) proofend; theorem :: PDIFF_5:47 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`12_in u0 & f2 is_hpartial_differentiable`12_in u0 holds ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in u0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),u0,2) = (hpartdiff12 (f1,u0)) + (hpartdiff12 (f2,u0)) ) proofend; theorem :: PDIFF_5:48 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`13_in u0 & f2 is_hpartial_differentiable`13_in u0 holds ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in u0,3 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),u0,3) = (hpartdiff13 (f1,u0)) + (hpartdiff13 (f2,u0)) ) proofend; theorem :: PDIFF_5:49 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`21_in u0 & f2 is_hpartial_differentiable`21_in u0 holds ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in u0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),u0,1) = (hpartdiff21 (f1,u0)) + (hpartdiff21 (f2,u0)) ) proofend; theorem :: PDIFF_5:50 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`22_in u0 & f2 is_hpartial_differentiable`22_in u0 holds ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in u0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),u0,2) = (hpartdiff22 (f1,u0)) + (hpartdiff22 (f2,u0)) ) proofend; theorem :: PDIFF_5:51 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`23_in u0 & f2 is_hpartial_differentiable`23_in u0 holds ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in u0,3 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),u0,3) = (hpartdiff23 (f1,u0)) + (hpartdiff23 (f2,u0)) ) proofend; theorem :: PDIFF_5:52 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`11_in u0 & f2 is_hpartial_differentiable`11_in u0 holds ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in u0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),u0,1) = (hpartdiff11 (f1,u0)) - (hpartdiff11 (f2,u0)) ) proofend; theorem :: PDIFF_5:53 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`12_in u0 & f2 is_hpartial_differentiable`12_in u0 holds ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in u0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),u0,2) = (hpartdiff12 (f1,u0)) - (hpartdiff12 (f2,u0)) ) proofend; theorem :: PDIFF_5:54 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`13_in u0 & f2 is_hpartial_differentiable`13_in u0 holds ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in u0,3 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),u0,3) = (hpartdiff13 (f1,u0)) - (hpartdiff13 (f2,u0)) ) proofend; theorem :: PDIFF_5:55 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`21_in u0 & f2 is_hpartial_differentiable`21_in u0 holds ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in u0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),u0,1) = (hpartdiff21 (f1,u0)) - (hpartdiff21 (f2,u0)) ) proofend; theorem :: PDIFF_5:56 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`22_in u0 & f2 is_hpartial_differentiable`22_in u0 holds ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in u0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),u0,2) = (hpartdiff22 (f1,u0)) - (hpartdiff22 (f2,u0)) ) proofend; theorem :: PDIFF_5:57 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`23_in u0 & f2 is_hpartial_differentiable`23_in u0 holds ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in u0,3 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),u0,3) = (hpartdiff23 (f1,u0)) - (hpartdiff23 (f2,u0)) ) proofend; theorem :: PDIFF_5:58 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`11_in u0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in u0,1 & partdiff ((r (#) (pdiff1 (f,1))),u0,1) = r * (hpartdiff11 (f,u0)) ) proofend; theorem :: PDIFF_5:59 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`12_in u0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in u0,2 & partdiff ((r (#) (pdiff1 (f,1))),u0,2) = r * (hpartdiff12 (f,u0)) ) proofend; theorem :: PDIFF_5:60 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`13_in u0 holds ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in u0,3 & partdiff ((r (#) (pdiff1 (f,1))),u0,3) = r * (hpartdiff13 (f,u0)) ) proofend; theorem :: PDIFF_5:61 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`21_in u0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in u0,1 & partdiff ((r (#) (pdiff1 (f,2))),u0,1) = r * (hpartdiff21 (f,u0)) ) proofend; theorem :: PDIFF_5:62 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`22_in u0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in u0,2 & partdiff ((r (#) (pdiff1 (f,2))),u0,2) = r * (hpartdiff22 (f,u0)) ) proofend; theorem :: PDIFF_5:63 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`23_in u0 holds ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in u0,3 & partdiff ((r (#) (pdiff1 (f,2))),u0,3) = r * (hpartdiff23 (f,u0)) ) proofend; theorem :: PDIFF_5:64 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`31_in u0 holds ( r (#) (pdiff1 (f,3)) is_partial_differentiable_in u0,1 & partdiff ((r (#) (pdiff1 (f,3))),u0,1) = r * (hpartdiff31 (f,u0)) ) proofend; theorem :: PDIFF_5:65 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`32_in u0 holds ( r (#) (pdiff1 (f,3)) is_partial_differentiable_in u0,2 & partdiff ((r (#) (pdiff1 (f,3))),u0,2) = r * (hpartdiff32 (f,u0)) ) proofend; theorem :: PDIFF_5:66 for r being Real for u0 being Element of REAL 3 for f being PartFunc of (REAL 3),REAL st f is_hpartial_differentiable`33_in u0 holds ( r (#) (pdiff1 (f,3)) is_partial_differentiable_in u0,3 & partdiff ((r (#) (pdiff1 (f,3))),u0,3) = r * (hpartdiff33 (f,u0)) ) proofend; theorem :: PDIFF_5:67 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`11_in u0 & f2 is_hpartial_differentiable`11_in u0 holds (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in u0,1 proofend; theorem :: PDIFF_5:68 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`12_in u0 & f2 is_hpartial_differentiable`12_in u0 holds (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in u0,2 proofend; theorem :: PDIFF_5:69 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`13_in u0 & f2 is_hpartial_differentiable`13_in u0 holds (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in u0,3 proofend; theorem :: PDIFF_5:70 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`21_in u0 & f2 is_hpartial_differentiable`21_in u0 holds (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in u0,1 proofend; theorem :: PDIFF_5:71 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`22_in u0 & f2 is_hpartial_differentiable`22_in u0 holds (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in u0,2 proofend; theorem :: PDIFF_5:72 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`23_in u0 & f2 is_hpartial_differentiable`23_in u0 holds (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in u0,3 proofend; theorem :: PDIFF_5:73 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`31_in u0 & f2 is_hpartial_differentiable`31_in u0 holds (pdiff1 (f1,3)) (#) (pdiff1 (f2,3)) is_partial_differentiable_in u0,1 proofend; theorem :: PDIFF_5:74 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`32_in u0 & f2 is_hpartial_differentiable`32_in u0 holds (pdiff1 (f1,3)) (#) (pdiff1 (f2,3)) is_partial_differentiable_in u0,2 proofend; theorem :: PDIFF_5:75 for u0 being Element of REAL 3 for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`33_in u0 & f2 is_hpartial_differentiable`33_in u0 holds (pdiff1 (f1,3)) (#) (pdiff1 (f2,3)) is_partial_differentiable_in u0,3 proofend; theorem :: PDIFF_5:76 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`11_in u0 holds SVF1 (1,(pdiff1 (f,1)),u0) is_continuous_in (proj (1,3)) . u0 proofend; theorem :: PDIFF_5:77 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`12_in u0 holds SVF1 (2,(pdiff1 (f,1)),u0) is_continuous_in (proj (2,3)) . u0 proofend; theorem :: PDIFF_5:78 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`13_in u0 holds SVF1 (3,(pdiff1 (f,1)),u0) is_continuous_in (proj (3,3)) . u0 proofend; theorem :: PDIFF_5:79 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`21_in u0 holds SVF1 (1,(pdiff1 (f,2)),u0) is_continuous_in (proj (1,3)) . u0 proofend; theorem :: PDIFF_5:80 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`22_in u0 holds SVF1 (2,(pdiff1 (f,2)),u0) is_continuous_in (proj (2,3)) . u0 proofend; theorem :: PDIFF_5:81 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`23_in u0 holds SVF1 (3,(pdiff1 (f,2)),u0) is_continuous_in (proj (3,3)) . u0 proofend; theorem :: PDIFF_5:82 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`31_in u0 holds SVF1 (1,(pdiff1 (f,3)),u0) is_continuous_in (proj (1,3)) . u0 proofend; theorem :: PDIFF_5:83 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`32_in u0 holds SVF1 (2,(pdiff1 (f,3)),u0) is_continuous_in (proj (2,3)) . u0 proofend; theorem :: PDIFF_5:84 for f being PartFunc of (REAL 3),REAL for u0 being Element of REAL 3 st f is_hpartial_differentiable`33_in u0 holds SVF1 (3,(pdiff1 (f,3)),u0) is_continuous_in (proj (3,3)) . u0 proofend;