:: Second-order Partial Differentiation of Real Binary Functions
:: by Bing Xie , Xiquan Liang and Xiuzhuan Shen
::
:: Received December 16, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

registration
clusterV21() RestFunc-like  ->  total for Element of K6(K7(REAL,REAL));
coherence
 for b1 being RestFunc holds b1 is total by FDIFF_1:def_2;
end;

definition
let i be Element of NAT ;
let n be non empty Element of NAT ;
let f be PartFunc of (REAL n),REAL;
func pdiff1 (f,i) ->  Function of (REAL n),REAL means :: PDIFF_3:def 1
 for z being Element of REAL n holds it . z = partdiff (f,z,i);
existence
 ex b1 being Function of (REAL n),REAL st
for z being Element of REAL n holds b1 . z = partdiff (f,z,i)
proofend;
uniqueness
 for b1, b2 being Function of (REAL n),REAL st ( for z being Element of REAL n holds b1 . z = partdiff (f,z,i) ) & ( for z being Element of REAL n holds b2 . z = partdiff (f,z,i) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines pdiff1 PDIFF_3:def_1_:_
 for i being Element of NAT
for n being non empty Element of NAT
for f being PartFunc of (REAL n),REAL
for b4 being Function of (REAL n),REAL holds
( b4 = pdiff1 (f,i) iff for z being Element of REAL n holds b4 . z = partdiff (f,z,i) );

definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
predf is_hpartial_differentiable`11_in z means :Def2: :: PDIFF_3:def 2
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
predf is_hpartial_differentiable`12_in z means :Def3: :: PDIFF_3:def 3
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
predf is_hpartial_differentiable`21_in z means :Def4: :: PDIFF_3:def 4
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
predf is_hpartial_differentiable`22_in z means :Def5: :: PDIFF_3:def 5
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
end;

:: deftheorem Def2 defines is_hpartial_differentiable`11_in PDIFF_3:def_2_:_
 for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( f is_hpartial_differentiable`11_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) &amp; 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*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) &amp; 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*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) &amp; 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*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`11_in z ;
func hpartdiff11 (f,z) ->  Real means :Def6: :: PDIFF_3:def 6
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( it = L . 1 &amp; ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
 ex b1, x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) ) &amp; ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 &amp; ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines hpartdiff11 PDIFF_3:def_6_:_
 for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`11_in z holds
for b3 being Real holds
( b3 = hpartdiff11 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 &amp; ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`12_in z ;
func hpartdiff12 (f,z) ->  Real means :Def7: :: PDIFF_3:def 7
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( it = L . 1 &amp; ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
 ex b1, x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) ) &amp; ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 &amp; ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines hpartdiff12 PDIFF_3:def_7_:_
 for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`12_in z holds
for b3 being Real holds
( b3 = hpartdiff12 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 &amp; ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`21_in z ;
func hpartdiff21 (f,z) ->  Real means :Def8: :: PDIFF_3:def 8
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( it = L . 1 &amp; ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
 ex b1, x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) ) &amp; ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 &amp; ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines hpartdiff21 PDIFF_3:def_8_:_
 for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`21_in z holds
for b3 being Real holds
( b3 = hpartdiff21 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 &amp; ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`22_in z ;
func hpartdiff22 (f,z) ->  Real means :Def9: :: PDIFF_3:def 9
 ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( it = L . 1 &amp; ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
 ex b1, x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 &amp; ( 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)) ) ) ) ) &amp; ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 &amp; ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines hpartdiff22 PDIFF_3:def_9_:_
 for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`22_in z holds
for b3 being Real holds
( b3 = hpartdiff22 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> &amp; ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) &amp; ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 &amp; ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );

theorem :: PDIFF_3:1
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> &amp; f is_hpartial_differentiable`11_in z holds
SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0
proofend;

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*> &amp; f is_hpartial_differentiable`12_in z holds
SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0
proofend;

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*> &amp; f is_hpartial_differentiable`21_in z holds
SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0
proofend;

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*> &amp; f is_hpartial_differentiable`22_in z holds
SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0
proofend;

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*> &amp; f is_hpartial_differentiable`11_in z holds
hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0)
proofend;

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*> &amp; f is_hpartial_differentiable`12_in z holds
hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0)
proofend;

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*> &amp; f is_hpartial_differentiable`21_in z holds
hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0)
proofend;

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*> &amp; f is_hpartial_differentiable`22_in z holds
hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0)
proofend;

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
predf is_hpartial_differentiable`11_on Z means :Def10: :: PDIFF_3:def 10
( Z c= dom f &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`11_in z ) );
predf is_hpartial_differentiable`12_on Z means :Def11: :: PDIFF_3:def 11
( Z c= dom f &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`12_in z ) );
predf is_hpartial_differentiable`21_on Z means :Def12: :: PDIFF_3:def 12
( Z c= dom f &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`21_in z ) );
predf is_hpartial_differentiable`22_on Z means :Def13: :: PDIFF_3:def 13
( Z c= dom f &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`22_in z ) );
end;

:: deftheorem Def10 defines is_hpartial_differentiable`11_on PDIFF_3:def_10_:_
 for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_hpartial_differentiable`11_on Z iff ( Z c= dom f &amp; ( 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 &amp; ( 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 &amp; ( 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 &amp; ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`22_in z ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`11_on Z ;
funcf `hpartial11| Z ->  PartFunc of (REAL 2),REAL means :: PDIFF_3:def 14
( dom it = Z &amp; ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff11 (f,z) ) );
existence
 ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff11 (f,z) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff11 (f,z) ) &amp; dom b2 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff11 (f,z) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines `hpartial11| PDIFF_3:def_14_:_
 for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`11_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial11| Z iff ( dom b3 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff11 (f,z) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`12_on Z ;
funcf `hpartial12| Z ->  PartFunc of (REAL 2),REAL means :: PDIFF_3:def 15
( dom it = Z &amp; ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff12 (f,z) ) );
existence
 ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff12 (f,z) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff12 (f,z) ) &amp; dom b2 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff12 (f,z) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines `hpartial12| PDIFF_3:def_15_:_
 for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`12_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial12| Z iff ( dom b3 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff12 (f,z) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`21_on Z ;
funcf `hpartial21| Z ->  PartFunc of (REAL 2),REAL means :: PDIFF_3:def 16
( dom it = Z &amp; ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff21 (f,z) ) );
existence
 ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff21 (f,z) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff21 (f,z) ) &amp; dom b2 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff21 (f,z) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines `hpartial21| PDIFF_3:def_16_:_
 for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`21_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial21| Z iff ( dom b3 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff21 (f,z) ) ) );

definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`22_on Z ;
funcf `hpartial22| Z ->  PartFunc of (REAL 2),REAL means :: PDIFF_3:def 17
( dom it = Z &amp; ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff22 (f,z) ) );
existence
 ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff22 (f,z) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff22 (f,z) ) &amp; dom b2 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff22 (f,z) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines `hpartial22| PDIFF_3:def_17_:_
 for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`22_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial22| Z iff ( dom b3 = Z &amp; ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff22 (f,z) ) ) );

begin

theorem Th9: :: PDIFF_3:9
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 )
proofend;

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

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

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

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

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

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

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

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 &amp; 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)} &amp; rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent &amp; hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )
proofend;

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 &amp; 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)} &amp; rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent &amp; hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )
proofend;

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 &amp; 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)} &amp; rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent &amp; hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )
proofend;

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 &amp; 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)} &amp; rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent &amp; hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
proofend;

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 &amp; f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 &amp; partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 &amp; partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 &amp; partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 &amp; partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 &amp; partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 &amp; partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 &amp; partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 &amp; partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) )
proofend;

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 &amp; partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) )
proofend;

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 &amp; partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) )
proofend;

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 &amp; partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) )
proofend;

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 &amp; partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) )
proofend;

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 &amp; f2 is_hpartial_differentiable`11_in z0 holds
(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1
proofend;

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 &amp; f2 is_hpartial_differentiable`12_in z0 holds
(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2
proofend;

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 &amp; f2 is_hpartial_differentiable`21_in z0 holds
(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1
proofend;

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 &amp; f2 is_hpartial_differentiable`22_in z0 holds
(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2
proofend;

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

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

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

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