:: by Takao Inou\'e

::

:: Received January 26, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

definition

let f be PartFunc of (REAL 3),REAL;

let u be Element of REAL 3;

end;
let u be Element of REAL 3;

pred f is_hpartial_differentiable`11_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`12_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`13_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`21_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`22_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`23_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`31_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`32_in u means :: 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)) ) );

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)) ) );

pred f is_hpartial_differentiable`33_in u means :: 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)) ) );

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)) ) );

:: deftheorem 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)) ) ) );

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 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)) ) ) );

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 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)) ) ) );

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 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)) ) ) );

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 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)) ) ) );

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 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)) ) ) );

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 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)) ) ) );

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 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)) ) ) );

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 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)) ) ) );

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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (1,(pdiff1 (f,1)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (1,(pdiff1 (f,1)),u)) . x) - ((SVF1 (1,(pdiff1 (f,1)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (2,(pdiff1 (f,1)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (2,(pdiff1 (f,1)),u)) . y) - ((SVF1 (2,(pdiff1 (f,1)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (3,(pdiff1 (f,1)),u)) . z) - ((SVF1 (3,(pdiff1 (f,1)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (1,(pdiff1 (f,2)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (1,(pdiff1 (f,2)),u)) . x) - ((SVF1 (1,(pdiff1 (f,2)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (2,(pdiff1 (f,2)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (2,(pdiff1 (f,2)),u)) . y) - ((SVF1 (2,(pdiff1 (f,2)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (3,(pdiff1 (f,2)),u)) . z) - ((SVF1 (3,(pdiff1 (f,2)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (1,(pdiff1 (f,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (1,(pdiff1 (f,3)),u)) . x) - ((SVF1 (1,(pdiff1 (f,3)),u)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (2,(pdiff1 (f,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (2,(pdiff1 (f,3)),u)) . y) - ((SVF1 (2,(pdiff1 (f,3)),u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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 ;

ex b_{1}, 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

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

end;
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 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)) ) ) ) );

ex b

( 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

( b

((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) )

proof end;

uniqueness for b

( 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

( b

((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

( b

((SVF1 (3,(pdiff1 (f,3)),u)) . z) - ((SVF1 (3,(pdiff1 (f,3)),u)) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) holds

b

proof 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 b_{3} being Real holds

( b_{3} = 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

( b_{3} = 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)) ) ) ) ) );

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 b

( b

( 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

( b

((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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

end;
let D be set ;

pred f is_hpartial_differentiable`11_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`11_in u ) );

pred f is_hpartial_differentiable`12_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`12_in u ) );

pred f is_hpartial_differentiable`13_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`13_in u ) );

pred f is_hpartial_differentiable`21_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`21_in u ) );

pred f is_hpartial_differentiable`22_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`22_in u ) );

pred f is_hpartial_differentiable`23_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`23_in u ) );

pred f is_hpartial_differentiable`31_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`31_in u ) );

pred f is_hpartial_differentiable`32_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`32_in u ) );

pred f is_hpartial_differentiable`33_on D means :: 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 ) );

( D c= dom f & ( for u being Element of REAL 3 st u in D holds

f | D is_hpartial_differentiable`33_in u ) );

:: deftheorem 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 ) ) );

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 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 ) ) );

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 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 ) ) );

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 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 ) ) );

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 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 ) ) );

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 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 ) ) );

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 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 ) ) );

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 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 ) ) );

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 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 ) ) );

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 ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff11 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff11 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff11 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`11_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff11 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial11| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff11 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`11_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`12_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff12 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff12 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff12 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`12_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff12 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial12| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff12 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`12_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`13_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff13 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff13 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff13 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`13_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff13 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial13| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff13 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`13_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`21_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff21 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff21 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff21 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`21_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff21 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial21| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff21 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`21_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`22_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff22 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff22 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff22 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`22_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff22 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial22| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff22 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`22_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`23_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff23 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff23 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff23 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`23_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff23 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial23| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff23 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`23_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`31_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff31 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff31 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff31 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`31_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff31 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial31| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff31 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`31_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`32_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff32 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff32 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff32 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`32_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff32 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial32| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff32 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`32_on D holds

for b

( b

b

definition

let f be PartFunc of (REAL 3),REAL;

let D be set ;

assume A1: f is_hpartial_differentiable`33_on D ;

ex b_{1} being PartFunc of (REAL 3),REAL st

( dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff33 (f,u) ) )

for b_{1}, b_{2} being PartFunc of (REAL 3),REAL st dom b_{1} = D & ( for u being Element of REAL 3 st u in D holds

b_{1} . u = hpartdiff33 (f,u) ) & dom b_{2} = D & ( for u being Element of REAL 3 st u in D holds

b_{2} . u = hpartdiff33 (f,u) ) holds

b_{1} = b_{2}

end;
let D be set ;

assume A1: f is_hpartial_differentiable`33_on D ;

func f `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 ( dom it = D & ( for u being Element of REAL 3 st u in D holds

it . u = hpartdiff33 (f,u) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of (REAL 3),REAL holds

( b_{3} = f `hpartial33| D iff ( dom b_{3} = D & ( for u being Element of REAL 3 st u in D holds

b_{3} . u = hpartdiff33 (f,u) ) ) );

for f being PartFunc of (REAL 3),REAL

for D being set st f is_hpartial_differentiable`33_on D holds

for b

( b

b

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 ) by PDIFF_4:13;

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 ) by PDIFF_4:13;

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 ) by PDIFF_4:14;

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 ) by PDIFF_4:14;

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 ) by PDIFF_4:15;

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 ) by PDIFF_4:15;

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 ) by PDIFF_4:13;

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 ) by PDIFF_4:13;

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 ) by PDIFF_4:14;

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 ) by PDIFF_4:14;

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 ) by PDIFF_4:15;

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 ) by PDIFF_4:15;

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 ) by PDIFF_4:13;

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 ) by PDIFF_4:13;

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 ) by PDIFF_4:14;

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 ) by PDIFF_4:14;

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 ) by PDIFF_4:15;

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 ) by PDIFF_4:15;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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)

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)

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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))) )

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))) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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)) )

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)) )

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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 by Th19, PDIFF_4:31;

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 by Th19, PDIFF_4:31;

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 by Th20, PDIFF_4:32;

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 by Th20, PDIFF_4:32;

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 by Th21, PDIFF_4:33;

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 by Th21, PDIFF_4:33;

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 by Th22, PDIFF_4:31;

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 by Th22, PDIFF_4:31;

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 by Th23, PDIFF_4:32;

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 by Th23, PDIFF_4:32;

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 by Th24, PDIFF_4:33;

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 by Th24, PDIFF_4:33;

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 by Th25, PDIFF_4:31;

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 by Th25, PDIFF_4:31;

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 by Th26, PDIFF_4:32;

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 by Th26, PDIFF_4:32;

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 by Th27, PDIFF_4:33;

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 by Th27, PDIFF_4:33;