pdiff_3.miz



    begin

    reserve x,x0,x1,y,y0,y1,r,r1,s,p,p1 for Real;

    reserve z,z0 for Element of ( REAL 2);

    reserve n for Element of NAT ;

    reserve s1 for Real_Sequence;

    reserve f,f1,f2 for PartFunc of ( REAL 2), REAL ;

    reserve R,R1 for RestFunc;

    reserve L,L1 for LinearFunc;

    registration

      cluster -> total for RestFunc;

      coherence by FDIFF_1:def 2;

    end

    definition

      let i be Element of NAT ;

      let n be non zero Element of NAT ;

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

      :: PDIFF_3:def1

      func pdiff1 (f,i) -> Function of ( REAL n), REAL means for z be Element of ( REAL n) holds (it . z) = ( partdiff (f,z,i));

      existence

      proof

        deffunc F( Element of ( REAL n)) = ( In (( partdiff (f,$1,i)), REAL ));

        consider g be Function of ( REAL n), REAL such that

         A1: for z be Element of ( REAL n) holds (g . z) = F(z) from FUNCT_2:sch 4;

        take g;

        let z be Element of ( REAL n);

        (g . z) = F(z) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function of ( REAL n), REAL ;

        assume that

         A2: for z be Element of ( REAL n) holds (F . z) = ( partdiff (f,z,i)) and

         A3: for z be Element of ( REAL n) holds (G . z) = ( partdiff (f,z,i));

        now

          let z be Element of ( REAL n);

          (F . z) = ( partdiff (f,z,i)) by A2;

          hence (F . z) = (G . z) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

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

      let z be Element of ( REAL 2);

      :: PDIFF_3:def2

      pred f is_hpartial_differentiable`11_in z means ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0)));

      :: PDIFF_3:def3

      pred f is_hpartial_differentiable`12_in z means ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0)));

      :: PDIFF_3:def4

      pred f is_hpartial_differentiable`21_in z means ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0)));

      :: PDIFF_3:def5

      pred f is_hpartial_differentiable`22_in z means ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0)));

    end

    definition

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

      let z be Element of ( REAL 2);

      assume

       A1: f is_hpartial_differentiable`11_in z;

      :: PDIFF_3:def6

      func hpartdiff11 (f,z) -> Real means

      : Def6: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st it = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0)));

      existence

      proof

        consider x0, y0 such that

         A2: z = <*x0, y0*> and

         A3: ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A1;

        consider N be Neighbourhood of x0 such that

         A4: N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) and

         A5: ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3;

        consider L, R such that

         A6: for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A5;

        consider r such that

         A7: for p holds (L . p) = (r * p) by FDIFF_1:def 3;

        take r;

        (L . 1) = (r * 1) by A7

        .= r;

        hence thesis by A2, A4, A6;

      end;

      uniqueness

      proof

        let r,s be Real;

        assume that

         A8: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) and

         A9: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st s = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0)));

        consider x1, y1 such that

         A10: z = <*x1, y1*> and

         A11: ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st s = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A9;

        consider N1 be Neighbourhood of x1 such that N1 c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) and

         A12: ex L, R st s = (L . 1) & for x st x in N1 holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A11;

        consider L1, R1 such that

         A13: s = (L1 . 1) and

         A14: for x st x in N1 holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x1)) = ((L1 . (x - x1)) + (R1 . (x - x1))) by A12;

        consider p1 such that

         A15: for p holds (L1 . p) = (p1 * p) by FDIFF_1:def 3;

        

         A16: s = (p1 * 1) by A13, A15;

        consider x0, y0 such that

         A17: z = <*x0, y0*> and

         A18: ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A8;

        consider N be Neighbourhood of x0 such that N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) and

         A19: ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A18;

        consider L, R such that

         A20: r = (L . 1) and

         A21: for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A19;

        consider r1 such that

         A22: for p holds (L . p) = (r1 * p) by FDIFF_1:def 3;

        

         A23: x0 = x1 by A17, A10, FINSEQ_1: 77;

        then

        consider N0 be Neighbourhood of x0 such that

         A24: N0 c= N & N0 c= N1 by RCOMP_1: 17;

        consider g be Real such that

         A25: 0 < g and

         A26: N0 = ].(x0 - g), (x0 + g).[ by RCOMP_1:def 6;

        deffunc F( Nat) = (g / ($1 + 2));

        consider s1 such that

         A27: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

        now

          let n be Nat;

          (g / (n + 2)) <> 0 by A25, XREAL_1: 139;

          hence (s1 . n) <> 0 by A27;

        end;

        then

         A28: s1 is non-zero by SEQ_1: 5;

        s1 is convergent & ( lim s1) = 0 by A27, SEQ_4: 31;

        then

        reconsider h = s1 as 0 -convergent non-zero Real_Sequence by A28, FDIFF_1:def 1;

        

         A29: for n holds ex x st x in N & x in N1 & (h . n) = (x - x0)

        proof

          let n;

          take (x0 + (g / (n + 2)));

          ( 0 + 1) < ((n + 1) + 1) by XREAL_1: 6;

          then (g / (n + 2)) < (g / 1) by A25, XREAL_1: 76;

          then

           A30: (x0 + (g / (n + 2))) < (x0 + g) by XREAL_1: 6;

          (g / (n + 2)) > 0 by A25, XREAL_1: 139;

          then (x0 + ( - g)) < (x0 + (g / (n + 2))) by A25, XREAL_1: 6;

          then (x0 + (g / (n + 2))) in ].(x0 - g), (x0 + g).[ by A30;

          hence thesis by A24, A26, A27;

        end;

        

         A31: r = (r1 * 1) by A20, A22;

         A32:

        now

          let x;

          assume that

           A33: x in N and

           A34: x in N1;

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

          then ((L . (x - x0)) + (R . (x - x0))) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A14, A23, A34;

          then ((r1 * (x - x0)) + (R . (x - x0))) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A22;

          hence ((r * (x - x0)) + (R . (x - x0))) = ((s * (x - x0)) + (R1 . (x - x0))) by A15, A31, A16;

        end;

        

         A35: (r - s) in REAL by XREAL_0:def 1;

        for n be Nat holds (r - s) = ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n)

        proof

          ( dom R1) = REAL by PARTFUN1:def 2;

          then

           A36: ( rng h) c= ( dom R1);

          let n be Nat;

          ( dom R) = REAL by PARTFUN1:def 2;

          then

           A37: ( rng h) c= ( dom R);

          

           A38: n in NAT by ORDINAL1:def 12;

          then ex x st x in N & x in N1 & (h . n) = (x - x0) by A29;

          then ((r * (h . n)) + (R . (h . n))) = ((s * (h . n)) + (R1 . (h . n))) by A32;

          then

           A39: (((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n))) = (((s * (h . n)) + (R1 . (h . n))) / (h . n)) by XCMPLX_1: 62;

          

           A40: ((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 A38, A37, FUNCT_2: 108

          .= (((h " ) (#) (R /* h)) . n) by VALUED_1: 5;

          

           A41: (h . n) <> 0 by SEQ_1: 5;

          

           A42: ((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, A36, FUNCT_2: 108

          .= (((h " ) (#) (R1 /* h)) . n) by VALUED_1: 5;

          

           A43: ((s * (h . n)) / (h . n)) = (s * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (s * 1) by A41, XCMPLX_1: 60

          .= s;

          ((r * (h . n)) / (h . n)) = (r * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (r * 1) by A41, XCMPLX_1: 60

          .= r;

          then (r + ((R . (h . n)) / (h . n))) = (s + ((R1 . (h . n)) / (h . n))) by A39, A43, XCMPLX_1: 62;

          then r = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by A40, A42;

          hence thesis by RFUNCT_2: 1;

        end;

        then (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) is constant & ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1) = (r - s) by VALUED_0:def 18, A35;

        then

         A44: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - s) by SEQ_4: 25;

        

         A45: ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0 by FDIFF_1:def 2;

        ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0 by FDIFF_1:def 2;

        then (r - s) = ( 0 - 0 ) by A44, A45, SEQ_2: 12;

        hence thesis;

      end;

    end

    definition

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

      let z be Element of ( REAL 2);

      assume

       A1: f is_hpartial_differentiable`12_in z;

      :: PDIFF_3:def7

      func hpartdiff12 (f,z) -> Real means

      : Def7: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st it = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0)));

      existence

      proof

        consider x0, y0 such that

         A2: z = <*x0, y0*> and

         A3: ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1;

        consider N be Neighbourhood of y0 such that

         A4: N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) and

         A5: ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A3;

        consider L, R such that

         A6: for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A5;

        consider r such that

         A7: for p holds (L . p) = (r * p) by FDIFF_1:def 3;

        take r;

        (L . 1) = (r * 1) by A7

        .= r;

        hence thesis by A2, A4, A6;

      end;

      uniqueness

      proof

        let r,s be Real;

        assume that

         A8: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) and

         A9: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st s = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0)));

        consider x1, y1 such that

         A10: z = <*x1, y1*> and

         A11: ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st s = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A9;

        consider N1 be Neighbourhood of y1 such that N1 c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) and

         A12: ex L, R st s = (L . 1) & for y st y in N1 holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A11;

        consider L1, R1 such that

         A13: s = (L1 . 1) and

         A14: for y st y in N1 holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y1)) = ((L1 . (y - y1)) + (R1 . (y - y1))) by A12;

        consider p1 such that

         A15: for p holds (L1 . p) = (p1 * p) by FDIFF_1:def 3;

        

         A16: s = (p1 * 1) by A13, A15;

        consider x0, y0 such that

         A17: z = <*x0, y0*> and

         A18: ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A8;

        consider N be Neighbourhood of y0 such that N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) and

         A19: ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A18;

        consider L, R such that

         A20: r = (L . 1) and

         A21: for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A19;

        consider r1 such that

         A22: for p holds (L . p) = (r1 * p) by FDIFF_1:def 3;

        

         A23: y0 = y1 by A17, A10, FINSEQ_1: 77;

        then

        consider N0 be Neighbourhood of y0 such that

         A24: N0 c= N & N0 c= N1 by RCOMP_1: 17;

        consider g be Real such that

         A25: 0 < g and

         A26: N0 = ].(y0 - g), (y0 + g).[ by RCOMP_1:def 6;

        deffunc F( Nat) = (g / ($1 + 2));

        consider s1 such that

         A27: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

        now

          let n be Nat;

          (g / (n + 2)) <> 0 by A25, XREAL_1: 139;

          hence (s1 . n) <> 0 by A27;

        end;

        then

         A28: s1 is non-zero by SEQ_1: 5;

        s1 is convergent & ( lim s1) = 0 by A27, SEQ_4: 31;

        then

        reconsider h = s1 as 0 -convergent non-zero Real_Sequence by A28, FDIFF_1:def 1;

        

         A29: for n holds ex y st y in N & y in N1 & (h . n) = (y - y0)

        proof

          let n;

          take (y0 + (g / (n + 2)));

          ( 0 + 1) < ((n + 1) + 1) by XREAL_1: 6;

          then (g / (n + 2)) < (g / 1) by A25, XREAL_1: 76;

          then

           A30: (y0 + (g / (n + 2))) < (y0 + g) by XREAL_1: 6;

          (g / (n + 2)) > 0 by A25, XREAL_1: 139;

          then (y0 + ( - g)) < (y0 + (g / (n + 2))) by A25, XREAL_1: 6;

          then (y0 + (g / (n + 2))) in ].(y0 - g), (y0 + g).[ by A30;

          hence thesis by A24, A26, A27;

        end;

        

         A31: r = (r1 * 1) by A20, A22;

         A32:

        now

          let y;

          assume that

           A33: y in N and

           A34: y in N1;

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

          then ((L . (y - y0)) + (R . (y - y0))) = ((L1 . (y - y0)) + (R1 . (y - y0))) by A14, A23, A34;

          then ((r1 * (y - y0)) + (R . (y - y0))) = ((L1 . (y - y0)) + (R1 . (y - y0))) by A22;

          hence ((r * (y - y0)) + (R . (y - y0))) = ((s * (y - y0)) + (R1 . (y - y0))) by A15, A31, A16;

        end;

        

         A35: (r - s) in REAL by XREAL_0:def 1;

        now

          ( dom R1) = REAL by PARTFUN1:def 2;

          then

           A36: ( rng h) c= ( dom R1);

          let n be Nat;

          ( dom R) = REAL by PARTFUN1:def 2;

          then

           A37: ( rng h) c= ( dom R);

          

           A38: n in NAT by ORDINAL1:def 12;

          then ex y st y in N & y in N1 & (h . n) = (y - y0) by A29;

          then ((r * (h . n)) + (R . (h . n))) = ((s * (h . n)) + (R1 . (h . n))) by A32;

          then

           A39: (((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n))) = (((s * (h . n)) + (R1 . (h . n))) / (h . n)) by XCMPLX_1: 62;

          

           A40: ((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 A38, A37, FUNCT_2: 108

          .= (((h " ) (#) (R /* h)) . n) by VALUED_1: 5;

          

           A41: (h . n) <> 0 by SEQ_1: 5;

          

           A42: ((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, A36, FUNCT_2: 108

          .= (((h " ) (#) (R1 /* h)) . n) by VALUED_1: 5;

          

           A43: ((s * (h . n)) / (h . n)) = (s * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (s * 1) by A41, XCMPLX_1: 60

          .= s;

          ((r * (h . n)) / (h . n)) = (r * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (r * 1) by A41, XCMPLX_1: 60

          .= r;

          then (r + ((R . (h . n)) / (h . n))) = (s + ((R1 . (h . n)) / (h . n))) by A39, A43, XCMPLX_1: 62;

          then r = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by A40, A42;

          hence (r - s) = ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n) by RFUNCT_2: 1;

        end;

        then (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) is constant & ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1) = (r - s) by VALUED_0:def 18, A35;

        then

         A44: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - s) by SEQ_4: 25;

        

         A45: ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0 by FDIFF_1:def 2;

        ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0 by FDIFF_1:def 2;

        then (r - s) = ( 0 - 0 ) by A44, A45, SEQ_2: 12;

        hence thesis;

      end;

    end

    definition

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

      let z be Element of ( REAL 2);

      assume

       A1: f is_hpartial_differentiable`21_in z;

      :: PDIFF_3:def8

      func hpartdiff21 (f,z) -> Real means

      : Def8: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st it = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0)));

      existence

      proof

        consider x0, y0 such that

         A2: z = <*x0, y0*> and

         A3: ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A1;

        consider N be Neighbourhood of x0 such that

         A4: N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) and

         A5: ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3;

        consider L, R such that

         A6: for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A5;

        consider r such that

         A7: for p holds (L . p) = (r * p) by FDIFF_1:def 3;

        take r;

        (L . 1) = (r * 1) by A7

        .= r;

        hence thesis by A2, A4, A6;

      end;

      uniqueness

      proof

        let r,s be Real;

        assume that

         A8: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) and

         A9: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st s = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0)));

        consider x1, y1 such that

         A10: z = <*x1, y1*> and

         A11: ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st s = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A9;

        consider N1 be Neighbourhood of x1 such that N1 c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) and

         A12: ex L, R st s = (L . 1) & for x st x in N1 holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A11;

        consider L1, R1 such that

         A13: s = (L1 . 1) and

         A14: for x st x in N1 holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x1)) = ((L1 . (x - x1)) + (R1 . (x - x1))) by A12;

        consider p1 such that

         A15: for p holds (L1 . p) = (p1 * p) by FDIFF_1:def 3;

        

         A16: s = (p1 * 1) by A13, A15;

        consider x0, y0 such that

         A17: z = <*x0, y0*> and

         A18: ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A8;

        consider N be Neighbourhood of x0 such that N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) and

         A19: ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A18;

        consider L, R such that

         A20: r = (L . 1) and

         A21: for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A19;

        consider r1 such that

         A22: for p holds (L . p) = (r1 * p) by FDIFF_1:def 3;

        

         A23: x0 = x1 by A17, A10, FINSEQ_1: 77;

        then

        consider N0 be Neighbourhood of x0 such that

         A24: N0 c= N & N0 c= N1 by RCOMP_1: 17;

        consider g be Real such that

         A25: 0 < g and

         A26: N0 = ].(x0 - g), (x0 + g).[ by RCOMP_1:def 6;

        deffunc F( Nat) = (g / ($1 + 2));

        consider s1 such that

         A27: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

        now

          let n be Nat;

          (g / (n + 2)) <> 0 by A25, XREAL_1: 139;

          hence (s1 . n) <> 0 by A27;

        end;

        then

         A28: s1 is non-zero by SEQ_1: 5;

        s1 is convergent & ( lim s1) = 0 by A27, SEQ_4: 31;

        then

        reconsider h = s1 as 0 -convergent non-zero Real_Sequence by A28, FDIFF_1:def 1;

        

         A29: for n holds ex x st x in N & x in N1 & (h . n) = (x - x0)

        proof

          let n;

          take (x0 + (g / (n + 2)));

          ( 0 + 1) < ((n + 1) + 1) by XREAL_1: 6;

          then (g / (n + 2)) < (g / 1) by A25, XREAL_1: 76;

          then

           A30: (x0 + (g / (n + 2))) < (x0 + g) by XREAL_1: 6;

          (g / (n + 2)) > 0 by A25, XREAL_1: 139;

          then (x0 + ( - g)) < (x0 + (g / (n + 2))) by A25, XREAL_1: 6;

          then (x0 + (g / (n + 2))) in ].(x0 - g), (x0 + g).[ by A30;

          hence thesis by A24, A26, A27;

        end;

        

         A31: r = (r1 * 1) by A20, A22;

         A32:

        now

          let x;

          assume that

           A33: x in N and

           A34: x in N1;

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

          then ((L . (x - x0)) + (R . (x - x0))) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A14, A23, A34;

          then ((r1 * (x - x0)) + (R . (x - x0))) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A22;

          hence ((r * (x - x0)) + (R . (x - x0))) = ((s * (x - x0)) + (R1 . (x - x0))) by A15, A31, A16;

        end;

        

         A35: (r - s) in REAL by XREAL_0:def 1;

        now

          ( dom R1) = REAL by PARTFUN1:def 2;

          then

           A36: ( rng h) c= ( dom R1);

          let n be Nat;

          ( dom R) = REAL by PARTFUN1:def 2;

          then

           A37: ( rng h) c= ( dom R);

          

           A38: n in NAT by ORDINAL1:def 12;

          then ex x st x in N & x in N1 & (h . n) = (x - x0) by A29;

          then ((r * (h . n)) + (R . (h . n))) = ((s * (h . n)) + (R1 . (h . n))) by A32;

          then

           A39: (((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n))) = (((s * (h . n)) + (R1 . (h . n))) / (h . n)) by XCMPLX_1: 62;

          

           A40: ((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 A38, A37, FUNCT_2: 108

          .= (((h " ) (#) (R /* h)) . n) by VALUED_1: 5;

          

           A41: (h . n) <> 0 by SEQ_1: 5;

          

           A42: ((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, A36, FUNCT_2: 108

          .= (((h " ) (#) (R1 /* h)) . n) by VALUED_1: 5;

          

           A43: ((s * (h . n)) / (h . n)) = (s * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (s * 1) by A41, XCMPLX_1: 60

          .= s;

          ((r * (h . n)) / (h . n)) = (r * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (r * 1) by A41, XCMPLX_1: 60

          .= r;

          then (r + ((R . (h . n)) / (h . n))) = (s + ((R1 . (h . n)) / (h . n))) by A39, A43, XCMPLX_1: 62;

          then r = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by A40, A42;

          hence (r - s) = ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n) by A38, VALUED_1: 15;

        end;

        then (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) is constant & ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1) = (r - s) by VALUED_0:def 18, A35;

        then

         A44: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - s) by SEQ_4: 25;

        

         A45: ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0 by FDIFF_1:def 2;

        ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0 by FDIFF_1:def 2;

        then (r - s) = ( 0 - 0 ) by A44, A45, SEQ_2: 12;

        hence thesis;

      end;

    end

    definition

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

      let z be Element of ( REAL 2);

      assume

       A1: f is_hpartial_differentiable`22_in z;

      :: PDIFF_3:def9

      func hpartdiff22 (f,z) -> Real means

      : Def9: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st it = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0)));

      existence

      proof

        consider x0, y0 such that

         A2: z = <*x0, y0*> and

         A3: ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1;

        consider N be Neighbourhood of y0 such that

         A4: N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) and

         A5: ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A3;

        consider L, R such that

         A6: for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A5;

        consider r such that

         A7: for p holds (L . p) = (r * p) by FDIFF_1:def 3;

        take r;

        (L . 1) = (r * 1) by A7

        .= r;

        hence thesis by A2, A4, A6;

      end;

      uniqueness

      proof

        let r,s be Real;

        assume that

         A8: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) and

         A9: ex x0, y0 st z = <*x0, y0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st s = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0)));

        consider x1, y1 such that

         A10: z = <*x1, y1*> and

         A11: ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st s = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A9;

        consider N1 be Neighbourhood of y1 such that N1 c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) and

         A12: ex L, R st s = (L . 1) & for y st y in N1 holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A11;

        consider L1, R1 such that

         A13: s = (L1 . 1) and

         A14: for y st y in N1 holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y1)) = ((L1 . (y - y1)) + (R1 . (y - y1))) by A12;

        consider p1 such that

         A15: for p holds (L1 . p) = (p1 * p) by FDIFF_1:def 3;

        

         A16: s = (p1 * 1) by A13, A15;

        consider x0, y0 such that

         A17: z = <*x0, y0*> and

         A18: ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A8;

        consider N be Neighbourhood of y0 such that N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) and

         A19: ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A18;

        consider L, R such that

         A20: r = (L . 1) and

         A21: for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A19;

        consider r1 such that

         A22: for p holds (L . p) = (r1 * p) by FDIFF_1:def 3;

        

         A23: y0 = y1 by A17, A10, FINSEQ_1: 77;

        then

        consider N0 be Neighbourhood of y0 such that

         A24: N0 c= N & N0 c= N1 by RCOMP_1: 17;

        consider g be Real such that

         A25: 0 < g and

         A26: N0 = ].(y0 - g), (y0 + g).[ by RCOMP_1:def 6;

        deffunc F( Nat) = (g / ($1 + 2));

        consider s1 such that

         A27: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

        now

          let n be Nat;

          (g / (n + 2)) <> 0 by A25, XREAL_1: 139;

          hence (s1 . n) <> 0 by A27;

        end;

        then

         A28: s1 is non-zero by SEQ_1: 5;

        s1 is convergent & ( lim s1) = 0 by A27, SEQ_4: 31;

        then

        reconsider h = s1 as 0 -convergent non-zero Real_Sequence by A28, FDIFF_1:def 1;

        

         A29: for n holds ex y st y in N & y in N1 & (h . n) = (y - y0)

        proof

          let n;

          take (y0 + (g / (n + 2)));

          ( 0 + 1) < ((n + 1) + 1) by XREAL_1: 6;

          then (g / (n + 2)) < (g / 1) by A25, XREAL_1: 76;

          then

           A30: (y0 + (g / (n + 2))) < (y0 + g) by XREAL_1: 6;

          (g / (n + 2)) > 0 by A25, XREAL_1: 139;

          then (y0 + ( - g)) < (y0 + (g / (n + 2))) by A25, XREAL_1: 6;

          then (y0 + (g / (n + 2))) in ].(y0 - g), (y0 + g).[ by A30;

          hence thesis by A24, A26, A27;

        end;

        

         A31: r = (r1 * 1) by A20, A22;

         A32:

        now

          let y;

          assume that

           A33: y in N and

           A34: y in N1;

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

          then ((L . (y - y0)) + (R . (y - y0))) = ((L1 . (y - y0)) + (R1 . (y - y0))) by A14, A23, A34;

          then ((r1 * (y - y0)) + (R . (y - y0))) = ((L1 . (y - y0)) + (R1 . (y - y0))) by A22;

          hence ((r * (y - y0)) + (R . (y - y0))) = ((s * (y - y0)) + (R1 . (y - y0))) by A15, A31, A16;

        end;

        

         A35: (r - s) in REAL by XREAL_0:def 1;

        now

          ( dom R1) = REAL by PARTFUN1:def 2;

          then

           A36: ( rng h) c= ( dom R1);

          let n be Nat;

          ( dom R) = REAL by PARTFUN1:def 2;

          then

           A37: ( rng h) c= ( dom R);

          

           A38: n in NAT by ORDINAL1:def 12;

          then ex y st y in N & y in N1 & (h . n) = (y - y0) by A29;

          then ((r * (h . n)) + (R . (h . n))) = ((s * (h . n)) + (R1 . (h . n))) by A32;

          then

           A39: (((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n))) = (((s * (h . n)) + (R1 . (h . n))) / (h . n)) by XCMPLX_1: 62;

          

           A40: ((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 A38, A37, FUNCT_2: 108

          .= (((h " ) (#) (R /* h)) . n) by VALUED_1: 5;

          

           A41: (h . n) <> 0 by SEQ_1: 5;

          

           A42: ((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, A36, FUNCT_2: 108

          .= (((h " ) (#) (R1 /* h)) . n) by VALUED_1: 5;

          

           A43: ((s * (h . n)) / (h . n)) = (s * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (s * 1) by A41, XCMPLX_1: 60

          .= s;

          ((r * (h . n)) / (h . n)) = (r * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (r * 1) by A41, XCMPLX_1: 60

          .= r;

          then (r + ((R . (h . n)) / (h . n))) = (s + ((R1 . (h . n)) / (h . n))) by A39, A43, XCMPLX_1: 62;

          then r = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by A40, A42;

          hence (r - s) = ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n) by RFUNCT_2: 1;

        end;

        then (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) is constant & ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1) = (r - s) by VALUED_0:def 18, A35;

        then

         A44: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - s) by SEQ_4: 25;

        

         A45: ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0 by FDIFF_1:def 2;

        ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0 by FDIFF_1:def 2;

        then (r - s) = ( 0 - 0 ) by A44, A45, SEQ_2: 12;

        hence thesis;

      end;

    end

    theorem :: PDIFF_3:1

    z = <*x0, y0*> & f is_hpartial_differentiable`11_in z implies ( SVF1 (1,( pdiff1 (f,1)),z)) is_differentiable_in x0

    proof

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`11_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A2;

      x0 = x1 by A1, A3, FINSEQ_1: 77;

      hence thesis by A4, FDIFF_1:def 4;

    end;

    theorem :: PDIFF_3:2

    z = <*x0, y0*> & f is_hpartial_differentiable`12_in z implies ( SVF1 (2,( pdiff1 (f,1)),z)) is_differentiable_in y0

    proof

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`12_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A2;

      y0 = y1 by A1, A3, FINSEQ_1: 77;

      hence thesis by A4, FDIFF_1:def 4;

    end;

    theorem :: PDIFF_3:3

    z = <*x0, y0*> & f is_hpartial_differentiable`21_in z implies ( SVF1 (1,( pdiff1 (f,2)),z)) is_differentiable_in x0

    proof

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`21_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A2;

      x0 = x1 by A1, A3, FINSEQ_1: 77;

      hence thesis by A4, FDIFF_1:def 4;

    end;

    theorem :: PDIFF_3:4

    z = <*x0, y0*> & f is_hpartial_differentiable`22_in z implies ( SVF1 (2,( pdiff1 (f,2)),z)) is_differentiable_in y0

    proof

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`22_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A2;

      y0 = y1 by A1, A3, FINSEQ_1: 77;

      hence thesis by A4, FDIFF_1:def 4;

    end;

    theorem :: PDIFF_3:5

    

     Th5: z = <*x0, y0*> & f is_hpartial_differentiable`11_in z implies ( hpartdiff11 (f,z)) = ( diff (( SVF1 (1,( pdiff1 (f,1)),z)),x0))

    proof

      set r = ( hpartdiff11 (f,z));

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`11_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A2;

      consider N be Neighbourhood of x1 such that

       A5: N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z))) and

       A6: ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A4;

      

       A7: x0 = x1 by A1, A3, FINSEQ_1: 77;

      then

       A8: ( SVF1 (1,( pdiff1 (f,1)),z)) is_differentiable_in x0 by A5, A6, FDIFF_1:def 4;

      consider L, R such that

       A9: for x st x in N holds ((( SVF1 (1,( pdiff1 (f,1)),z)) . x) - (( SVF1 (1,( pdiff1 (f,1)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A6;

      r = (L . 1) by A2, A3, A5, A9, Def6;

      hence thesis by A5, A9, A7, A8, FDIFF_1:def 5;

    end;

    theorem :: PDIFF_3:6

    

     Th6: z = <*x0, y0*> & f is_hpartial_differentiable`12_in z implies ( hpartdiff12 (f,z)) = ( diff (( SVF1 (2,( pdiff1 (f,1)),z)),y0))

    proof

      set r = ( hpartdiff12 (f,z));

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`12_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A2;

      consider N be Neighbourhood of y1 such that

       A5: N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z))) and

       A6: ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A4;

      

       A7: y0 = y1 by A1, A3, FINSEQ_1: 77;

      then

       A8: ( SVF1 (2,( pdiff1 (f,1)),z)) is_differentiable_in y0 by A5, A6, FDIFF_1:def 4;

      consider L, R such that

       A9: for y st y in N holds ((( SVF1 (2,( pdiff1 (f,1)),z)) . y) - (( SVF1 (2,( pdiff1 (f,1)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A6;

      r = (L . 1) by A2, A3, A5, A9, Def7;

      hence thesis by A5, A9, A7, A8, FDIFF_1:def 5;

    end;

    theorem :: PDIFF_3:7

    

     Th7: z = <*x0, y0*> & f is_hpartial_differentiable`21_in z implies ( hpartdiff21 (f,z)) = ( diff (( SVF1 (1,( pdiff1 (f,2)),z)),x0))

    proof

      set r = ( hpartdiff21 (f,z));

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`21_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) & ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A2;

      consider N be Neighbourhood of x1 such that

       A5: N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z))) and

       A6: ex L, R st for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A4;

      

       A7: x0 = x1 by A1, A3, FINSEQ_1: 77;

      then

       A8: ( SVF1 (1,( pdiff1 (f,2)),z)) is_differentiable_in x0 by A5, A6, FDIFF_1:def 4;

      consider L, R such that

       A9: for x st x in N holds ((( SVF1 (1,( pdiff1 (f,2)),z)) . x) - (( SVF1 (1,( pdiff1 (f,2)),z)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A6;

      r = (L . 1) by A2, A3, A5, A9, Def8;

      hence thesis by A5, A9, A7, A8, FDIFF_1:def 5;

    end;

    theorem :: PDIFF_3:8

    

     Th8: z = <*x0, y0*> & f is_hpartial_differentiable`22_in z implies ( hpartdiff22 (f,z)) = ( diff (( SVF1 (2,( pdiff1 (f,2)),z)),y0))

    proof

      set r = ( hpartdiff22 (f,z));

      assume that

       A1: z = <*x0, y0*> and

       A2: f is_hpartial_differentiable`22_in z;

      consider x1, y1 such that

       A3: z = <*x1, y1*> and

       A4: ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) & ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A2;

      consider N be Neighbourhood of y1 such that

       A5: N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z))) and

       A6: ex L, R st for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A4;

      

       A7: y0 = y1 by A1, A3, FINSEQ_1: 77;

      then

       A8: ( SVF1 (2,( pdiff1 (f,2)),z)) is_differentiable_in y0 by A5, A6, FDIFF_1:def 4;

      consider L, R such that

       A9: for y st y in N holds ((( SVF1 (2,( pdiff1 (f,2)),z)) . y) - (( SVF1 (2,( pdiff1 (f,2)),z)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A6;

      r = (L . 1) by A2, A3, A5, A9, Def9;

      hence thesis by A5, A9, A7, A8, FDIFF_1:def 5;

    end;

    definition

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

      let Z be set;

      :: PDIFF_3:def10

      pred f is_hpartial_differentiable`11_on Z means Z c= ( dom f) & for z be Element of ( REAL 2) st z in Z holds (f | Z) is_hpartial_differentiable`11_in z;

      :: PDIFF_3:def11

      pred f is_hpartial_differentiable`12_on Z means Z c= ( dom f) & for z be Element of ( REAL 2) st z in Z holds (f | Z) is_hpartial_differentiable`12_in z;

      :: PDIFF_3:def12

      pred f is_hpartial_differentiable`21_on Z means Z c= ( dom f) & for z be Element of ( REAL 2) st z in Z holds (f | Z) is_hpartial_differentiable`21_in z;

      :: PDIFF_3:def13

      pred f is_hpartial_differentiable`22_on Z means Z c= ( dom f) & for z be Element of ( REAL 2) st z in Z holds (f | Z) is_hpartial_differentiable`22_in z;

    end

    definition

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

      let Z be set;

      assume

       A1: f is_hpartial_differentiable`11_on Z;

      :: PDIFF_3:def14

      func f `hpartial11| Z -> PartFunc of ( REAL 2), REAL means ( dom it ) = Z & for z be Element of ( REAL 2) st z in Z holds (it . z) = ( hpartdiff11 (f,z));

      existence

      proof

        deffunc F( Element of ( REAL 2)) = ( In (( hpartdiff11 (f,$1)), REAL ));

        defpred P[ Element of ( REAL 2)] means $1 in Z;

        consider F be PartFunc of ( REAL 2), REAL such that

         A2: (for z be Element of ( REAL 2) holds z in ( dom F) iff P[z]) & for z be Element of ( REAL 2) st z in ( dom F) holds (F . z) = F(z) from SEQ_1:sch 3;

        take F;

        now

          Z c= ( dom f) by A1;

          then

           A3: Z is Subset of ( REAL 2) by XBOOLE_1: 1;

          let y be object;

          assume y in Z;

          hence y in ( dom F) by A2, A3;

        end;

        then

         A4: Z c= ( dom F) by TARSKI:def 3;

        for y be object st y in ( dom F) holds y in Z by A2;

        then ( dom F) c= Z by TARSKI:def 3;

        hence ( dom F) = Z by A4, XBOOLE_0:def 10;

        hereby

          let z be Element of ( REAL 2);

          assume z in Z;

          then z in ( dom F) by A2;

          

          hence (F . z) = F(z) by A2

          .= ( hpartdiff11 (f,z));

        end;

      end;

      uniqueness

      proof

        let F,G be PartFunc of ( REAL 2), REAL ;

        assume that

         A5: ( dom F) = Z and

         A6: for z be Element of ( REAL 2) st z in Z holds (F . z) = ( hpartdiff11 (f,z)) and

         A7: ( dom G) = Z and

         A8: for z be Element of ( REAL 2) st z in Z holds (G . z) = ( hpartdiff11 (f,z));

        now

          let z be Element of ( REAL 2);

          assume

           A9: z in ( dom F);

          then (F . z) = ( hpartdiff11 (f,z)) by A5, A6;

          hence (F . z) = (G . z) by A5, A8, A9;

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

    definition

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

      let Z be set;

      assume

       A1: f is_hpartial_differentiable`12_on Z;

      :: PDIFF_3:def15

      func f `hpartial12| Z -> PartFunc of ( REAL 2), REAL means ( dom it ) = Z & for z be Element of ( REAL 2) st z in Z holds (it . z) = ( hpartdiff12 (f,z));

      existence

      proof

        deffunc F( Element of ( REAL 2)) = ( In (( hpartdiff12 (f,$1)), REAL ));

        defpred P[ Element of ( REAL 2)] means $1 in Z;

        consider F be PartFunc of ( REAL 2), REAL such that

         A2: (for z be Element of ( REAL 2) holds z in ( dom F) iff P[z]) & for z be Element of ( REAL 2) st z in ( dom F) holds (F . z) = F(z) from SEQ_1:sch 3;

        take F;

        now

          Z c= ( dom f) by A1;

          then

           A3: Z is Subset of ( REAL 2) by XBOOLE_1: 1;

          let y be object;

          assume y in Z;

          hence y in ( dom F) by A2, A3;

        end;

        then

         A4: Z c= ( dom F) by TARSKI:def 3;

        for y be object st y in ( dom F) holds y in Z by A2;

        then ( dom F) c= Z by TARSKI:def 3;

        hence ( dom F) = Z by A4, XBOOLE_0:def 10;

        hereby

          let z be Element of ( REAL 2);

          assume z in Z;

          then z in ( dom F) by A2;

          

          hence (F . z) = F(z) by A2

          .= ( hpartdiff12 (f,z));

        end;

      end;

      uniqueness

      proof

        let F,G be PartFunc of ( REAL 2), REAL ;

        assume that

         A5: ( dom F) = Z and

         A6: for z be Element of ( REAL 2) st z in Z holds (F . z) = ( hpartdiff12 (f,z)) and

         A7: ( dom G) = Z and

         A8: for z be Element of ( REAL 2) st z in Z holds (G . z) = ( hpartdiff12 (f,z));

        now

          let z be Element of ( REAL 2);

          assume

           A9: z in ( dom F);

          then (F . z) = ( hpartdiff12 (f,z)) by A5, A6;

          hence (F . z) = (G . z) by A5, A8, A9;

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

    definition

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

      let Z be set;

      assume

       A1: f is_hpartial_differentiable`21_on Z;

      :: PDIFF_3:def16

      func f `hpartial21| Z -> PartFunc of ( REAL 2), REAL means ( dom it ) = Z & for z be Element of ( REAL 2) st z in Z holds (it . z) = ( hpartdiff21 (f,z));

      existence

      proof

        deffunc F( Element of ( REAL 2)) = ( In (( hpartdiff21 (f,$1)), REAL ));

        defpred P[ Element of ( REAL 2)] means $1 in Z;

        consider F be PartFunc of ( REAL 2), REAL such that

         A2: (for z be Element of ( REAL 2) holds z in ( dom F) iff P[z]) & for z be Element of ( REAL 2) st z in ( dom F) holds (F . z) = F(z) from SEQ_1:sch 3;

        take F;

        now

          Z c= ( dom f) by A1;

          then

           A3: Z is Subset of ( REAL 2) by XBOOLE_1: 1;

          let y be object;

          assume y in Z;

          hence y in ( dom F) by A2, A3;

        end;

        then

         A4: Z c= ( dom F) by TARSKI:def 3;

        for y be object st y in ( dom F) holds y in Z by A2;

        then ( dom F) c= Z by TARSKI:def 3;

        hence ( dom F) = Z by A4, XBOOLE_0:def 10;

        hereby

          let z be Element of ( REAL 2);

          assume z in Z;

          then z in ( dom F) by A2;

          

          hence (F . z) = F(z) by A2

          .= ( hpartdiff21 (f,z));

        end;

      end;

      uniqueness

      proof

        let F,G be PartFunc of ( REAL 2), REAL ;

        assume that

         A5: ( dom F) = Z and

         A6: for z be Element of ( REAL 2) st z in Z holds (F . z) = ( hpartdiff21 (f,z)) and

         A7: ( dom G) = Z and

         A8: for z be Element of ( REAL 2) st z in Z holds (G . z) = ( hpartdiff21 (f,z));

        now

          let z be Element of ( REAL 2);

          assume

           A9: z in ( dom F);

          then (F . z) = ( hpartdiff21 (f,z)) by A5, A6;

          hence (F . z) = (G . z) by A5, A8, A9;

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

    definition

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

      let Z be set;

      assume

       A1: f is_hpartial_differentiable`22_on Z;

      :: PDIFF_3:def17

      func f `hpartial22| Z -> PartFunc of ( REAL 2), REAL means ( dom it ) = Z & for z be Element of ( REAL 2) st z in Z holds (it . z) = ( hpartdiff22 (f,z));

      existence

      proof

        deffunc F( Element of ( REAL 2)) = ( In (( hpartdiff22 (f,$1)), REAL ));

        defpred P[ Element of ( REAL 2)] means $1 in Z;

        consider F be PartFunc of ( REAL 2), REAL such that

         A2: (for z be Element of ( REAL 2) holds z in ( dom F) iff P[z]) & for z be Element of ( REAL 2) st z in ( dom F) holds (F . z) = F(z) from SEQ_1:sch 3;

        take F;

        now

          Z c= ( dom f) by A1;

          then

           A3: Z is Subset of ( REAL 2) by XBOOLE_1: 1;

          let y be object;

          assume y in Z;

          hence y in ( dom F) by A2, A3;

        end;

        then

         A4: Z c= ( dom F) by TARSKI:def 3;

        for y be object st y in ( dom F) holds y in Z by A2;

        then ( dom F) c= Z by TARSKI:def 3;

        hence ( dom F) = Z by A4, XBOOLE_0:def 10;

        hereby

          let z be Element of ( REAL 2);

          assume z in Z;

          then z in ( dom F) by A2;

          

          hence (F . z) = F(z) by A2

          .= ( hpartdiff22 (f,z));

        end;

      end;

      uniqueness

      proof

        let F,G be PartFunc of ( REAL 2), REAL ;

        assume that

         A5: ( dom F) = Z and

         A6: for z be Element of ( REAL 2) st z in Z holds (F . z) = ( hpartdiff22 (f,z)) and

         A7: ( dom G) = Z and

         A8: for z be Element of ( REAL 2) st z in Z holds (G . z) = ( hpartdiff22 (f,z));

        now

          let z be Element of ( REAL 2);

          assume

           A9: z in ( dom F);

          then (F . z) = ( hpartdiff22 (f,z)) by A5, A6;

          hence (F . z) = (G . z) by A5, A8, A9;

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

    begin

    theorem :: PDIFF_3:9

    

     Th9: f is_hpartial_differentiable`11_in z iff ( pdiff1 (f,1)) is_partial_differentiable_in (z,1) by PDIFF_2: 9;

    theorem :: PDIFF_3:10

    

     Th10: f is_hpartial_differentiable`12_in z iff ( pdiff1 (f,1)) is_partial_differentiable_in (z,2) by PDIFF_2: 10;

    theorem :: PDIFF_3:11

    

     Th11: f is_hpartial_differentiable`21_in z iff ( pdiff1 (f,2)) is_partial_differentiable_in (z,1) by PDIFF_2: 9;

    theorem :: PDIFF_3:12

    

     Th12: f is_hpartial_differentiable`22_in z iff ( pdiff1 (f,2)) is_partial_differentiable_in (z,2) by PDIFF_2: 10;

    theorem :: PDIFF_3:13

    

     Th13: f is_hpartial_differentiable`11_in z implies ( hpartdiff11 (f,z)) = ( partdiff (( pdiff1 (f,1)),z,1))

    proof

      consider x0,y0 be Element of REAL such that

       A1: z = <*x0, y0*> by FINSEQ_2: 100;

      assume

       A2: f is_hpartial_differentiable`11_in z;

      then

       A3: ( pdiff1 (f,1)) is_partial_differentiable_in (z,1) by Th9;

      ( hpartdiff11 (f,z)) = ( diff (( SVF1 (1,( pdiff1 (f,1)),z)),x0)) by A2, A1, Th5

      .= ( partdiff (( pdiff1 (f,1)),z,1)) by A1, A3, PDIFF_2: 13;

      hence thesis;

    end;

    theorem :: PDIFF_3:14

    

     Th14: f is_hpartial_differentiable`12_in z implies ( hpartdiff12 (f,z)) = ( partdiff (( pdiff1 (f,1)),z,2))

    proof

      consider x0,y0 be Element of REAL such that

       A1: z = <*x0, y0*> by FINSEQ_2: 100;

      assume

       A2: f is_hpartial_differentiable`12_in z;

      then

       A3: ( pdiff1 (f,1)) is_partial_differentiable_in (z,2) by Th10;

      ( hpartdiff12 (f,z)) = ( diff (( SVF1 (2,( pdiff1 (f,1)),z)),y0)) by A2, A1, Th6

      .= ( partdiff (( pdiff1 (f,1)),z,2)) by A1, A3, PDIFF_2: 14;

      hence thesis;

    end;

    theorem :: PDIFF_3:15

    

     Th15: f is_hpartial_differentiable`21_in z implies ( hpartdiff21 (f,z)) = ( partdiff (( pdiff1 (f,2)),z,1))

    proof

      consider x0,y0 be Element of REAL such that

       A1: z = <*x0, y0*> by FINSEQ_2: 100;

      assume

       A2: f is_hpartial_differentiable`21_in z;

      then

       A3: ( pdiff1 (f,2)) is_partial_differentiable_in (z,1) by Th11;

      ( hpartdiff21 (f,z)) = ( diff (( SVF1 (1,( pdiff1 (f,2)),z)),x0)) by A2, A1, Th7

      .= ( partdiff (( pdiff1 (f,2)),z,1)) by A1, A3, PDIFF_2: 13;

      hence thesis;

    end;

    theorem :: PDIFF_3:16

    

     Th16: f is_hpartial_differentiable`22_in z implies ( hpartdiff22 (f,z)) = ( partdiff (( pdiff1 (f,2)),z,2))

    proof

      consider x0,y0 be Element of REAL such that

       A1: z = <*x0, y0*> by FINSEQ_2: 100;

      assume

       A2: f is_hpartial_differentiable`22_in z;

      then

       A3: ( pdiff1 (f,2)) is_partial_differentiable_in (z,2) by Th12;

      ( hpartdiff22 (f,z)) = ( diff (( SVF1 (2,( pdiff1 (f,2)),z)),y0)) by A2, A1, Th8

      .= ( partdiff (( pdiff1 (f,2)),z,2)) by A1, A3, PDIFF_2: 14;

      hence thesis;

    end;

    theorem :: PDIFF_3:17

    for z0 be Element of ( REAL 2) holds for N be Neighbourhood of (( proj (1,2)) . z0) st f is_hpartial_differentiable`11_in z0 & N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z0))) holds for h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence st ( rng c) = {(( proj (1,2)) . z0)} & ( rng (h + c)) c= N holds ((h " ) (#) ((( SVF1 (1,( pdiff1 (f,1)),z0)) /* (h + c)) - (( SVF1 (1,( pdiff1 (f,1)),z0)) /* c))) is convergent & ( hpartdiff11 (f,z0)) = ( lim ((h " ) (#) ((( SVF1 (1,( pdiff1 (f,1)),z0)) /* (h + c)) - (( SVF1 (1,( pdiff1 (f,1)),z0)) /* c))))

    proof

      let z0 be Element of ( REAL 2);

      let N be Neighbourhood of (( proj (1,2)) . z0);

      assume that

       A1: f is_hpartial_differentiable`11_in z0 and

       A2: N c= ( dom ( SVF1 (1,( pdiff1 (f,1)),z0)));

      let h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence such that

       A3: ( rng c) = {(( proj (1,2)) . z0)} & ( rng (h + c)) c= N;

      consider x0,y0 be Element of REAL such that

       A4: z0 = <*x0, y0*> by FINSEQ_2: 100;

      

       A5: ( pdiff1 (f,1)) is_partial_differentiable_in (z0,1) by A1, Th9;

      

      then ( partdiff (( pdiff1 (f,1)),z0,1)) = ( diff (( SVF1 (1,( pdiff1 (f,1)),z0)),x0)) by A4, PDIFF_2: 13

      .= ( hpartdiff11 (f,z0)) by A1, A4, Th5;

      hence thesis by A2, A3, A5, PDIFF_2: 17;

    end;

    theorem :: PDIFF_3:18

    for z0 be Element of ( REAL 2) holds for N be Neighbourhood of (( proj (2,2)) . z0) st f is_hpartial_differentiable`12_in z0 & N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z0))) holds for h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence st ( rng c) = {(( proj (2,2)) . z0)} & ( rng (h + c)) c= N holds ((h " ) (#) ((( SVF1 (2,( pdiff1 (f,1)),z0)) /* (h + c)) - (( SVF1 (2,( pdiff1 (f,1)),z0)) /* c))) is convergent & ( hpartdiff12 (f,z0)) = ( lim ((h " ) (#) ((( SVF1 (2,( pdiff1 (f,1)),z0)) /* (h + c)) - (( SVF1 (2,( pdiff1 (f,1)),z0)) /* c))))

    proof

      let z0 be Element of ( REAL 2);

      let N be Neighbourhood of (( proj (2,2)) . z0);

      assume that

       A1: f is_hpartial_differentiable`12_in z0 and

       A2: N c= ( dom ( SVF1 (2,( pdiff1 (f,1)),z0)));

      let h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence such that

       A3: ( rng c) = {(( proj (2,2)) . z0)} & ( rng (h + c)) c= N;

      consider x0,y0 be Element of REAL such that

       A4: z0 = <*x0, y0*> by FINSEQ_2: 100;

      

       A5: ( pdiff1 (f,1)) is_partial_differentiable_in (z0,2) by A1, Th10;

      

      then ( partdiff (( pdiff1 (f,1)),z0,2)) = ( diff (( SVF1 (2,( pdiff1 (f,1)),z0)),y0)) by A4, PDIFF_2: 14

      .= ( hpartdiff12 (f,z0)) by A1, A4, Th6;

      hence thesis by A2, A3, A5, PDIFF_2: 18;

    end;

    theorem :: PDIFF_3:19

    for z0 be Element of ( REAL 2) holds for N be Neighbourhood of (( proj (1,2)) . z0) st f is_hpartial_differentiable`21_in z0 & N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z0))) holds for h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence st ( rng c) = {(( proj (1,2)) . z0)} & ( rng (h + c)) c= N holds ((h " ) (#) ((( SVF1 (1,( pdiff1 (f,2)),z0)) /* (h + c)) - (( SVF1 (1,( pdiff1 (f,2)),z0)) /* c))) is convergent & ( hpartdiff21 (f,z0)) = ( lim ((h " ) (#) ((( SVF1 (1,( pdiff1 (f,2)),z0)) /* (h + c)) - (( SVF1 (1,( pdiff1 (f,2)),z0)) /* c))))

    proof

      let z0 be Element of ( REAL 2);

      let N be Neighbourhood of (( proj (1,2)) . z0);

      assume that

       A1: f is_hpartial_differentiable`21_in z0 and

       A2: N c= ( dom ( SVF1 (1,( pdiff1 (f,2)),z0)));

      let h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence such that

       A3: ( rng c) = {(( proj (1,2)) . z0)} & ( rng (h + c)) c= N;

      consider x0,y0 be Element of REAL such that

       A4: z0 = <*x0, y0*> by FINSEQ_2: 100;

      

       A5: ( pdiff1 (f,2)) is_partial_differentiable_in (z0,1) by A1, Th11;

      

      then ( partdiff (( pdiff1 (f,2)),z0,1)) = ( diff (( SVF1 (1,( pdiff1 (f,2)),z0)),x0)) by A4, PDIFF_2: 13

      .= ( hpartdiff21 (f,z0)) by A1, A4, Th7;

      hence thesis by A2, A3, A5, PDIFF_2: 17;

    end;

    theorem :: PDIFF_3:20

    for z0 be Element of ( REAL 2) holds for N be Neighbourhood of (( proj (2,2)) . z0) st f is_hpartial_differentiable`22_in z0 & N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z0))) holds for h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence st ( rng c) = {(( proj (2,2)) . z0)} & ( rng (h + c)) c= N holds ((h " ) (#) ((( SVF1 (2,( pdiff1 (f,2)),z0)) /* (h + c)) - (( SVF1 (2,( pdiff1 (f,2)),z0)) /* c))) is convergent & ( hpartdiff22 (f,z0)) = ( lim ((h " ) (#) ((( SVF1 (2,( pdiff1 (f,2)),z0)) /* (h + c)) - (( SVF1 (2,( pdiff1 (f,2)),z0)) /* c))))

    proof

      let z0 be Element of ( REAL 2);

      let N be Neighbourhood of (( proj (2,2)) . z0);

      assume that

       A1: f is_hpartial_differentiable`22_in z0 and

       A2: N c= ( dom ( SVF1 (2,( pdiff1 (f,2)),z0)));

      let h be 0 -convergent non-zero Real_Sequence, c be constant Real_Sequence such that

       A3: ( rng c) = {(( proj (2,2)) . z0)} & ( rng (h + c)) c= N;

      consider x0,y0 be Element of REAL such that

       A4: z0 = <*x0, y0*> by FINSEQ_2: 100;

      

       A5: ( pdiff1 (f,2)) is_partial_differentiable_in (z0,2) by A1, Th12;

      

      then ( partdiff (( pdiff1 (f,2)),z0,2)) = ( diff (( SVF1 (2,( pdiff1 (f,2)),z0)),y0)) by A4, PDIFF_2: 14

      .= ( hpartdiff22 (f,z0)) by A1, A4, Th8;

      hence thesis by A2, A3, A5, PDIFF_2: 18;

    end;

    theorem :: PDIFF_3:21

    f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies (( pdiff1 (f1,1)) + ( pdiff1 (f2,1))) is_partial_differentiable_in (z0,1) & ( partdiff ((( pdiff1 (f1,1)) + ( pdiff1 (f2,1))),z0,1)) = (( hpartdiff11 (f1,z0)) + ( hpartdiff11 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`11_in z0 and

       A2: f2 is_hpartial_differentiable`11_in z0;

      

       A3: ( pdiff1 (f1,1)) is_partial_differentiable_in (z0,1) & ( pdiff1 (f2,1)) is_partial_differentiable_in (z0,1) by A1, A2, Th9;

      then ( partdiff ((( pdiff1 (f1,1)) + ( pdiff1 (f2,1))),z0,1)) = (( partdiff (( pdiff1 (f1,1)),z0,1)) + ( partdiff (( pdiff1 (f2,1)),z0,1))) by PDIFF_1: 29;

      

      then ( partdiff ((( pdiff1 (f1,1)) + ( pdiff1 (f2,1))),z0,1)) = (( hpartdiff11 (f1,z0)) + ( partdiff (( pdiff1 (f2,1)),z0,1))) by A1, Th13

      .= (( hpartdiff11 (f1,z0)) + ( hpartdiff11 (f2,z0))) by A2, Th13;

      hence thesis by A3, PDIFF_1: 29;

    end;

    theorem :: PDIFF_3:22

    f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies (( pdiff1 (f1,1)) + ( pdiff1 (f2,1))) is_partial_differentiable_in (z0,2) & ( partdiff ((( pdiff1 (f1,1)) + ( pdiff1 (f2,1))),z0,2)) = (( hpartdiff12 (f1,z0)) + ( hpartdiff12 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`12_in z0 and

       A2: f2 is_hpartial_differentiable`12_in z0;

      

       A3: ( pdiff1 (f1,1)) is_partial_differentiable_in (z0,2) & ( pdiff1 (f2,1)) is_partial_differentiable_in (z0,2) by A1, A2, Th10;

      then ( partdiff ((( pdiff1 (f1,1)) + ( pdiff1 (f2,1))),z0,2)) = (( partdiff (( pdiff1 (f1,1)),z0,2)) + ( partdiff (( pdiff1 (f2,1)),z0,2))) by PDIFF_1: 29;

      

      then ( partdiff ((( pdiff1 (f1,1)) + ( pdiff1 (f2,1))),z0,2)) = (( hpartdiff12 (f1,z0)) + ( partdiff (( pdiff1 (f2,1)),z0,2))) by A1, Th14

      .= (( hpartdiff12 (f1,z0)) + ( hpartdiff12 (f2,z0))) by A2, Th14;

      hence thesis by A3, PDIFF_1: 29;

    end;

    theorem :: PDIFF_3:23

    f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies (( pdiff1 (f1,2)) + ( pdiff1 (f2,2))) is_partial_differentiable_in (z0,1) & ( partdiff ((( pdiff1 (f1,2)) + ( pdiff1 (f2,2))),z0,1)) = (( hpartdiff21 (f1,z0)) + ( hpartdiff21 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`21_in z0 and

       A2: f2 is_hpartial_differentiable`21_in z0;

      

       A3: ( pdiff1 (f1,2)) is_partial_differentiable_in (z0,1) & ( pdiff1 (f2,2)) is_partial_differentiable_in (z0,1) by A1, A2, Th11;

      then ( partdiff ((( pdiff1 (f1,2)) + ( pdiff1 (f2,2))),z0,1)) = (( partdiff (( pdiff1 (f1,2)),z0,1)) + ( partdiff (( pdiff1 (f2,2)),z0,1))) by PDIFF_1: 29;

      

      then ( partdiff ((( pdiff1 (f1,2)) + ( pdiff1 (f2,2))),z0,1)) = (( hpartdiff21 (f1,z0)) + ( partdiff (( pdiff1 (f2,2)),z0,1))) by A1, Th15

      .= (( hpartdiff21 (f1,z0)) + ( hpartdiff21 (f2,z0))) by A2, Th15;

      hence thesis by A3, PDIFF_1: 29;

    end;

    theorem :: PDIFF_3:24

    f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies (( pdiff1 (f1,2)) + ( pdiff1 (f2,2))) is_partial_differentiable_in (z0,2) & ( partdiff ((( pdiff1 (f1,2)) + ( pdiff1 (f2,2))),z0,2)) = (( hpartdiff22 (f1,z0)) + ( hpartdiff22 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`22_in z0 and

       A2: f2 is_hpartial_differentiable`22_in z0;

      

       A3: ( pdiff1 (f1,2)) is_partial_differentiable_in (z0,2) & ( pdiff1 (f2,2)) is_partial_differentiable_in (z0,2) by A1, A2, Th12;

      then ( partdiff ((( pdiff1 (f1,2)) + ( pdiff1 (f2,2))),z0,2)) = (( partdiff (( pdiff1 (f1,2)),z0,2)) + ( partdiff (( pdiff1 (f2,2)),z0,2))) by PDIFF_1: 29;

      

      then ( partdiff ((( pdiff1 (f1,2)) + ( pdiff1 (f2,2))),z0,2)) = (( hpartdiff22 (f1,z0)) + ( partdiff (( pdiff1 (f2,2)),z0,2))) by A1, Th16

      .= (( hpartdiff22 (f1,z0)) + ( hpartdiff22 (f2,z0))) by A2, Th16;

      hence thesis by A3, PDIFF_1: 29;

    end;

    theorem :: PDIFF_3:25

    f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies (( pdiff1 (f1,1)) - ( pdiff1 (f2,1))) is_partial_differentiable_in (z0,1) & ( partdiff ((( pdiff1 (f1,1)) - ( pdiff1 (f2,1))),z0,1)) = (( hpartdiff11 (f1,z0)) - ( hpartdiff11 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`11_in z0 and

       A2: f2 is_hpartial_differentiable`11_in z0;

      

       A3: ( pdiff1 (f1,1)) is_partial_differentiable_in (z0,1) & ( pdiff1 (f2,1)) is_partial_differentiable_in (z0,1) by A1, A2, Th9;

      then ( partdiff ((( pdiff1 (f1,1)) - ( pdiff1 (f2,1))),z0,1)) = (( partdiff (( pdiff1 (f1,1)),z0,1)) - ( partdiff (( pdiff1 (f2,1)),z0,1))) by PDIFF_1: 31;

      

      then ( partdiff ((( pdiff1 (f1,1)) - ( pdiff1 (f2,1))),z0,1)) = (( hpartdiff11 (f1,z0)) - ( partdiff (( pdiff1 (f2,1)),z0,1))) by A1, Th13

      .= (( hpartdiff11 (f1,z0)) - ( hpartdiff11 (f2,z0))) by A2, Th13;

      hence thesis by A3, PDIFF_1: 31;

    end;

    theorem :: PDIFF_3:26

    f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies (( pdiff1 (f1,1)) - ( pdiff1 (f2,1))) is_partial_differentiable_in (z0,2) & ( partdiff ((( pdiff1 (f1,1)) - ( pdiff1 (f2,1))),z0,2)) = (( hpartdiff12 (f1,z0)) - ( hpartdiff12 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`12_in z0 and

       A2: f2 is_hpartial_differentiable`12_in z0;

      

       A3: ( pdiff1 (f1,1)) is_partial_differentiable_in (z0,2) & ( pdiff1 (f2,1)) is_partial_differentiable_in (z0,2) by A1, A2, Th10;

      then ( partdiff ((( pdiff1 (f1,1)) - ( pdiff1 (f2,1))),z0,2)) = (( partdiff (( pdiff1 (f1,1)),z0,2)) - ( partdiff (( pdiff1 (f2,1)),z0,2))) by PDIFF_1: 31;

      

      then ( partdiff ((( pdiff1 (f1,1)) - ( pdiff1 (f2,1))),z0,2)) = (( hpartdiff12 (f1,z0)) - ( partdiff (( pdiff1 (f2,1)),z0,2))) by A1, Th14

      .= (( hpartdiff12 (f1,z0)) - ( hpartdiff12 (f2,z0))) by A2, Th14;

      hence thesis by A3, PDIFF_1: 31;

    end;

    theorem :: PDIFF_3:27

    f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies (( pdiff1 (f1,2)) - ( pdiff1 (f2,2))) is_partial_differentiable_in (z0,1) & ( partdiff ((( pdiff1 (f1,2)) - ( pdiff1 (f2,2))),z0,1)) = (( hpartdiff21 (f1,z0)) - ( hpartdiff21 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`21_in z0 and

       A2: f2 is_hpartial_differentiable`21_in z0;

      

       A3: ( pdiff1 (f1,2)) is_partial_differentiable_in (z0,1) & ( pdiff1 (f2,2)) is_partial_differentiable_in (z0,1) by A1, A2, Th11;

      then ( partdiff ((( pdiff1 (f1,2)) - ( pdiff1 (f2,2))),z0,1)) = (( partdiff (( pdiff1 (f1,2)),z0,1)) - ( partdiff (( pdiff1 (f2,2)),z0,1))) by PDIFF_1: 31;

      

      then ( partdiff ((( pdiff1 (f1,2)) - ( pdiff1 (f2,2))),z0,1)) = (( hpartdiff21 (f1,z0)) - ( partdiff (( pdiff1 (f2,2)),z0,1))) by A1, Th15

      .= (( hpartdiff21 (f1,z0)) - ( hpartdiff21 (f2,z0))) by A2, Th15;

      hence thesis by A3, PDIFF_1: 31;

    end;

    theorem :: PDIFF_3:28

    f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies (( pdiff1 (f1,2)) - ( pdiff1 (f2,2))) is_partial_differentiable_in (z0,2) & ( partdiff ((( pdiff1 (f1,2)) - ( pdiff1 (f2,2))),z0,2)) = (( hpartdiff22 (f1,z0)) - ( hpartdiff22 (f2,z0)))

    proof

      assume that

       A1: f1 is_hpartial_differentiable`22_in z0 and

       A2: f2 is_hpartial_differentiable`22_in z0;

      

       A3: ( pdiff1 (f1,2)) is_partial_differentiable_in (z0,2) & ( pdiff1 (f2,2)) is_partial_differentiable_in (z0,2) by A1, A2, Th12;

      then ( partdiff ((( pdiff1 (f1,2)) - ( pdiff1 (f2,2))),z0,2)) = (( partdiff (( pdiff1 (f1,2)),z0,2)) - ( partdiff (( pdiff1 (f2,2)),z0,2))) by PDIFF_1: 31;

      

      then ( partdiff ((( pdiff1 (f1,2)) - ( pdiff1 (f2,2))),z0,2)) = (( hpartdiff22 (f1,z0)) - ( partdiff (( pdiff1 (f2,2)),z0,2))) by A1, Th16

      .= (( hpartdiff22 (f1,z0)) - ( hpartdiff22 (f2,z0))) by A2, Th16;

      hence thesis by A3, PDIFF_1: 31;

    end;

    theorem :: PDIFF_3:29

    f is_hpartial_differentiable`11_in z0 implies (r (#) ( pdiff1 (f,1))) is_partial_differentiable_in (z0,1) & ( partdiff ((r (#) ( pdiff1 (f,1))),z0,1)) = (r * ( hpartdiff11 (f,z0)))

    proof

      assume

       A1: f is_hpartial_differentiable`11_in z0;

      reconsider r as Real;

      

       A2: ( pdiff1 (f,1)) is_partial_differentiable_in (z0,1) by Th9, A1;

      then ( partdiff ((r (#) ( pdiff1 (f,1))),z0,1)) = (r * ( partdiff (( pdiff1 (f,1)),z0,1))) by PDIFF_1: 33;

      hence thesis by A1, A2, Th13, PDIFF_1: 33;

    end;

    theorem :: PDIFF_3:30

    f is_hpartial_differentiable`12_in z0 implies (r (#) ( pdiff1 (f,1))) is_partial_differentiable_in (z0,2) & ( partdiff ((r (#) ( pdiff1 (f,1))),z0,2)) = (r * ( hpartdiff12 (f,z0)))

    proof

      assume

       A1: f is_hpartial_differentiable`12_in z0;

      reconsider r as Real;

      

       A2: ( pdiff1 (f,1)) is_partial_differentiable_in (z0,2) by Th10, A1;

      ( partdiff ((r (#) ( pdiff1 (f,1))),z0,2)) = (r * ( partdiff (( pdiff1 (f,1)),z0,2))) by PDIFF_1: 33, A2;

      hence thesis by A1, A2, Th14, PDIFF_1: 33;

    end;

    theorem :: PDIFF_3:31

    f is_hpartial_differentiable`21_in z0 implies (r (#) ( pdiff1 (f,2))) is_partial_differentiable_in (z0,1) & ( partdiff ((r (#) ( pdiff1 (f,2))),z0,1)) = (r * ( hpartdiff21 (f,z0)))

    proof

      assume

       A1: f is_hpartial_differentiable`21_in z0;

      reconsider r as Real;

      

       A2: ( pdiff1 (f,2)) is_partial_differentiable_in (z0,1) by Th11, A1;

      ( partdiff ((r (#) ( pdiff1 (f,2))),z0,1)) = (r * ( partdiff (( pdiff1 (f,2)),z0,1))) by PDIFF_1: 33, A2;

      hence thesis by A1, A2, Th15, PDIFF_1: 33;

    end;

    theorem :: PDIFF_3:32

    f is_hpartial_differentiable`22_in z0 implies (r (#) ( pdiff1 (f,2))) is_partial_differentiable_in (z0,2) & ( partdiff ((r (#) ( pdiff1 (f,2))),z0,2)) = (r * ( hpartdiff22 (f,z0)))

    proof

      assume

       A1: f is_hpartial_differentiable`22_in z0;

      then

       A2: ( pdiff1 (f,2)) is_partial_differentiable_in (z0,2) by Th12;

      reconsider r as Real;

      ( partdiff ((r (#) ( pdiff1 (f,2))),z0,2)) = (r * ( partdiff (( pdiff1 (f,2)),z0,2))) by PDIFF_1: 33, A2;

      hence thesis by A1, A2, Th16, PDIFF_1: 33;

    end;

    theorem :: PDIFF_3:33

    f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies (( pdiff1 (f1,1)) (#) ( pdiff1 (f2,1))) is_partial_differentiable_in (z0,1)

    proof

      assume f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0;

      then ( pdiff1 (f1,1)) is_partial_differentiable_in (z0,1) & ( pdiff1 (f2,1)) is_partial_differentiable_in (z0,1) by Th9;

      hence thesis by PDIFF_2: 19;

    end;

    theorem :: PDIFF_3:34

    f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies (( pdiff1 (f1,1)) (#) ( pdiff1 (f2,1))) is_partial_differentiable_in (z0,2)

    proof

      assume f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0;

      then ( pdiff1 (f1,1)) is_partial_differentiable_in (z0,2) & ( pdiff1 (f2,1)) is_partial_differentiable_in (z0,2) by Th10;

      hence thesis by PDIFF_2: 20;

    end;

    theorem :: PDIFF_3:35

    f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies (( pdiff1 (f1,2)) (#) ( pdiff1 (f2,2))) is_partial_differentiable_in (z0,1)

    proof

      assume f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0;

      then ( pdiff1 (f1,2)) is_partial_differentiable_in (z0,1) & ( pdiff1 (f2,2)) is_partial_differentiable_in (z0,1) by Th11;

      hence thesis by PDIFF_2: 19;

    end;

    theorem :: PDIFF_3:36

    f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies (( pdiff1 (f1,2)) (#) ( pdiff1 (f2,2))) is_partial_differentiable_in (z0,2)

    proof

      assume f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0;

      then ( pdiff1 (f1,2)) is_partial_differentiable_in (z0,2) & ( pdiff1 (f2,2)) is_partial_differentiable_in (z0,2) by Th12;

      hence thesis by PDIFF_2: 20;

    end;

    theorem :: PDIFF_3:37

    for z0 be Element of ( REAL 2) holds f is_hpartial_differentiable`11_in z0 implies ( SVF1 (1,( pdiff1 (f,1)),z0)) is_continuous_in (( proj (1,2)) . z0) by Th9, PDIFF_2: 21;

    theorem :: PDIFF_3:38

    for z0 be Element of ( REAL 2) holds f is_hpartial_differentiable`12_in z0 implies ( SVF1 (2,( pdiff1 (f,1)),z0)) is_continuous_in (( proj (2,2)) . z0) by Th10, PDIFF_2: 22;

    theorem :: PDIFF_3:39

    for z0 be Element of ( REAL 2) holds f is_hpartial_differentiable`21_in z0 implies ( SVF1 (1,( pdiff1 (f,2)),z0)) is_continuous_in (( proj (1,2)) . z0) by Th11, PDIFF_2: 21;

    theorem :: PDIFF_3:40

    for z0 be Element of ( REAL 2) holds f is_hpartial_differentiable`22_in z0 implies ( SVF1 (2,( pdiff1 (f,2)),z0)) is_continuous_in (( proj (2,2)) . z0) by Th12, PDIFF_2: 22;