PDIFF_5: Second-order Partial Differentiation of Real Ternary Functions

:: Second-order Partial Differentiation of Real Ternary Functions
:: by Takao Inou\'e
::
:: Received January 26, 2010
:: Copyright (c) 2010 Association of Mizar Users

begin

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
pred f is_hpartial_differentiable`11_in u means :Def3: :: 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 LINEAR ex R being REST 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 :Def4: :: 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 LINEAR ex R being REST 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 :Def4ForZ: :: 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 LINEAR ex R being REST 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 :Def5: :: 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 LINEAR ex R being REST 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 :Def6: :: 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 LINEAR ex R being REST 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 :Def6ForZ: :: 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 LINEAR ex R being REST 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 :Def5ForSecondOrder: :: 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 LINEAR ex R being REST 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 :Def6ForSecondOrder: :: 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 LINEAR ex R being REST 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 :Def6ForZForSecondOrder: :: 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 LINEAR ex R being REST st
for z being Real st z in N holds
((SVF1 3,(pdiff1 f,3),u) . z) - ((SVF1 3,(pdiff1 f,3),u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) );

end;

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`11_in u ;
func hpartdiff11 f,u -> Real means :Def7: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines hpartdiff11 PDIFF_5:def 10 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`12_in u ;
func hpartdiff12 f,u -> Real means :Def8: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines hpartdiff12 PDIFF_5:def 11 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`13_in u ;
func hpartdiff13 f,u -> Real means :Def8ForZ: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8ForZ defines hpartdiff13 PDIFF_5:def 12 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`21_in u ;
func hpartdiff21 f,u -> Real means :Def9: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines hpartdiff21 PDIFF_5:def 13 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`22_in u ;
func hpartdiff22 f,u -> Real means :Def10: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines hpartdiff22 PDIFF_5:def 14 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`23_in u ;
func hpartdiff23 f,u -> Real means :Def10ForZ: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10ForZ defines hpartdiff23 PDIFF_5:def 15 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`31_in u ;
func hpartdiff31 f,u -> Real means :Def9ForSecondOrder: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9ForSecondOrder defines hpartdiff31 PDIFF_5:def 16 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`32_in u ;
func hpartdiff32 f,u -> Real means :Def10ForSecondOrder: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10ForSecondOrder defines hpartdiff32 PDIFF_5:def 17 :

definition

let f be PartFunc of (REAL 3),REAL ;
let u be Element of REAL 3;
assume A1: f is_hpartial_differentiable`33_in u ;
func hpartdiff33 f,u -> Real means :Def10ForZForSecondOrder: :: 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 LINEAR ex R being REST 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10ForZForSecondOrder defines hpartdiff33 PDIFF_5:def 18 :

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

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

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

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

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

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

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

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

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

proof end;

theorem Th5: :: 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

proof end;

theorem Th6: :: 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

proof end;

theorem Th6ForZ: :: 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

proof end;

theorem Th7: :: 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

proof end;

theorem Th8: :: 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

proof end;

theorem Th8ForZ: :: 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

proof end;

theorem Th7ForSecondOrder: :: 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

proof end;

theorem Th8ForSecondOrder: :: 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

proof end;

theorem Th8ForZForSecondOrder: :: 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

proof end;

definition

end;

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial11| PDIFF_5:def 28 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial12| PDIFF_5:def 29 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial13| PDIFF_5:def 30 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial21| PDIFF_5:def 31 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial22| PDIFF_5:def 32 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial23| PDIFF_5:def 33 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial31| PDIFF_5:def 34 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial32| PDIFF_5:def 35 :

definition

let f be PartFunc of (REAL 3),REAL ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines `hpartial33| PDIFF_5:def 36 :

begin

theorem Th9: :: 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 )

proof end;

theorem Th10: :: 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 )

proof end;

theorem Th10ForZ: :: 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 )

proof end;

theorem Th11: :: 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 )

proof end;

theorem Th12: :: 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 )

proof end;

theorem Th12ForZ: :: 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 )

proof end;

theorem Th11ForSecondOrder: :: 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 )

proof end;

theorem Th12ForSecondOrder: :: 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 )

proof end;

theorem Th12ForZForSecondOrder: :: 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 )

proof end;

theorem Th17: :: 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

proof end;

theorem Th18: :: 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

proof end;

theorem Th18ForZ: :: 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

proof end;

theorem Th19: :: 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

proof end;

theorem Th20: :: 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

proof end;

theorem Th20ForZ: :: 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

proof end;

theorem Th19ForSecondOrder: :: 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

proof end;

theorem Th20ForSecondOrder: :: 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

proof end;

theorem Th20ForZForSecondOrder: :: 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

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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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 convergent_to_0 Real_Sequence
for c being V20() 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) )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;