:: by Bing Xie , Xiquan Liang and Xiuzhuan Shen

::

:: Received December 16, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

definition

let i be Element of NAT ;

let n be non empty Element of NAT ;

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

ex b_{1} being Function of (REAL n),REAL st

for z being Element of REAL n holds b_{1} . z = partdiff (f,z,i)

for b_{1}, b_{2} being Function of (REAL n),REAL st ( for z being Element of REAL n holds b_{1} . z = partdiff (f,z,i) ) & ( for z being Element of REAL n holds b_{2} . z = partdiff (f,z,i) ) holds

b_{1} = b_{2}

end;
let n be non empty Element of NAT ;

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

func pdiff1 (f,i) -> Function of (REAL n),REAL means :: PDIFF_3:def 1

for z being Element of REAL n holds it . z = partdiff (f,z,i);

existence for z being Element of REAL n holds it . z = partdiff (f,z,i);

ex b

for z being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines pdiff1 PDIFF_3:def 1 :

for i being Element of NAT

for n being non empty Element of NAT

for f being PartFunc of (REAL n),REAL

for b_{4} being Function of (REAL n),REAL holds

( b_{4} = pdiff1 (f,i) iff for z being Element of REAL n holds b_{4} . z = partdiff (f,z,i) );

for i being Element of NAT

for n being non empty Element of NAT

for f being PartFunc of (REAL n),REAL

for b

( b

definition

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

let z be Element of REAL 2;

end;
let z be Element of REAL 2;

pred f is_hpartial_differentiable`11_in z means :Def2: :: PDIFF_3:def 2

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

pred f is_hpartial_differentiable`12_in z means :Def3: :: PDIFF_3:def 3

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

pred f is_hpartial_differentiable`21_in z means :Def4: :: PDIFF_3:def 4

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

pred f is_hpartial_differentiable`22_in z means :Def5: :: PDIFF_3:def 5

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

:: deftheorem Def2 defines is_hpartial_differentiable`11_in PDIFF_3:def 2 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`11_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`11_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

:: deftheorem Def3 defines is_hpartial_differentiable`12_in PDIFF_3:def 3 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`12_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`12_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

:: deftheorem Def4 defines is_hpartial_differentiable`21_in PDIFF_3:def 4 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`21_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`21_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

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

:: deftheorem Def5 defines is_hpartial_differentiable`22_in PDIFF_3:def 5 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`22_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 holds

( f is_hpartial_differentiable`22_in z iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

for y being Real st y in N holds

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

definition

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

let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`11_in z ;

ex b_{1}, x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for x being Real st x in N holds

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

for b_{1}, b_{2} being Real st ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for x being Real st x in N holds

((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{2} = L . 1 & ( for x being Real st x in N holds

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

b_{1} = b_{2}

end;
let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`11_in z ;

func hpartdiff11 (f,z) -> Real means :Def6: :: PDIFF_3:def 6

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for x being Real st x in N holds

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

existence ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for x being Real st x in N holds

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

ex b

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

proof end;

uniqueness for b

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

b

proof end;

:: deftheorem Def6 defines hpartdiff11 PDIFF_3:def 6 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`11_in z holds

for b_{3} being Real holds

( b_{3} = hpartdiff11 (f,z) iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{3} = L . 1 & ( for x being Real st x in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`11_in z holds

for b

( b

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

definition

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

let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`12_in z ;

ex b_{1}, x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for y being Real st y in N holds

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

for b_{1}, b_{2} being Real st ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for y being Real st y in N holds

((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{2} = L . 1 & ( for y being Real st y in N holds

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

b_{1} = b_{2}

end;
let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`12_in z ;

func hpartdiff12 (f,z) -> Real means :Def7: :: PDIFF_3:def 7

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for y being Real st y in N holds

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

existence ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for y being Real st y in N holds

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

ex b

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

proof end;

uniqueness for b

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

b

proof end;

:: deftheorem Def7 defines hpartdiff12 PDIFF_3:def 7 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`12_in z holds

for b_{3} being Real holds

( b_{3} = hpartdiff12 (f,z) iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{3} = L . 1 & ( for y being Real st y in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`12_in z holds

for b

( b

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

definition

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

let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`21_in z ;

ex b_{1}, x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for x being Real st x in N holds

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

for b_{1}, b_{2} being Real st ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for x being Real st x in N holds

((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{2} = L . 1 & ( for x being Real st x in N holds

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

b_{1} = b_{2}

end;
let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`21_in z ;

func hpartdiff21 (f,z) -> Real means :Def8: :: PDIFF_3:def 8

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for x being Real st x in N holds

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

existence ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for x being Real st x in N holds

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

ex b

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

proof end;

uniqueness for b

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

b

proof end;

:: deftheorem Def8 defines hpartdiff21 PDIFF_3:def 8 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`21_in z holds

for b_{3} being Real holds

( b_{3} = hpartdiff21 (f,z) iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{3} = L . 1 & ( for x being Real st x in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`21_in z holds

for b

( b

( z = <*x0,y0*> & ex N being Neighbourhood of x0 st

( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

definition

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

let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`22_in z ;

ex b_{1}, x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for y being Real st y in N holds

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

for b_{1}, b_{2} being Real st ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for y being Real st y in N holds

((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{2} = L . 1 & ( for y being Real st y in N holds

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

b_{1} = b_{2}

end;
let z be Element of REAL 2;

assume A1: f is_hpartial_differentiable`22_in z ;

func hpartdiff22 (f,z) -> Real means :Def9: :: PDIFF_3:def 9

ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for y being Real st y in N holds

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

existence ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for y being Real st y in N holds

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

ex b

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

proof end;

uniqueness for b

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

b

proof end;

:: deftheorem Def9 defines hpartdiff22 PDIFF_3:def 9 :

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`22_in z holds

for b_{3} being Real holds

( b_{3} = hpartdiff22 (f,z) iff ex x0, y0 being Real st

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b_{3} = L . 1 & ( for y being Real st y in N holds

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

for f being PartFunc of (REAL 2),REAL

for z being Element of REAL 2 st f is_hpartial_differentiable`22_in z holds

for b

( b

( z = <*x0,y0*> & ex N being Neighbourhood of y0 st

( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st

( b

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

theorem :: PDIFF_3:1

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds

SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds

SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0

proof end;

theorem :: PDIFF_3:2

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds

SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds

SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0

proof end;

theorem :: PDIFF_3:3

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds

SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds

SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0

proof end;

theorem :: PDIFF_3:4

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds

SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds

SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0

proof end;

theorem Th5: :: PDIFF_3:5

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds

hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0)

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds

hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0)

proof end;

theorem Th6: :: PDIFF_3:6

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds

hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0)

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds

hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0)

proof end;

theorem Th7: :: PDIFF_3:7

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds

hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0)

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds

hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0)

proof end;

theorem Th8: :: PDIFF_3:8

for x0, y0 being Real

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds

hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0)

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds

hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0)

proof end;

definition

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

let Z be set ;

end;
let Z be set ;

pred f is_hpartial_differentiable`11_on Z means :Def10: :: PDIFF_3:def 10

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`11_in z ) );

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`11_in z ) );

pred f is_hpartial_differentiable`12_on Z means :Def11: :: PDIFF_3:def 11

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`12_in z ) );

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`12_in z ) );

pred f is_hpartial_differentiable`21_on Z means :Def12: :: PDIFF_3:def 12

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`21_in z ) );

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`21_in z ) );

pred f is_hpartial_differentiable`22_on Z means :Def13: :: PDIFF_3:def 13

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`22_in z ) );

( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`22_in z ) );

:: deftheorem Def10 defines is_hpartial_differentiable`11_on PDIFF_3:def 10 :

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`11_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`11_in z ) ) );

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`11_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`11_in z ) ) );

:: deftheorem Def11 defines is_hpartial_differentiable`12_on PDIFF_3:def 11 :

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`12_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`12_in z ) ) );

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`12_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`12_in z ) ) );

:: deftheorem Def12 defines is_hpartial_differentiable`21_on PDIFF_3:def 12 :

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`21_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`21_in z ) ) );

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`21_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`21_in z ) ) );

:: deftheorem Def13 defines is_hpartial_differentiable`22_on PDIFF_3:def 13 :

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`22_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`22_in z ) ) );

for f being PartFunc of (REAL 2),REAL

for Z being set holds

( f is_hpartial_differentiable`22_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds

f | Z is_hpartial_differentiable`22_in z ) ) );

definition

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

let Z be set ;

assume A1: f is_hpartial_differentiable`11_on Z ;

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

( dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

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

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

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

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

b_{1} = b_{2}

end;
let Z be set ;

assume A1: f is_hpartial_differentiable`11_on Z ;

func f `hpartial11| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 14

( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

existence ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `hpartial11| PDIFF_3:def 14 :

for f being PartFunc of (REAL 2),REAL

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

for b_{3} being PartFunc of (REAL 2),REAL holds

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

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

for f being PartFunc of (REAL 2),REAL

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

for b

( b

b

definition

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

let Z be set ;

assume A1: f is_hpartial_differentiable`12_on Z ;

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

( dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

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

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

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

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

b_{1} = b_{2}

end;
let Z be set ;

assume A1: f is_hpartial_differentiable`12_on Z ;

func f `hpartial12| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 15

( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

existence ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `hpartial12| PDIFF_3:def 15 :

for f being PartFunc of (REAL 2),REAL

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

for b_{3} being PartFunc of (REAL 2),REAL holds

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

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

for f being PartFunc of (REAL 2),REAL

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

for b

( b

b

definition

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

let Z be set ;

assume A1: f is_hpartial_differentiable`21_on Z ;

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

( dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

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

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

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

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

b_{1} = b_{2}

end;
let Z be set ;

assume A1: f is_hpartial_differentiable`21_on Z ;

func f `hpartial21| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 16

( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

existence ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `hpartial21| PDIFF_3:def 16 :

for f being PartFunc of (REAL 2),REAL

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

for b_{3} being PartFunc of (REAL 2),REAL holds

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

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

for f being PartFunc of (REAL 2),REAL

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

for b

( b

b

definition

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

let Z be set ;

assume A1: f is_hpartial_differentiable`22_on Z ;

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

( dom b_{1} = Z & ( for z being Element of REAL 2 st z in Z holds

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

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

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

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

b_{1} = b_{2}

end;
let Z be set ;

assume A1: f is_hpartial_differentiable`22_on Z ;

func f `hpartial22| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 17

( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

existence ( dom it = Z & ( for z being Element of REAL 2 st z in Z holds

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

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines `hpartial22| PDIFF_3:def 17 :

for f being PartFunc of (REAL 2),REAL

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

for b_{3} being PartFunc of (REAL 2),REAL holds

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

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

for f being PartFunc of (REAL 2),REAL

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

for b

( b

b

begin

theorem Th9: :: PDIFF_3:9

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 )

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 )

proof end;

theorem Th10: :: PDIFF_3:10

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 )

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 )

proof end;

theorem Th11: :: PDIFF_3:11

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 )

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 )

proof end;

theorem Th12: :: PDIFF_3:12

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 )

for f being PartFunc of (REAL 2),REAL holds

( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 )

proof end;

theorem Th13: :: PDIFF_3:13

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z holds

hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1)

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z holds

hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1)

proof end;

theorem Th14: :: PDIFF_3:14

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z holds

hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2)

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z holds

hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2)

proof end;

theorem Th15: :: PDIFF_3:15

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z holds

hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1)

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z holds

hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1)

proof end;

theorem Th16: :: PDIFF_3:16

for z being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z holds

hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2)

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z holds

hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2)

proof end;

theorem :: PDIFF_3:17

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )

proof end;

theorem :: PDIFF_3:18

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )

proof end;

theorem :: PDIFF_3:19

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )

proof end;

theorem :: PDIFF_3:20

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )

for z0 being Element of REAL 2

for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds

( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )

proof end;

theorem :: PDIFF_3:21

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds

( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds

( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) )

proof end;

theorem :: PDIFF_3:22

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds

( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds

( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) )

proof end;

theorem :: PDIFF_3:23

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds

( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds

( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) )

proof end;

theorem :: PDIFF_3:24

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds

( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds

( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) )

proof end;

theorem :: PDIFF_3:25

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds

( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds

( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) )

proof end;

theorem :: PDIFF_3:26

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds

( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds

( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) )

proof end;

theorem :: PDIFF_3:27

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds

( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds

( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) )

proof end;

theorem :: PDIFF_3:28

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds

( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) )

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds

( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) )

proof end;

theorem :: PDIFF_3:29

for r being Real

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds

( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) )

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds

( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) )

proof end;

theorem :: PDIFF_3:30

for r being Real

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds

( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) )

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds

( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) )

proof end;

theorem :: PDIFF_3:31

for r being Real

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds

( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) )

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds

( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) )

proof end;

theorem :: PDIFF_3:32

for r being Real

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds

( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) )

for z0 being Element of REAL 2

for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds

( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) )

proof end;

theorem :: PDIFF_3:33

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds

(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds

(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1

proof end;

theorem :: PDIFF_3:34

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds

(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds

(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2

proof end;

theorem :: PDIFF_3:35

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds

(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds

(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1

proof end;

theorem :: PDIFF_3:36

for z0 being Element of REAL 2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds

(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2

for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds

(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2

proof end;

theorem :: PDIFF_3:37

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2 st f is_hpartial_differentiable`11_in z0 holds

SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0

for z0 being Element of REAL 2 st f is_hpartial_differentiable`11_in z0 holds

SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0

proof end;

theorem :: PDIFF_3:38

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2 st f is_hpartial_differentiable`12_in z0 holds

SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0

for z0 being Element of REAL 2 st f is_hpartial_differentiable`12_in z0 holds

SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0

proof end;

theorem :: PDIFF_3:39

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2 st f is_hpartial_differentiable`21_in z0 holds

SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0

for z0 being Element of REAL 2 st f is_hpartial_differentiable`21_in z0 holds

SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0

proof end;

theorem :: PDIFF_3:40

for f being PartFunc of (REAL 2),REAL

for z0 being Element of REAL 2 st f is_hpartial_differentiable`22_in z0 holds

SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0

for z0 being Element of REAL 2 st f is_hpartial_differentiable`22_in z0 holds

SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0

proof end;