PDIFF_5

:: Second-order Partial Differentiation of Real Ternary Functions
::  by Takao Inou\'e
::
:: Received January 26, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, ARYTM_1, FINSEQ_1, RELAT_1, ORDINAL2, SEQ_1, SEQ_2,
      RCOMP_1, PARTFUN1, FDIFF_1, PDIFF_1, ARYTM_3, FCONT_1, PDIFF_2, PDIFF_3,
      PDIFF_5, NUMBERS, SUBSET_1, CARD_1, REAL_1, TARSKI, XXREAL_0, VALUED_1,
      CARD_3, FUNCT_2, XXREAL_1, VALUED_0, NAT_1, FUNCT_7;
 notations TARSKI, SUBSET_1, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS,
      REAL_1, VALUED_0, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, VALUED_1, SEQ_1,
      SEQ_2, FINSEQ_1, RCOMP_1, EUCLID, FDIFF_1, FCONT_1, FINSEQ_2, PDIFF_1,
      PDIFF_2, PDIFF_3;
 constructors REAL_1, SEQ_2, RCOMP_1, FDIFF_1, FCONT_1, PDIFF_1, PDIFF_2,
      RELSET_1, PDIFF_3, RVSUM_1, BINOP_2, COMSEQ_2, COMPLEX1;
 registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
      VALUED_0, VALUED_1, PDIFF_3, EUCLID, ORDINAL1;
 requirements SUBSET, REAL, NUMERALS, ARITHM;
 equalities RCOMP_1, XBOOLE_0;
 expansions XBOOLE_0;
 theorems TARSKI, XBOOLE_1, XREAL_1, RCOMP_1, SEQ_4, SEQ_1, SEQ_2, FINSEQ_1,
      FINSEQ_2, RFUNCT_2, PARTFUN1, FDIFF_1, VALUED_1, XCMPLX_0, XCMPLX_1,
      FUNCT_2, VALUED_0, ORDINAL1, PDIFF_1, PDIFF_4, XREAL_0;
 schemes SEQ_1;

begin :: Second-order Partial Derivatives

reserve x,x0,x1,y,y0,y1,z,z0,z1,r,r1,s,p,p1 for Real;
reserve u,u0 for Element of REAL 3;
reserve n for Element of NAT;
reserve s1 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL 3,REAL;
reserve R,R1 for RestFunc;
reserve L,L1 for LinearFunc;

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
  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,R st for x 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
  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,R st for y 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
  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,R st for z 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
  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,R st for x 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
  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,R st for y 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
  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,R st for z 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
  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,R st for x 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
  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,R st for y 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
  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,R st for z 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 :Def10:
  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,R st it = L.1 & for x 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
    N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x 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)
    by A1;
    consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x 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)
    by A2;
    consider L,R such that
A4: for x 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5
    .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for x 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) and
A7:  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,R st s = L.1 & for x 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1),u) &
     ex L,R st r = L.1 & for x 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)
     by A6;
     consider N being Neighbourhood of x0 such that
A9:  N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st r = L.1 & for x 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) by A8;
     consider L,R such that
A10: r = L.1 & for x 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) by A9;
     consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
     ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,1),u) &
     ex L,R st s = L.1 & for x st x in N holds
     SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1
     = L.(x-x1) + R.(x-x1) by A7;
     consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(1,pdiff1(f,1),u) &
     ex L,R st s = L.1 & for x st x in N1 holds
     SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1
     = L.(x-x1) + R.(x-x1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
     SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L1.(x-x1) + R1.(x-x1)
     by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let x;
       assume
  A20: x in N & x in N1;
       then SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x0
       = L.(x-x0) + R.(x-x0) by A10;
       then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
       then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
       hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end;
     then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: x0+g/(n+2) < x0+g by XREAL_1:6;
    x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27;
       take x0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: for n being Nat holds r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n
     proof let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex x st x in N & x in N1 & h.n = x-x0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence thesis by RFUNCT_2:1;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`12_in u;
  func hpartdiff12(f,u) -> Real means :Def11:
  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,R st it = L.1 & for y 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
    N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y 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)
    by A1;
    consider N being Neighbourhood of y0 such that
A3: N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y 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)
    by A2;
    consider L,R such that
A4: for y 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5 .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for y 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) and
A7:  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,R st s = L.1 & for y 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1),u) &
     ex L,R st r = L.1 & for y 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)
     by A6;
     consider N being Neighbourhood of y0 such that
A9:  N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st r = L.1 & for y 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) by A8;
     consider L,R such that
A10: r = L.1 & for y 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) by A9;
     consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
     ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,1),u) &
     ex L,R st s = L.1 & for y st y in N holds
     SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1
     = L.(y-y1) + R.(y-y1) by A7;
     consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF1(2,pdiff1(f,1),u) &
     ex L,R st s = L.1 & for y st y in N1 holds
     SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1
     = L.(y-y1) + R.(y-y1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
     SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1
     = L1.(y-y1) + R1.(y-y1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let y;
       assume
  A20: y in N & y in N1;
       then SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y0
       = L.(y-y0) + R.(y-y0) by A10;
       then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
       then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
       hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: y0+g/(n+2) < y0+g by XREAL_1:6;
    y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27;
       take y0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex y st y in N & y in N1 & h.n = y-y0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`13_in u;
  func hpartdiff13(f,u) -> Real means :Def12:
  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,R st it = L.1 & for z 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
    N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z 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)
    by A1;
    consider N being Neighbourhood of z0 such that
A3: N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z 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)
    by A2;
    consider L,R such that
A4: for z 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5 .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for z 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) and
A7:  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,R st s = L.1 & for z 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of z0 st N c= dom SVF1(3,pdiff1(f,1),u) &
     ex L,R st r = L.1 & for z 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)
     by A6;
     consider N being Neighbourhood of z0 such that
A9:  N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st r = L.1 & for z 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) by A8;
     consider L,R such that
A10: r = L.1 & for z 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) by A9;
     consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
     ex N being Neighbourhood of z1 st N c= dom SVF1(3,pdiff1(f,1),u) &
     ex L,R st s = L.1 & for z st z in N holds
     SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1
     = L.(z-z1) + R.(z-z1) by A7;
     consider N1 being Neighbourhood of z1 such that
A12: N1 c= dom SVF1(3,pdiff1(f,1),u) &
     ex L,R st s = L.1 & for z st z in N1 holds
     SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1
     = L.(z-z1) + R.(z-z1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for z st z in N1 holds
     SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1
     = L1.(z-z1) + R1.(z-z1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let z;
       assume
  A20: z in N & z in N1;
       then SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z0
       = L.(z-z0) + R.(z-z0) by A10;
       then L.(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A13,A18,A20;
       then r1*(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A14;
       hence r*(z-z0) + R.(z-z0) = s*(z-z0) + R1.(z-z0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of z0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex z st z in N & z in N1 & h.n = z-z0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: z0+g/(n+2) < z0+g by XREAL_1:6;
    z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: z0+g/(n+2) in ].z0-g,z0+g.[ by A27;
       take z0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex z st z in N & z in N1 & h.n = z-z0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`21_in u;
  func hpartdiff21(f,u) -> Real means :Def13:
  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,R st it = L.1 & for x 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
    N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x 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)
    by A1;
    consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x 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)
    by A2;
    consider L,R such that
A4: for x 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5
    .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for x 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) and
A7:  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,R st s = L.1 & for x 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2),u) &
     ex L,R st r = L.1 & for x 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)
     by A6;
     consider N being Neighbourhood of x0 such that
A9:  N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st r = L.1 & for x 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) by A8;
     consider L,R such that
A10: r = L.1 & for x 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) by A9;
     consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
     ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,2),u) &
     ex L,R st s = L.1 & for x st x in N holds
     SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1
     = L.(x-x1) + R.(x-x1) by A7;
     consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(1,pdiff1(f,2),u) &
     ex L,R st s = L.1 & for x st x in N1 holds
     SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1
     = L.(x-x1) + R.(x-x1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
     SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1
     = L1.(x-x1) + R1.(x-x1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let x;
       assume
  A20: x in N & x in N1;
       then SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x0
       = L.(x-x0) + R.(x-x0) by A10;
       then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
       then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
       hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: x0+g/(n+2) < x0+g by XREAL_1:6;
    x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27;
       take x0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex x st x in N & x in N1 & h.n = x-x0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A31,VALUED_1:15;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`22_in u;
  func hpartdiff22(f,u) -> Real means :Def14:
  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,R st it = L.1 & for y 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
    N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y 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)
    by A1;
    consider N being Neighbourhood of y0 such that
A3: N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y 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)
    by A2;
    consider L,R such that
A4: for y 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5 .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for y 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) and
A7:  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,R st s = L.1 & for y 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2),u) &
     ex L,R st r = L.1 & for y 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)
     by A6;
     consider N being Neighbourhood of y0 such that
A9:  N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st r = L.1 & for y 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) by A8;
     consider L,R such that
A10: r = L.1 & for y 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) by A9;
     consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
     ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,2),u) &
     ex L,R st s = L.1 & for y st y in N holds
     SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1
     = L.(y-y1) + R.(y-y1) by A7;
     consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF1(2,pdiff1(f,2),u) &
     ex L,R st s = L.1 & for y st y in N1 holds
     SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1
     = L.(y-y1) + R.(y-y1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
     SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1
     = L1.(y-y1) + R1.(y-y1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let y;
       assume
  A20: y in N & y in N1;
       then SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y0
       = L.(y-y0) + R.(y-y0) by A10;
       then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
       then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
       hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: y0+g/(n+2) < y0+g by XREAL_1:6;
    y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27;
       take y0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex y st y in N & y in N1 & h.n = y-y0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`23_in u;
  func hpartdiff23(f,u) -> Real means :Def15:
  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,R st it = L.1 & for z 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
    N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z 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)
    by A1;
    consider N being Neighbourhood of z0 such that
A3: N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z 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)
    by A2;
    consider L,R such that
A4: for z 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5 .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for z 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) and
A7:  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,R st s = L.1 & for z 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of z0 st N c= dom SVF1(3,pdiff1(f,2),u) &
     ex L,R st r = L.1 & for z 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)
     by A6;
     consider N being Neighbourhood of z0 such that
A9:  N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st r = L.1 & for z 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) by A8;
     consider L,R such that
A10: r = L.1 & for z 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) by A9;
     consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
     ex N being Neighbourhood of z1 st N c= dom SVF1(3,pdiff1(f,2),u) &
     ex L,R st s = L.1 & for z st z in N holds
     SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1
     = L.(z-z1) + R.(z-z1) by A7;
     consider N1 being Neighbourhood of z1 such that
A12: N1 c= dom SVF1(3,pdiff1(f,2),u) &
     ex L,R st s = L.1 & for z st z in N1 holds
     SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1
     = L.(z-z1) + R.(z-z1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for z st z in N1 holds
     SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1
     = L1.(z-z1) + R1.(z-z1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let z;
       assume
  A20: z in N & z in N1;
       then SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z0
       = L.(z-z0) + R.(z-z0) by A10;
       then L.(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A13,A18,A20;
       then r1*(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A14;
       hence r*(z-z0) + R.(z-z0) = s*(z-z0) + R1.(z-z0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of z0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat ;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex z st z in N & z in N1 & h.n = z-z0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: z0+g/(n+2) < z0+g by XREAL_1:6;
    z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: z0+g/(n+2) in ].z0-g,z0+g.[ by A27;
       take z0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex z st z in N & z in N1 & h.n = z-z0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`31_in u;
  func hpartdiff31(f,u) -> Real means :Def16:
  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,R st it = L.1 & for x 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
    N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x 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)
    by A1;
    consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x 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)
    by A2;
    consider L,R such that
A4: for x 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5
    .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for x 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) and
A7:  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,R st s = L.1 & for x 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,3),u) &
     ex L,R st r = L.1 & for x 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)
     by A6;
     consider N being Neighbourhood of x0 such that
A9:  N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st r = L.1 & for x 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) by A8;
     consider L,R such that
A10: r = L.1 & for x 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) by A9;
     consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
     ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,3),u) &
     ex L,R st s = L.1 & for x st x in N holds
     SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1
     = L.(x-x1) + R.(x-x1) by A7;
     consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(1,pdiff1(f,3),u) &
     ex L,R st s = L.1 & for x st x in N1 holds
     SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1
     = L.(x-x1) + R.(x-x1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
     SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1
     = L1.(x-x1) + R1.(x-x1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let x;
       assume
  A20: x in N & x in N1;
       then SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x0
       = L.(x-x0) + R.(x-x0) by A10;
       then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
       then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
       hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: x0+g/(n+2) < x0+g by XREAL_1:6;
    x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27;
       take x0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex x st x in N & x in N1 & h.n = x-x0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A31,VALUED_1:15;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`32_in u;
  func hpartdiff32(f,u) -> Real means :Def17:
  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,R st it = L.1 & for y 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
    N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y 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)
    by A1;
    consider N being Neighbourhood of y0 such that
A3: N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y 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)
    by A2;
    consider L,R such that
A4: for y 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5 .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for y 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) and
A7:  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,R st s = L.1 & for y 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,3),u) &
     ex L,R st r = L.1 & for y 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)
     by A6;
     consider N being Neighbourhood of y0 such that
A9:  N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st r = L.1 & for y 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) by A8;
     consider L,R such that
A10: r = L.1 & for y 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) by A9;
     consider x1,y1, z1 being Real such that
A11: u = <*x1,y1, z1*> &
     ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,3),u) &
     ex L,R st s = L.1 & for y st y in N holds
     SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1
     = L.(y-y1) + R.(y-y1) by A7;
     consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF1(2,pdiff1(f,3),u) &
     ex L,R st s = L.1 & for y st y in N1 holds
     SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1
     = L.(y-y1) + R.(y-y1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
     SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1
     = L1.(y-y1) + R1.(y-y1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let y;
       assume
  A20: y in N & y in N1;
       then SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y0
       = L.(y-y0) + R.(y-y0) by A10;
       then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
       then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
       hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: y0+g/(n+2) < y0+g by XREAL_1:6;
    y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27;
       take y0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex y st y in N & y in N1 & h.n = y-y0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let u be Element of REAL 3;
  assume A1: f is_hpartial_differentiable`33_in u;
  func hpartdiff33(f,u) -> Real means :Def18:
  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,R st it = L.1 & for z 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
    consider x0,y0,z0 being Real such that
A2: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
    N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z 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)
    by A1;
    consider N being Neighbourhood of z0 such that
A3: N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z 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)
    by A2;
    consider L,R such that
A4: for z 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)
    by A3;
    consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 3;
    take r;
    L.1 = r*1 by A5 .= r;
    hence thesis by A2,A3,A4;
end;
uniqueness
proof
     let r,s be Real;
     assume that
A6:  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,R st r = L.1 & for z 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) and
A7:  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,R st s = L.1 & for z 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);
     consider x0,y0,z0 being Real such that
A8:  u = <*x0,y0,z0*> &
     ex N being Neighbourhood of z0 st N c= dom SVF1(3,pdiff1(f,3),u) &
     ex L,R st r = L.1 & for z 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)
     by A6;
     consider N being Neighbourhood of z0 such that
A9:  N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st r = L.1 & for z 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) by A8;
     consider L,R such that
A10: r = L.1 & for z 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) by A9;
     consider x1,y1,z1 being Real such that
A11: u = <*x1,y1,z1*> &
     ex N being Neighbourhood of z1 st N c= dom SVF1(3,pdiff1(f,3),u) &
     ex L,R st s = L.1 & for z st z in N holds
     SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1
     = L.(z-z1) + R.(z-z1) by A7;
     consider N1 being Neighbourhood of z1 such that
A12: N1 c= dom SVF1(3,pdiff1(f,3),u) &
     ex L,R st s = L.1 & for z st z in N1 holds
     SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1
     = L.(z-z1) + R.(z-z1) by A11;
     consider L1,R1 such that
A13: s = L1.1 & for z st z in N1 holds
     SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1
     = L1.(z-z1) + R1.(z-z1) by A12;
     consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 3;
     consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 & z0 = z1 by A8,A11,FINSEQ_1:78;
A19: now let z;
       assume
  A20: z in N & z in N1;
       then SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z0
       = L.(z-z0) + R.(z-z0) by A10;
       then L.(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A13,A18,A20;
       then r1*(z-z0) + R.(z-z0) = L1.(z-z0) + R1.(z-z0) by A14;
       hence r*(z-z0) + R.(z-z0) = s*(z-z0) + R1.(z-z0) by A15,A16,A17;
     end;
     consider N0 be Neighbourhood of z0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:17;
     consider g be Real such that
A22: 0 < g & N0 = ].z0-g,z0+g.[ by RCOMP_1:def 6;
     deffunc F(Nat) = g/($1+2);
     consider s1 such that
A23: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
     now let n be Nat;
       g/(n+2) <> 0 by A22,XREAL_1:139;
       hence s1.n <> 0 by A23;
     end; then
A24: s1 is non-zero by SEQ_1:5;
     s1 is convergent & lim s1 = 0 by A23,SEQ_4:31;
     then reconsider h = s1 as 0-convergent non-zero Real_Sequence
     by A24,FDIFF_1:def 1;
A25: for n ex z st z in N & z in N1 & h.n = z-z0
     proof
       let n;
  A26: g/(n+2) > 0 by A22,XREAL_1:139;
       0+1 < n+1+1 by XREAL_1:6;
       then g/(n+2) < g/1 by A22,XREAL_1:76;then
  A27: z0+g/(n+2) < z0+g by XREAL_1:6;
    z0+-g < z0+g/(n+2) by A22,A26,XREAL_1:6;
  then A28: z0+g/(n+2) in ].z0-g,z0+g.[ by A27;
       take z0+g/(n+2);
       thus thesis by A21,A22,A23,A28;
     end;
A29:  r - s in REAL by XREAL_0:def 1;
A30: now let n be Nat;
A31:     n in NAT by ORDINAL1:def 12; then
       ex z st z in N & z in N1 & h.n = z-z0 by A25;then
  A32: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
  A33: h.n <> 0 by SEQ_1:5;
  A34: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
       by A32,XCMPLX_1:62;
  A35: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
       .= r*1 by A33,XCMPLX_1:60
       .= r;
       (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
       .= s*1 by A33,XCMPLX_1:60
       .= s;then
  A36: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A34,A35,XCMPLX_1:62;
       dom R = REAL by PARTFUN1:def 2;then
  A37: rng h c= dom R;
       dom R1 = REAL by PARTFUN1:def 2;then
  A38: rng h c= dom R1;
  A39: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R.(h.n))*(h".n) by VALUED_1:10
       .= ((R/*h).n)*(h".n) by A37,A31,FUNCT_2:108
       .= ((h")(#)(R/*h)).n by VALUED_1:5;
       (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
       .= (R1.(h.n))*(h".n) by VALUED_1:10
       .= ((R1/*h).n)*(h".n) by A38,A31,FUNCT_2:108
       .= ((h")(#)(R1/*h)).n by VALUED_1:5;
       then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A36,A39;
       hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
     end; then
A40: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18,A29;
     (((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A30;then
A41: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A40,SEQ_4:25;
A42: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
     (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
     then r-s = 0-0 by A41,A42,SEQ_2:12;
     hence thesis;
end;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u implies
  SVF1(1,pdiff1(f,1),u) is_differentiable_in x0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`11_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
    N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
    by A2;
    x0 = x1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u implies
  SVF1(2,pdiff1(f,1),u) is_differentiable_in y0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`12_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
    N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
    by A2;
    y0 = y1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u implies
  SVF1(3,pdiff1(f,1),u) is_differentiable_in z0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`13_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
    N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
    by A2;
    z0 = z1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u implies
  SVF1(1,pdiff1(f,2),u) is_differentiable_in x0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`21_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
    N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
    by A2;
    x0 = x1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u implies
  SVF1(2,pdiff1(f,2),u) is_differentiable_in y0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`22_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
    N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
    by A2;
    y0 = y1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u implies
  SVF1(3,pdiff1(f,2),u) is_differentiable_in z0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`23_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
    N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
    by A2;
    z0 = z1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u implies
  SVF1(1,pdiff1(f,3),u) is_differentiable_in x0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`31_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
    N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
    by A2;
    x0 = x1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u implies
  SVF1(2,pdiff1(f,3),u) is_differentiable_in y0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`32_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
    N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
    by A2;
    y0 = y1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u implies
  SVF1(3,pdiff1(f,3),u) is_differentiable_in z0
proof
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`33_in u;
    consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
    N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
    by A2;
    z0 = z1 by A1,A3,FINSEQ_1:78;
    hence thesis by A3,FDIFF_1:def 4;
end;

theorem Th10:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`11_in u implies
  hpartdiff11(f,u) = diff(SVF1(1,pdiff1(f,1),u),x0)
proof
    set r = hpartdiff11(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`11_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
    N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
    by A2;
    consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(1,pdiff1(f,1),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
    by A3;
    consider L,R such that
A5: for x st x in N holds
    SVF1(1,pdiff1(f,1),u).x - SVF1(1,pdiff1(f,1),u).x1 = L.(x-x1) + R.(x-x1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def10;
 SVF1(1,pdiff1(f,1),u) is_differentiable_in x0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th11:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`12_in u implies
  hpartdiff12(f,u) = diff(SVF1(2,pdiff1(f,1),u),y0)
proof
    set r = hpartdiff12(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`12_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
    N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
    by A2;
    consider N being Neighbourhood of y1 such that
A4: N c= dom SVF1(2,pdiff1(f,1),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
    by A3;
    consider L,R such that
A5: for y st y in N holds
    SVF1(2,pdiff1(f,1),u).y - SVF1(2,pdiff1(f,1),u).y1 = L.(y-y1) + R.(y-y1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def11;
 SVF1(2,pdiff1(f,1),u) is_differentiable_in y0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th12:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`13_in u implies
  hpartdiff13(f,u) = diff(SVF1(3,pdiff1(f,1),u),z0)
proof
    set r = hpartdiff13(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`13_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
    N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
    by A2;
    consider N being Neighbourhood of z1 such that
A4: N c= dom SVF1(3,pdiff1(f,1),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
    by A3;
    consider L,R such that
A5: for z st z in N holds
    SVF1(3,pdiff1(f,1),u).z - SVF1(3,pdiff1(f,1),u).z1 = L.(z-z1) + R.(z-z1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def12;
 SVF1(3,pdiff1(f,1),u) is_differentiable_in z0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th13:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`21_in u implies
  hpartdiff21(f,u) = diff(SVF1(1,pdiff1(f,2),u),x0)
proof
    set r = hpartdiff21(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`21_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
    N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
    by A2;
    consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(1,pdiff1(f,2),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
    by A3;
    consider L,R such that
A5: for x st x in N holds
    SVF1(1,pdiff1(f,2),u).x - SVF1(1,pdiff1(f,2),u).x1 = L.(x-x1) + R.(x-x1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def13;
 SVF1(1,pdiff1(f,2),u) is_differentiable_in x0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th14:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`22_in u implies
  hpartdiff22(f,u) = diff(SVF1(2,pdiff1(f,2),u),y0)
proof
    set r = hpartdiff22(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`22_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
    N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
    by A2;
    consider N being Neighbourhood of y1 such that
A4: N c= dom SVF1(2,pdiff1(f,2),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
    by A3;
    consider L,R such that
A5: for y st y in N holds
    SVF1(2,pdiff1(f,2),u).y - SVF1(2,pdiff1(f,2),u).y1 = L.(y-y1) + R.(y-y1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def14;
 SVF1(2,pdiff1(f,2),u) is_differentiable_in y0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th15:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`23_in u implies
  hpartdiff23(f,u) = diff(SVF1(3,pdiff1(f,2),u),z0)
proof
    set r = hpartdiff23(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`23_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
    N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
    by A2;
    consider N being Neighbourhood of z1 such that
A4: N c= dom SVF1(3,pdiff1(f,2),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
    by A3;
    consider L,R such that
A5: for z st z in N holds
    SVF1(3,pdiff1(f,2),u).z - SVF1(3,pdiff1(f,2),u).z1 = L.(z-z1) + R.(z-z1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def15;
 SVF1(3,pdiff1(f,2),u) is_differentiable_in z0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th16:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`31_in u implies
  hpartdiff31(f,u) = diff(SVF1(1,pdiff1(f,3),u),x0)
proof
    set r = hpartdiff31(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`31_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st
    N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
    by A2;
    consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(1,pdiff1(f,3),u) & ex L,R st for x st x in N holds
    SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
    by A3;
    consider L,R such that
A5: for x st x in N holds
    SVF1(1,pdiff1(f,3),u).x - SVF1(1,pdiff1(f,3),u).x1 = L.(x-x1) + R.(x-x1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def16;
 SVF1(1,pdiff1(f,3),u) is_differentiable_in x0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th17:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`32_in u implies
  hpartdiff32(f,u) = diff(SVF1(2,pdiff1(f,3),u),y0)
proof
    set r = hpartdiff32(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`32_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st
    N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
    by A2;
    consider N being Neighbourhood of y1 such that
A4: N c= dom SVF1(2,pdiff1(f,3),u) & ex L,R st for y st y in N holds
    SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
    by A3;
    consider L,R such that
A5: for y st y in N holds
    SVF1(2,pdiff1(f,3),u).y - SVF1(2,pdiff1(f,3),u).y1 = L.(y-y1) + R.(y-y1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def17;
 SVF1(2,pdiff1(f,3),u) is_differentiable_in y0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

theorem Th18:
  u = <*x0,y0,z0*> & f is_hpartial_differentiable`33_in u implies
  hpartdiff33(f,u) = diff(SVF1(3,pdiff1(f,3),u),z0)
proof
    set r = hpartdiff33(f,u);
    assume that
A1: u = <*x0,y0,z0*> and
A2: f is_hpartial_differentiable`33_in u;
    consider x1,y1,z1 being Real such that
A3: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st
    N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
    by A2;
    consider N being Neighbourhood of z1 such that
A4: N c= dom SVF1(3,pdiff1(f,3),u) & ex L,R st for z st z in N holds
    SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
    by A3;
    consider L,R such that
A5: for z st z in N holds
    SVF1(3,pdiff1(f,3),u).z - SVF1(3,pdiff1(f,3),u).z1 = L.(z-z1) + R.(z-z1)
    by A4;
A6: x0 = x1 & y0 = y1 & z0 = z1 by A1,A3,FINSEQ_1:78;
A7: r = L.1 by A2,A3,A4,A5,Def18;
 SVF1(3,pdiff1(f,3),u) is_differentiable_in z0 by A4,A6,FDIFF_1:def 4;
    hence thesis by A4,A5,A6,A7,FDIFF_1:def 5;
end;

definition
  let f be PartFunc of REAL 3,REAL;
  let D be set;
  pred f is_hpartial_differentiable`11_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`11_in u;
  pred f is_hpartial_differentiable`12_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`12_in u;
  pred f is_hpartial_differentiable`13_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`13_in u;
  pred f is_hpartial_differentiable`21_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`21_in u;
  pred f is_hpartial_differentiable`22_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`22_in u;
  pred f is_hpartial_differentiable`23_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`23_in u;
  pred f is_hpartial_differentiable`31_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`31_in u;
  pred f is_hpartial_differentiable`32_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`32_in u;
  pred f is_hpartial_differentiable`33_on D means
  D c= dom f & for u be Element of REAL 3 st u in D holds
  f|D is_hpartial_differentiable`33_in u;
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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff11(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff11(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u = F(u) by A2
          .= hpartdiff11(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff11(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff11(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff11(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff12(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff12(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff12(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff12(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff12(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff12(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff13(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff13(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff13(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff13(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff13(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff13(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff21(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff21(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff21(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff21(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff21(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff21(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff22(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff22(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff22(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff22(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff22(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff22(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff23(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff23(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff23(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff23(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff23(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff23(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff31(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff31(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff31(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff31(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff31(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff31(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff32(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff32(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff32(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff32(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff32(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff32(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

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
  dom it = D & for u be Element of REAL 3 st u in D holds
  it.u = hpartdiff33(f,u);
existence
proof
    defpred P[Element of REAL 3] means $1 in D;
    deffunc F(Element of REAL 3) = In(hpartdiff33(f,$1),REAL);
    consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
    for u be Element of REAL 3 st u in dom F holds F.u = F(u)
    from SEQ_1:sch 3;
    take F;
    for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D by TARSKI:def 3;
    now
      let y be object such that
  A4: y in D;
      D c= dom f by A1;
      then D is Subset of REAL 3 by XBOOLE_1:1;
      hence y in dom F by A2,A4;
    end;
    then D c= dom F by TARSKI:def 3;
    hence dom F = D by A3;
    hereby
      let u be Element of REAL 3;
      assume u in D;then
      u in dom F by A2;
      hence F.u  = F(u) by A2
          .= hpartdiff33(f,u);
    end;
end;
uniqueness
proof
    let F,G be PartFunc of REAL 3,REAL;
    assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
    F.u = hpartdiff33(f,u) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
    G.u = hpartdiff33(f,u);
    now
      let u be Element of REAL 3;
      assume
  A7: u in dom F;
      then F.u = hpartdiff33(f,u) by A5;
      hence F.u = G.u by A5,A6,A7;
    end;
    hence thesis by A5,A6,PARTFUN1:5;
end;
end;

begin :: Main Properties of Second-order Partial Derivatives

theorem Th19:
  f is_hpartial_differentiable`11_in u iff
  pdiff1(f,1) is_partial_differentiable_in u,1
by PDIFF_4:13;

theorem Th20:
  f is_hpartial_differentiable`12_in u iff
  pdiff1(f,1) is_partial_differentiable_in u,2
by PDIFF_4:14;

theorem Th21:
  f is_hpartial_differentiable`13_in u iff
  pdiff1(f,1) is_partial_differentiable_in u,3
by PDIFF_4:15;

theorem Th22:
  f is_hpartial_differentiable`21_in u iff
  pdiff1(f,2) is_partial_differentiable_in u,1
by PDIFF_4:13;

theorem Th23:
  f is_hpartial_differentiable`22_in u iff
  pdiff1(f,2) is_partial_differentiable_in u,2
by PDIFF_4:14;

theorem Th24:
  f is_hpartial_differentiable`23_in u iff
  pdiff1(f,2) is_partial_differentiable_in u,3
by PDIFF_4:15;

theorem Th25:
  f is_hpartial_differentiable`31_in u iff
  pdiff1(f,3) is_partial_differentiable_in u,1
by PDIFF_4:13;

theorem Th26:
  f is_hpartial_differentiable`32_in u iff
  pdiff1(f,3) is_partial_differentiable_in u,2
by PDIFF_4:14;

theorem Th27:
  f is_hpartial_differentiable`33_in u iff
  pdiff1(f,3) is_partial_differentiable_in u,3
by PDIFF_4:15;

theorem Th28:
  f is_hpartial_differentiable`11_in u implies
  hpartdiff11(f,u) = partdiff(pdiff1(f,1),u,1)
proof
    assume
A1: f is_hpartial_differentiable`11_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff11(f,u) = diff(SVF1(1,pdiff1(f,1),u),x0) by A1,A2,Th10
    .= partdiff(pdiff1(f,1),u,1) by A2,PDIFF_4:19;
    hence thesis;
end;

theorem Th29:
  f is_hpartial_differentiable`12_in u implies
  hpartdiff12(f,u) = partdiff(pdiff1(f,1),u,2)
proof
    assume
A1: f is_hpartial_differentiable`12_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff12(f,u) = diff(SVF1(2,pdiff1(f,1),u),y0) by A1,A2,Th11
    .= partdiff(pdiff1(f,1),u,2) by A2,PDIFF_4:20;
    hence thesis;
end;

theorem Th30:
  f is_hpartial_differentiable`13_in u implies
  hpartdiff13(f,u) = partdiff(pdiff1(f,1),u,3)
proof
    assume
A1: f is_hpartial_differentiable`13_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff13(f,u) = diff(SVF1(3,pdiff1(f,1),u),z0) by A1,A2,Th12
    .= partdiff(pdiff1(f,1),u,3) by A2,PDIFF_4:21;
    hence thesis;
end;

theorem Th31:
  f is_hpartial_differentiable`21_in u implies
  hpartdiff21(f,u) = partdiff(pdiff1(f,2),u,1)
proof
    assume
A1: f is_hpartial_differentiable`21_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff21(f,u) = diff(SVF1(1,pdiff1(f,2),u),x0) by A1,A2,Th13
    .= partdiff(pdiff1(f,2),u,1) by A2,PDIFF_4:19;
    hence thesis;
end;

theorem Th32:
  f is_hpartial_differentiable`22_in u implies
  hpartdiff22(f,u) = partdiff(pdiff1(f,2),u,2)
proof
    assume
A1: f is_hpartial_differentiable`22_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff22(f,u) = diff(SVF1(2,pdiff1(f,2),u),y0) by A1,A2,Th14
    .= partdiff(pdiff1(f,2),u,2) by A2,PDIFF_4:20;
    hence thesis;
end;

theorem Th33:
  f is_hpartial_differentiable`23_in u implies
  hpartdiff23(f,u) = partdiff(pdiff1(f,2),u,3)
proof
    assume
A1: f is_hpartial_differentiable`23_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff23(f,u) = diff(SVF1(3,pdiff1(f,2),u),z0) by A1,A2,Th15
    .= partdiff(pdiff1(f,2),u,3) by A2,PDIFF_4:21;
    hence thesis;
end;

theorem Th34:
  f is_hpartial_differentiable`31_in u implies
  hpartdiff31(f,u) = partdiff(pdiff1(f,3),u,1)
proof
    assume
A1: f is_hpartial_differentiable`31_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff31(f,u) = diff(SVF1(1,pdiff1(f,3),u),x0)
    by A1,A2,Th16
    .= partdiff(pdiff1(f,3),u,1) by A2,PDIFF_4:19;
    hence thesis;
end;

theorem Th35:
  f is_hpartial_differentiable`32_in u implies
  hpartdiff32(f,u) = partdiff(pdiff1(f,3),u,2)
proof
    assume
A1: f is_hpartial_differentiable`32_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff32(f,u) = diff(SVF1(2,pdiff1(f,3),u),y0)
    by A1,A2,Th17
    .= partdiff(pdiff1(f,3),u,2) by A2,PDIFF_4:20;
    hence thesis;
end;

theorem Th36:
  f is_hpartial_differentiable`33_in u implies
  hpartdiff33(f,u) = partdiff(pdiff1(f,3),u,3)
proof
    assume
A1: f is_hpartial_differentiable`33_in u;
    consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
    hpartdiff33(f,u) = diff(SVF1(3,pdiff1(f,3),u),z0)
    by A1,A2,Th18
    .= partdiff(pdiff1(f,3),u,3) by A2,PDIFF_4:21;
    hence thesis;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(1,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(1,pdiff1(f,1),u0)/*(h+c) - SVF1(1,pdiff1(f,1),u0)/*c)
    is convergent &
  hpartdiff11(f,u0)
  = lim (h"(#)(SVF1(1,pdiff1(f,1),u0)/*(h+c) - SVF1(1,pdiff1(f,1),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(1,3).u0;
    assume
A1: f is_hpartial_differentiable`11_in u0 & N c= dom SVF1(1,pdiff1(f,1),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(1,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,1) is_partial_differentiable_in u0,1 by A1,Th19;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,1),u0,1)
    = diff(SVF1(1,pdiff1(f,1),u0),x0) by A4,PDIFF_4:19
   .= hpartdiff11(f,u0) by A1,A4,Th10;
    hence thesis by A1,A2,A3,PDIFF_4:25;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(2,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(2,pdiff1(f,1),u0)/*(h+c) - SVF1(2,pdiff1(f,1),u0)/*c)
    is convergent &
  hpartdiff12(f,u0)
  = lim (h"(#)(SVF1(2,pdiff1(f,1),u0)/*(h+c) - SVF1(2,pdiff1(f,1),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(2,3).u0;
    assume
A1: f is_hpartial_differentiable`12_in u0 & N c= dom SVF1(2,pdiff1(f,1),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(2,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,1) is_partial_differentiable_in u0,2 by A1,Th20;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,1),u0,2)
    = diff(SVF1(2,pdiff1(f,1),u0),y0) by A4,PDIFF_4:20
   .= hpartdiff12(f,u0) by A1,A4,Th11;
    hence thesis by A1,A2,A3,PDIFF_4:26;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(3,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(3,pdiff1(f,1),u0)/*(h+c) - SVF1(3,pdiff1(f,1),u0)/*c)
    is convergent &
  hpartdiff13(f,u0)
  = lim (h"(#)(SVF1(3,pdiff1(f,1),u0)/*(h+c) - SVF1(3,pdiff1(f,1),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(3,3).u0;
    assume
A1: f is_hpartial_differentiable`13_in u0 & N c= dom SVF1(3,pdiff1(f,1),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(3,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,1) is_partial_differentiable_in u0,3 by A1,Th21;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,1),u0,3)
    = diff(SVF1(3,pdiff1(f,1),u0),z0) by A4,PDIFF_4:21
   .= hpartdiff13(f,u0) by A1,A4,Th12;
    hence thesis by A1,A2,A3,PDIFF_4:27;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(1,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(1,pdiff1(f,2),u0)/*(h+c) - SVF1(1,pdiff1(f,2),u0)/*c)
    is convergent &
  hpartdiff21(f,u0)
  = lim (h"(#)(SVF1(1,pdiff1(f,2),u0)/*(h+c) - SVF1(1,pdiff1(f,2),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(1,3).u0;
    assume
A1: f is_hpartial_differentiable`21_in u0 & N c= dom SVF1(1,pdiff1(f,2),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(1,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,2) is_partial_differentiable_in u0,1 by A1,Th22;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,2),u0,1)
    = diff(SVF1(1,pdiff1(f,2),u0),x0) by A4,PDIFF_4:19
   .= hpartdiff21(f,u0) by A1,A4,Th13;
    hence thesis by A1,A2,A3,PDIFF_4:25;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(2,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(2,pdiff1(f,2),u0)/*(h+c) - SVF1(2,pdiff1(f,2),u0)/*c)
    is convergent &
  hpartdiff22(f,u0)
  = lim (h"(#)(SVF1(2,pdiff1(f,2),u0)/*(h+c) - SVF1(2,pdiff1(f,2),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(2,3).u0;
    assume
A1: f is_hpartial_differentiable`22_in u0 & N c= dom SVF1(2,pdiff1(f,2),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(2,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,2) is_partial_differentiable_in u0,2 by A1,Th23;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,2),u0,2)
    = diff(SVF1(2,pdiff1(f,2),u0),y0) by A4,PDIFF_4:20
   .= hpartdiff22(f,u0) by A1,A4,Th14;
    hence thesis by A1,A2,A3,PDIFF_4:26;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(3,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(3,pdiff1(f,2),u0)/*(h+c) - SVF1(3,pdiff1(f,2),u0)/*c)
    is convergent &
  hpartdiff23(f,u0)
  = lim (h"(#)(SVF1(3,pdiff1(f,2),u0)/*(h+c) - SVF1(3,pdiff1(f,2),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(3,3).u0;
    assume
A1: f is_hpartial_differentiable`23_in u0 & N c= dom SVF1(3,pdiff1(f,2),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(3,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,2) is_partial_differentiable_in u0,3 by A1,Th24;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,2),u0,3)
    = diff(SVF1(3,pdiff1(f,2),u0),z0) by A4,PDIFF_4:21
   .= hpartdiff23(f,u0) by A1,A4,Th15;
    hence thesis by A1,A2,A3,PDIFF_4:27;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(1,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(1,pdiff1(f,3),u0)/*(h+c) - SVF1(1,pdiff1(f,3),u0)/*c)
    is convergent &
  hpartdiff31(f,u0)
  = lim (h"(#)(SVF1(1,pdiff1(f,3),u0)/*(h+c) - SVF1(1,pdiff1(f,3),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(1,3).u0;
    assume
A1: f is_hpartial_differentiable`31_in u0 & N c= dom SVF1(1,pdiff1(f,3),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(1,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,3) is_partial_differentiable_in u0,1 by A1,Th25;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,3),u0,1)
    = diff(SVF1(1,pdiff1(f,3),u0),x0) by A4,PDIFF_4:19
   .= hpartdiff31(f,u0) by A1,A4,Th16;
    hence thesis by A1,A2,A3,PDIFF_4:25;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(2,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(2,pdiff1(f,3),u0)/*(h+c) - SVF1(2,pdiff1(f,3),u0)/*c)
    is convergent &
  hpartdiff32(f,u0)
  = lim (h"(#)(SVF1(2,pdiff1(f,3),u0)/*(h+c) - SVF1(2,pdiff1(f,3),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(2,3).u0;
    assume
A1: f is_hpartial_differentiable`32_in u0 & N c= dom SVF1(2,pdiff1(f,3),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(2,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,3) is_partial_differentiable_in u0,2 by A1,Th26;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,3),u0,2)
    = diff(SVF1(2,pdiff1(f,3),u0),y0) by A4,PDIFF_4:20
   .= hpartdiff32(f,u0) by A1,A4,Th17;
    hence thesis by A1,A2,A3,PDIFF_4:26;
end;

theorem
  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 be 0-convergent non-zero Real_Sequence, c be constant Real_Sequence
  st rng c = {proj(3,3).u0} & rng (h+c) c= N holds
  h"(#)(SVF1(3,pdiff1(f,3),u0)/*(h+c) - SVF1(3,pdiff1(f,3),u0)/*c)
    is convergent &
  hpartdiff33(f,u0)
  = lim (h"(#)(SVF1(3,pdiff1(f,3),u0)/*(h+c) - SVF1(3,pdiff1(f,3),u0)/*c))
proof
    let u0 be Element of REAL 3;
    let N be Neighbourhood of proj(3,3).u0;
    assume
A1: f is_hpartial_differentiable`33_in u0 & N c= dom SVF1(3,pdiff1(f,3),u0);
    let h be 0-convergent non-zero Real_Sequence,
    c be constant Real_Sequence such that
A2: rng c = {proj(3,3).u0} & rng (h+c) c= N;
A3: pdiff1(f,3) is_partial_differentiable_in u0,3 by A1,Th27;
    consider x0,y0,z0 being Element of REAL such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:103;
    partdiff(pdiff1(f,3),u0,3)
    = diff(SVF1(3,pdiff1(f,3),u0),z0) by A4,PDIFF_4:21
   .= hpartdiff33(f,u0) by A1,A4,Th18;
    hence thesis by A1,A2,A3,PDIFF_4:27;
end;

theorem
  f1 is_hpartial_differentiable`11_in u0 &
  f2 is_hpartial_differentiable`11_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`11_in u0 and
A2: f2 is_hpartial_differentiable`11_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,1 by A1,Th19;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,1 by A2,Th19;then
 pdiff1(f1,1)+pdiff1(f2,1) is_partial_differentiable_in u0,1 &
    partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,1)
    = partdiff(pdiff1(f1,1),u0,1) + partdiff(pdiff1(f2,1),u0,1)
    by A3,PDIFF_1:29;
    then partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,1)
    = hpartdiff11(f1,u0) + partdiff(pdiff1(f2,1),u0,1) by A1,Th28
   .= hpartdiff11(f1,u0) + hpartdiff11(f2,u0) by A2,Th28;
    hence thesis by A3,A4,PDIFF_1:29;
end;

theorem
  f1 is_hpartial_differentiable`12_in u0 &
  f2 is_hpartial_differentiable`12_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`12_in u0 and
A2: f2 is_hpartial_differentiable`12_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,2 by A1,Th20;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,2 by A2,Th20;then
 pdiff1(f1,1)+pdiff1(f2,1) is_partial_differentiable_in u0,2 &
    partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,2)
    = partdiff(pdiff1(f1,1),u0,2) + partdiff(pdiff1(f2,1),u0,2)
    by A3,PDIFF_1:29;
    then partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,2)
    = hpartdiff12(f1,u0) + partdiff(pdiff1(f2,1),u0,2) by A1,Th29
   .= hpartdiff12(f1,u0) + hpartdiff12(f2,u0) by A2,Th29;
    hence thesis by A3,A4,PDIFF_1:29;
end;

theorem
  f1 is_hpartial_differentiable`13_in u0 &
  f2 is_hpartial_differentiable`13_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`13_in u0 and
A2: f2 is_hpartial_differentiable`13_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,3 by A1,Th21;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,3 by A2,Th21;then
 pdiff1(f1,1)+pdiff1(f2,1) is_partial_differentiable_in u0,3 &
    partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,3)
    = partdiff(pdiff1(f1,1),u0,3) + partdiff(pdiff1(f2,1),u0,3)
    by A3,PDIFF_1:29;
    then partdiff(pdiff1(f1,1)+pdiff1(f2,1),u0,3)
    = hpartdiff13(f1,u0) + partdiff(pdiff1(f2,1),u0,3) by A1,Th30
   .= hpartdiff13(f1,u0) + hpartdiff13(f2,u0) by A2,Th30;
    hence thesis by A3,A4,PDIFF_1:29;
end;

theorem
  f1 is_hpartial_differentiable`21_in u0 &
  f2 is_hpartial_differentiable`21_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`21_in u0 and
A2: f2 is_hpartial_differentiable`21_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,1 by A1,Th22;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,1 by A2,Th22;then
 pdiff1(f1,2)+pdiff1(f2,2) is_partial_differentiable_in u0,1 &
    partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,1)
    = partdiff(pdiff1(f1,2),u0,1) + partdiff(pdiff1(f2,2),u0,1)
    by A3,PDIFF_1:29;
    then partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,1)
    = hpartdiff21(f1,u0) + partdiff(pdiff1(f2,2),u0,1) by A1,Th31
   .= hpartdiff21(f1,u0) + hpartdiff21(f2,u0) by A2,Th31;
    hence thesis by A3,A4,PDIFF_1:29;
end;

theorem
  f1 is_hpartial_differentiable`22_in u0 &
  f2 is_hpartial_differentiable`22_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`22_in u0 and
A2: f2 is_hpartial_differentiable`22_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,2 by A1,Th23;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,2 by A2,Th23;then
 pdiff1(f1,2)+pdiff1(f2,2) is_partial_differentiable_in u0,2 &
    partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,2)
    = partdiff(pdiff1(f1,2),u0,2) + partdiff(pdiff1(f2,2),u0,2)
    by A3,PDIFF_1:29;
    then partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,2)
    = hpartdiff22(f1,u0) + partdiff(pdiff1(f2,2),u0,2) by A1,Th32
   .= hpartdiff22(f1,u0) + hpartdiff22(f2,u0) by A2,Th32;
    hence thesis by A3,A4,PDIFF_1:29;
end;

theorem
  f1 is_hpartial_differentiable`23_in u0 &
  f2 is_hpartial_differentiable`23_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`23_in u0 and
A2: f2 is_hpartial_differentiable`23_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,3 by A1,Th24;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,3 by A2,Th24;then
 pdiff1(f1,2)+pdiff1(f2,2) is_partial_differentiable_in u0,3 &
    partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,3)
    = partdiff(pdiff1(f1,2),u0,3) + partdiff(pdiff1(f2,2),u0,3)
    by A3,PDIFF_1:29;
    then partdiff(pdiff1(f1,2)+pdiff1(f2,2),u0,3)
    = hpartdiff23(f1,u0) + partdiff(pdiff1(f2,2),u0,3) by A1,Th33
   .= hpartdiff23(f1,u0) + hpartdiff23(f2,u0) by A2,Th33;
    hence thesis by A3,A4,PDIFF_1:29;
end;

theorem
  f1 is_hpartial_differentiable`11_in u0 &
  f2 is_hpartial_differentiable`11_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`11_in u0 and
A2: f2 is_hpartial_differentiable`11_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,1 by A1,Th19;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,1 by A2,Th19;then
 pdiff1(f1,1)-pdiff1(f2,1) is_partial_differentiable_in u0,1 &
    partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,1)
    = partdiff(pdiff1(f1,1),u0,1) - partdiff(pdiff1(f2,1),u0,1)
    by A3,PDIFF_1:31;
    then partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,1)
    = hpartdiff11(f1,u0) - partdiff(pdiff1(f2,1),u0,1) by A1,Th28
   .= hpartdiff11(f1,u0) - hpartdiff11(f2,u0) by A2,Th28;
    hence thesis by A3,A4,PDIFF_1:31;
end;

theorem
  f1 is_hpartial_differentiable`12_in u0 &
  f2 is_hpartial_differentiable`12_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`12_in u0 and
A2: f2 is_hpartial_differentiable`12_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,2 by A1,Th20;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,2 by A2,Th20;then
 pdiff1(f1,1)-pdiff1(f2,1) is_partial_differentiable_in u0,2 &
    partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,2)
    = partdiff(pdiff1(f1,1),u0,2) - partdiff(pdiff1(f2,1),u0,2)
    by A3,PDIFF_1:31;
    then partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,2)
    = hpartdiff12(f1,u0) - partdiff(pdiff1(f2,1),u0,2) by A1,Th29
   .= hpartdiff12(f1,u0) - hpartdiff12(f2,u0) by A2,Th29;
    hence thesis by A3,A4,PDIFF_1:31;
end;

theorem
  f1 is_hpartial_differentiable`13_in u0 &
  f2 is_hpartial_differentiable`13_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`13_in u0 and
A2: f2 is_hpartial_differentiable`13_in u0;
A3: pdiff1(f1,1) is_partial_differentiable_in u0,3 by A1,Th21;
A4: pdiff1(f2,1) is_partial_differentiable_in u0,3 by A2,Th21;then
 pdiff1(f1,1)-pdiff1(f2,1) is_partial_differentiable_in u0,3 &
    partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,3)
    = partdiff(pdiff1(f1,1),u0,3) - partdiff(pdiff1(f2,1),u0,3)
    by A3,PDIFF_1:31;
    then partdiff(pdiff1(f1,1)-pdiff1(f2,1),u0,3)
    = hpartdiff13(f1,u0) - partdiff(pdiff1(f2,1),u0,3) by A1,Th30
   .= hpartdiff13(f1,u0) - hpartdiff13(f2,u0) by A2,Th30;
    hence thesis by A3,A4,PDIFF_1:31;
end;

theorem
  f1 is_hpartial_differentiable`21_in u0 &
  f2 is_hpartial_differentiable`21_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`21_in u0 and
A2: f2 is_hpartial_differentiable`21_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,1 by A1,Th22;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,1 by A2,Th22;then
 pdiff1(f1,2)-pdiff1(f2,2) is_partial_differentiable_in u0,1 &
    partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,1)
    = partdiff(pdiff1(f1,2),u0,1) - partdiff(pdiff1(f2,2),u0,1)
    by A3,PDIFF_1:31;
    then partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,1)
    = hpartdiff21(f1,u0) - partdiff(pdiff1(f2,2),u0,1) by A1,Th31
   .= hpartdiff21(f1,u0) - hpartdiff21(f2,u0) by A2,Th31;
    hence thesis by A3,A4,PDIFF_1:31;
end;

theorem
  f1 is_hpartial_differentiable`22_in u0 &
  f2 is_hpartial_differentiable`22_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`22_in u0 and
A2: f2 is_hpartial_differentiable`22_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,2 by A1,Th23;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,2 by A2,Th23;then
 pdiff1(f1,2)-pdiff1(f2,2) is_partial_differentiable_in u0,2 &
    partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,2)
    = partdiff(pdiff1(f1,2),u0,2) - partdiff(pdiff1(f2,2),u0,2)
    by A3,PDIFF_1:31;
    then partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,2)
    = hpartdiff22(f1,u0) - partdiff(pdiff1(f2,2),u0,2) by A1,Th32
   .= hpartdiff22(f1,u0) - hpartdiff22(f2,u0) by A2,Th32;
    hence thesis by A3,A4,PDIFF_1:31;
end;

theorem
  f1 is_hpartial_differentiable`23_in u0 &
  f2 is_hpartial_differentiable`23_in u0 implies
  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
    assume that
A1: f1 is_hpartial_differentiable`23_in u0 and
A2: f2 is_hpartial_differentiable`23_in u0;
A3: pdiff1(f1,2) is_partial_differentiable_in u0,3 by A1,Th24;
A4: pdiff1(f2,2) is_partial_differentiable_in u0,3 by A2,Th24;then
 pdiff1(f1,2)-pdiff1(f2,2) is_partial_differentiable_in u0,3 &
    partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,3)
    = partdiff(pdiff1(f1,2),u0,3) - partdiff(pdiff1(f2,2),u0,3)
    by A3,PDIFF_1:31;
    then partdiff(pdiff1(f1,2)-pdiff1(f2,2),u0,3)
    = hpartdiff23(f1,u0) - partdiff(pdiff1(f2,2),u0,3) by A1,Th33
   .= hpartdiff23(f1,u0) - hpartdiff23(f2,u0) by A2,Th33;
    hence thesis by A3,A4,PDIFF_1:31;
end;

theorem
  f is_hpartial_differentiable`11_in u0 implies
  r(#)pdiff1(f,1) is_partial_differentiable_in u0,1 &
  partdiff((r(#)pdiff1(f,1)),u0,1) = r*hpartdiff11(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`11_in u0;
    then pdiff1(f,1) is_partial_differentiable_in u0,1 by Th19;then
    r(#)pdiff1(f,1) is_partial_differentiable_in u0,1 &
    partdiff((r(#)pdiff1(f,1)),u0,1) = r*partdiff(pdiff1(f,1),u0,1)
    by PDIFF_1:33;
    hence thesis by A1,Th28;
end;

theorem
  f is_hpartial_differentiable`12_in u0 implies
  r(#)pdiff1(f,1) is_partial_differentiable_in u0,2 &
  partdiff((r(#)pdiff1(f,1)),u0,2) = r*hpartdiff12(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`12_in u0;
    then pdiff1(f,1) is_partial_differentiable_in u0,2 by Th20;then
    r(#)pdiff1(f,1) is_partial_differentiable_in u0,2 &
    partdiff((r(#)pdiff1(f,1)),u0,2) = r*partdiff(pdiff1(f,1),u0,2)
    by PDIFF_1:33;
    hence thesis by A1,Th29;
end;

theorem
  f is_hpartial_differentiable`13_in u0 implies
  r(#)pdiff1(f,1) is_partial_differentiable_in u0,3 &
  partdiff((r(#)pdiff1(f,1)),u0,3) = r*hpartdiff13(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`13_in u0;
    then pdiff1(f,1) is_partial_differentiable_in u0,3 by Th21;then
    r(#)pdiff1(f,1) is_partial_differentiable_in u0,3 &
    partdiff((r(#)pdiff1(f,1)),u0,3) = r*partdiff(pdiff1(f,1),u0,3)
    by PDIFF_1:33;
    hence thesis by A1,Th30;
end;

theorem
  f is_hpartial_differentiable`21_in u0 implies
  r(#)pdiff1(f,2) is_partial_differentiable_in u0,1 &
  partdiff((r(#)pdiff1(f,2)),u0,1) = r*hpartdiff21(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`21_in u0;
    then pdiff1(f,2) is_partial_differentiable_in u0,1 by Th22;then
    r(#)pdiff1(f,2) is_partial_differentiable_in u0,1 &
    partdiff((r(#)pdiff1(f,2)),u0,1) = r*partdiff(pdiff1(f,2),u0,1)
    by PDIFF_1:33;
    hence thesis by A1,Th31;
end;

theorem
  f is_hpartial_differentiable`22_in u0 implies
  r(#)pdiff1(f,2) is_partial_differentiable_in u0,2 &
  partdiff((r(#)pdiff1(f,2)),u0,2) = r*hpartdiff22(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`22_in u0;
    then pdiff1(f,2) is_partial_differentiable_in u0,2 by Th23;then
    r(#)pdiff1(f,2) is_partial_differentiable_in u0,2 &
    partdiff((r(#)pdiff1(f,2)),u0,2) = r*partdiff(pdiff1(f,2),u0,2)
    by PDIFF_1:33;
    hence thesis by A1,Th32;
end;

theorem
  f is_hpartial_differentiable`23_in u0 implies
  r(#)pdiff1(f,2) is_partial_differentiable_in u0,3 &
  partdiff((r(#)pdiff1(f,2)),u0,3) = r*hpartdiff23(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`23_in u0;
    then pdiff1(f,2) is_partial_differentiable_in u0,3 by Th24;then
    r(#)pdiff1(f,2) is_partial_differentiable_in u0,3 &
    partdiff((r(#)pdiff1(f,2)),u0,3) = r*partdiff(pdiff1(f,2),u0,3)
    by PDIFF_1:33;
    hence thesis by A1,Th33;
end;

theorem
  f is_hpartial_differentiable`31_in u0 implies
  r(#)pdiff1(f,3) is_partial_differentiable_in u0,1 &
  partdiff((r(#)pdiff1(f,3)),u0,1) = r*hpartdiff31(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`31_in u0;
    then pdiff1(f,3) is_partial_differentiable_in u0,1
    by Th25;then
    r(#)pdiff1(f,3) is_partial_differentiable_in u0,1 &
    partdiff((r(#)pdiff1(f,3)),u0,1) = r*partdiff(pdiff1(f,3),u0,1)
    by PDIFF_1:33;
    hence thesis by A1,Th34;
end;

theorem
  f is_hpartial_differentiable`32_in u0 implies
  r(#)pdiff1(f,3) is_partial_differentiable_in u0,2 &
  partdiff((r(#)pdiff1(f,3)),u0,2) = r*hpartdiff32(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`32_in u0;
    then pdiff1(f,3) is_partial_differentiable_in u0,2
    by Th26;then
    r(#)pdiff1(f,3) is_partial_differentiable_in u0,2 &
    partdiff((r(#)pdiff1(f,3)),u0,2) = r*partdiff(pdiff1(f,3),u0,2)
    by PDIFF_1:33;
    hence thesis by A1,Th35;
end;

theorem
  f is_hpartial_differentiable`33_in u0 implies
  r(#)pdiff1(f,3) is_partial_differentiable_in u0,3 &
  partdiff((r(#)pdiff1(f,3)),u0,3) = r*hpartdiff33(f,u0)
proof
    assume
A1: f is_hpartial_differentiable`33_in u0;
    then pdiff1(f,3) is_partial_differentiable_in u0,3
    by Th27;then
    r(#)pdiff1(f,3) is_partial_differentiable_in u0,3 &
    partdiff((r(#)pdiff1(f,3)),u0,3) = r*partdiff(pdiff1(f,3),u0,3)
    by PDIFF_1:33;
    hence thesis by A1,Th36;
end;

theorem
  f1 is_hpartial_differentiable`11_in u0 &
  f2 is_hpartial_differentiable`11_in u0 implies
  pdiff1(f1,1)(#)pdiff1(f2,1) is_partial_differentiable_in u0,1
proof
  assume f1 is_hpartial_differentiable`11_in u0 &
  f2 is_hpartial_differentiable`11_in u0;
  then pdiff1(f1,1) is_partial_differentiable_in u0,1 &
  pdiff1(f2,1) is_partial_differentiable_in u0,1 by Th19;
  hence thesis by PDIFF_4:28;
end;

theorem
  f1 is_hpartial_differentiable`12_in u0 &
  f2 is_hpartial_differentiable`12_in u0 implies
  pdiff1(f1,1)(#)pdiff1(f2,1) is_partial_differentiable_in u0,2
proof
  assume f1 is_hpartial_differentiable`12_in u0 &
  f2 is_hpartial_differentiable`12_in u0;
  then pdiff1(f1,1) is_partial_differentiable_in u0,2 &
  pdiff1(f2,1) is_partial_differentiable_in u0,2 by Th20;
  hence thesis by PDIFF_4:29;
end;

theorem
  f1 is_hpartial_differentiable`13_in u0 &
  f2 is_hpartial_differentiable`13_in u0 implies
  pdiff1(f1,1)(#)pdiff1(f2,1) is_partial_differentiable_in u0,3
proof
  assume f1 is_hpartial_differentiable`13_in u0 &
  f2 is_hpartial_differentiable`13_in u0;
  then pdiff1(f1,1) is_partial_differentiable_in u0,3 &
  pdiff1(f2,1) is_partial_differentiable_in u0,3 by Th21;
  hence thesis by PDIFF_4:30;
end;

theorem
  f1 is_hpartial_differentiable`21_in u0 &
  f2 is_hpartial_differentiable`21_in u0 implies
  pdiff1(f1,2)(#)pdiff1(f2,2) is_partial_differentiable_in u0,1
proof
  assume f1 is_hpartial_differentiable`21_in u0 &
  f2 is_hpartial_differentiable`21_in u0;
  then pdiff1(f1,2) is_partial_differentiable_in u0,1 &
  pdiff1(f2,2) is_partial_differentiable_in u0,1 by Th22;
  hence thesis by PDIFF_4:28;
end;

theorem
  f1 is_hpartial_differentiable`22_in u0 &
  f2 is_hpartial_differentiable`22_in u0 implies
  pdiff1(f1,2)(#)pdiff1(f2,2) is_partial_differentiable_in u0,2
proof
  assume f1 is_hpartial_differentiable`22_in u0 &
  f2 is_hpartial_differentiable`22_in u0;
  then pdiff1(f1,2) is_partial_differentiable_in u0,2 &
  pdiff1(f2,2) is_partial_differentiable_in u0,2 by Th23;
  hence thesis by PDIFF_4:29;
end;

theorem
  f1 is_hpartial_differentiable`23_in u0 &
  f2 is_hpartial_differentiable`23_in u0 implies
  pdiff1(f1,2)(#)pdiff1(f2,2) is_partial_differentiable_in u0,3
proof
  assume f1 is_hpartial_differentiable`23_in u0 &
  f2 is_hpartial_differentiable`23_in u0;
  then pdiff1(f1,2) is_partial_differentiable_in u0,3 &
  pdiff1(f2,2) is_partial_differentiable_in u0,3 by Th24;
  hence thesis by PDIFF_4:30;
end;

theorem
  f1 is_hpartial_differentiable`31_in u0 &
  f2 is_hpartial_differentiable`31_in u0 implies
  pdiff1(f1,3)(#)pdiff1(f2,3) is_partial_differentiable_in u0,1
proof
  assume f1 is_hpartial_differentiable`31_in u0 &
  f2 is_hpartial_differentiable`31_in u0;
  then pdiff1(f1,3) is_partial_differentiable_in u0,1 &
  pdiff1(f2,3) is_partial_differentiable_in u0,1
  by Th25;
  hence thesis by PDIFF_4:28;
end;

theorem
  f1 is_hpartial_differentiable`32_in u0 &
  f2 is_hpartial_differentiable`32_in u0 implies
  pdiff1(f1,3)(#)pdiff1(f2,3) is_partial_differentiable_in u0,2
proof
  assume f1 is_hpartial_differentiable`32_in u0 &
  f2 is_hpartial_differentiable`32_in u0;
  then pdiff1(f1,3) is_partial_differentiable_in u0,2 &
  pdiff1(f2,3) is_partial_differentiable_in u0,2 by Th26;
  hence thesis by PDIFF_4:29;
end;

theorem
  f1 is_hpartial_differentiable`33_in u0 &
  f2 is_hpartial_differentiable`33_in u0 implies
  pdiff1(f1,3)(#)pdiff1(f2,3) is_partial_differentiable_in u0,3
proof
  assume f1 is_hpartial_differentiable`33_in u0 &
  f2 is_hpartial_differentiable`33_in u0;
  then pdiff1(f1,3) is_partial_differentiable_in u0,3 &
  pdiff1(f2,3) is_partial_differentiable_in u0,3
  by Th27;
  hence thesis by PDIFF_4:30;
end;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`11_in u0
  implies SVF1(1,pdiff1(f,1),u0) is_continuous_in proj(1,3).u0
by Th19,PDIFF_4:31;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`12_in u0
  implies SVF1(2,pdiff1(f,1),u0) is_continuous_in proj(2,3).u0
by Th20,PDIFF_4:32;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`13_in u0
  implies SVF1(3,pdiff1(f,1),u0) is_continuous_in proj(3,3).u0
by Th21,PDIFF_4:33;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`21_in u0
  implies SVF1(1,pdiff1(f,2),u0) is_continuous_in proj(1,3).u0
by Th22,PDIFF_4:31;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`22_in u0
  implies SVF1(2,pdiff1(f,2),u0) is_continuous_in proj(2,3).u0
by Th23,PDIFF_4:32;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`23_in u0
  implies SVF1(3,pdiff1(f,2),u0) is_continuous_in proj(3,3).u0
by Th24,PDIFF_4:33;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`31_in u0
  implies SVF1(1,pdiff1(f,3),u0) is_continuous_in proj(1,3).u0
by Th25,PDIFF_4:31;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`32_in u0
  implies SVF1(2,pdiff1(f,3),u0) is_continuous_in proj(2,3).u0
by Th26,PDIFF_4:32;

theorem
  for u0 being Element of REAL 3 holds f is_hpartial_differentiable`33_in u0
  implies SVF1(3,pdiff1(f,3),u0) is_continuous_in proj(3,3).u0
by Th27,PDIFF_4:33;