pdiff_5.miz



    begin

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

      :: PDIFF_5:def1

      pred f is_hpartial_differentiable`11_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def2

      pred f is_hpartial_differentiable`12_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def3

      pred f is_hpartial_differentiable`13_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def4

      pred f is_hpartial_differentiable`21_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def5

      pred f is_hpartial_differentiable`22_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def6

      pred f is_hpartial_differentiable`23_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def7

      pred f is_hpartial_differentiable`31_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def8

      pred f is_hpartial_differentiable`32_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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)));

      :: PDIFF_5:def9

      pred f is_hpartial_differentiable`33_in u means ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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;

      :: PDIFF_5:def10

      func hpartdiff11 (f,u) -> Real means

      : Def10: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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 be 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;

      :: PDIFF_5:def11

      func hpartdiff12 (f,u) -> Real means

      : Def11: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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;

      :: PDIFF_5:def12

      func hpartdiff13 (f,u) -> Real means

      : Def12: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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;

      :: PDIFF_5:def13

      func hpartdiff21 (f,u) -> Real means

      : Def13: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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;

      :: PDIFF_5:def14

      func hpartdiff22 (f,u) -> Real means

      : Def14: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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;

      :: PDIFF_5:def15

      func hpartdiff23 (f,u) -> Real means

      : Def15: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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;

      :: PDIFF_5:def16

      func hpartdiff31 (f,u) -> Real means

      : Def16: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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;

      :: PDIFF_5:def17

      func hpartdiff32 (f,u) -> Real means

      : Def17: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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;

      :: PDIFF_5:def18

      func hpartdiff33 (f,u) -> Real means

      : Def18: ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A2: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real st u = <*x0, y0, z0*> & ex N be 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 be Real such that

         A8: u = <*x0, y0, z0*> & ex N be 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 be 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 be Real such that

         A11: u = <*x1, y1, z1*> & ex N be 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 be 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 be 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 holds 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 :: PDIFF_5:1

    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 be 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 :: PDIFF_5:2

    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 be 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 :: PDIFF_5:3

    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 be 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 :: PDIFF_5:4

    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 be 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 :: PDIFF_5:5

    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 be 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 :: PDIFF_5:6

    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 be 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 :: PDIFF_5:7

    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 be 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 :: PDIFF_5:8

    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 be 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 :: PDIFF_5:9

    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 be 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 :: PDIFF_5:10

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:11

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:12

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:13

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:14

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:15

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:16

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:17

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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 :: PDIFF_5:18

    

     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 be Real such that

       A3: u = <*x1, y1, z1*> & ex N be 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 be 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;

      :: PDIFF_5:def19

      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;

      :: PDIFF_5:def20

      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;

      :: PDIFF_5:def21

      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;

      :: PDIFF_5:def22

      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;

      :: PDIFF_5:def23

      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;

      :: PDIFF_5:def24

      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;

      :: PDIFF_5:def25

      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;

      :: PDIFF_5:def26

      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;

      :: PDIFF_5:def27

      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;

      :: PDIFF_5:def28

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

      :: PDIFF_5:def29

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

      :: PDIFF_5:def30

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

      :: PDIFF_5:def31

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

      :: PDIFF_5:def32

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

      :: PDIFF_5:def33

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

      :: PDIFF_5:def34

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

      :: PDIFF_5:def35

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

      :: PDIFF_5:def36

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

    theorem :: PDIFF_5:19

    

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

    theorem :: PDIFF_5:20

    

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

    theorem :: PDIFF_5:21

    

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

    theorem :: PDIFF_5:22

    

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

    theorem :: PDIFF_5:23

    

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

    theorem :: PDIFF_5:24

    

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

    theorem :: PDIFF_5:25

    

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

    theorem :: PDIFF_5:26

    

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

    theorem :: PDIFF_5:27

    

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

    theorem :: PDIFF_5:28

    

     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 be 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 :: PDIFF_5:29

    

     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 be 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 :: PDIFF_5:30

    

     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 be 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 :: PDIFF_5:31

    

     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 be 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 :: PDIFF_5:32

    

     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 be 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 :: PDIFF_5:33

    

     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 be 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 :: PDIFF_5:34

    

     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 be 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 :: PDIFF_5:35

    

     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 be 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 :: PDIFF_5:36

    

     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 be 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 :: PDIFF_5:37

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:38

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:39

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:40

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:41

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:42

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:43

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:44

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:45

    for u0 be Element of ( REAL 3) holds for N be 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 be 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 :: PDIFF_5:46

    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 :: PDIFF_5:47

    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 :: PDIFF_5:48

    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 :: PDIFF_5:49

    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 :: PDIFF_5:50

    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 :: PDIFF_5:51

    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 :: PDIFF_5:52

    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 :: PDIFF_5:53

    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 :: PDIFF_5:54

    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 :: PDIFF_5:55

    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 :: PDIFF_5:56

    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 :: PDIFF_5:57

    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 :: PDIFF_5:58

    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 :: PDIFF_5:59

    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 :: PDIFF_5:60

    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 :: PDIFF_5:61

    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 :: PDIFF_5:62

    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 :: PDIFF_5:63

    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 :: PDIFF_5:64

    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 :: PDIFF_5:65

    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 :: PDIFF_5:66

    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 :: PDIFF_5:67

    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 :: PDIFF_5:68

    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 :: PDIFF_5:69

    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 :: PDIFF_5:70

    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 :: PDIFF_5:71

    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 :: PDIFF_5:72

    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 :: PDIFF_5:73

    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 :: PDIFF_5:74

    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 :: PDIFF_5:75

    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 :: PDIFF_5:76

    for u0 be 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 :: PDIFF_5:77

    for u0 be 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 :: PDIFF_5:78

    for u0 be 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 :: PDIFF_5:79

    for u0 be 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 :: PDIFF_5:80

    for u0 be 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 :: PDIFF_5:81

    for u0 be 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 :: PDIFF_5:82

    for u0 be 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 :: PDIFF_5:83

    for u0 be 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 :: PDIFF_5:84

    for u0 be 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;