pdiff_4.miz



    begin

    reserve D for set;

    reserve x,x0,x1,x2,y,y0,y1,y2,z,z0,z1,z2,r,s,t for Real;

    reserve p,a,u,u0 for Element of ( REAL 3);

    reserve n,m,k for Element of NAT ;

    reserve f,f1,f2,f3,g for PartFunc of ( REAL 3), REAL ;

    reserve R,R1,R2 for RestFunc;

    reserve L,L1,L2 for LinearFunc;

    theorem :: PDIFF_4:1

    

     Th1: ( dom ( proj (1,3))) = ( REAL 3) & ( rng ( proj (1,3))) = REAL & for x,y,z be Real holds (( proj (1,3)) . <*x, y, z*>) = x

    proof

      set f = ( proj (1,3));

      

       A1: for x be object st x in REAL holds ex u be object st u in ( REAL 3) & x = (f . u)

      proof

        let x be object;

        assume x in REAL ;

        then

        reconsider x1 = x as Element of REAL ;

        set y = the Element of REAL ;

        reconsider u = <*x1, y, y*> as Element of ( REAL 3) by FINSEQ_2: 104;

        (f . u) = (u . 1) by PDIFF_1:def 1;

        then (f . u) = x by FINSEQ_1: 45;

        hence thesis;

      end;

      now

        let x, y, z;

        reconsider xx = x, yy = y, zz = z as Element of REAL by XREAL_0:def 1;

         <*xx, yy, zz*> is Element of (3 -tuples_on REAL ) by FINSEQ_2: 104;

        then (( proj (1,3)) . <*x, y, z*>) = ( <*x, y, z*> . 1) by PDIFF_1:def 1;

        hence (( proj (1,3)) . <*x, y, z*>) = x by FINSEQ_1: 45;

      end;

      hence thesis by A1, FUNCT_2: 10, FUNCT_2:def 1;

    end;

    theorem :: PDIFF_4:2

    

     Th2: ( dom ( proj (2,3))) = ( REAL 3) & ( rng ( proj (2,3))) = REAL & for x,y,z be Real holds (( proj (2,3)) . <*x, y, z*>) = y

    proof

      set f = ( proj (2,3));

      

       A1: for y be object st y in REAL holds ex u be object st u in ( REAL 3) & y = (f . u)

      proof

        let y be object;

        assume y in REAL ;

        then

        reconsider y1 = y as Element of REAL ;

        set x = the Element of REAL ;

        reconsider u = <*x, y1, x*> as Element of ( REAL 3) by FINSEQ_2: 104;

        (f . u) = (u . 2) by PDIFF_1:def 1;

        then (f . u) = y by FINSEQ_1: 45;

        hence thesis;

      end;

      now

        let x, y, z;

        reconsider xx = x, yy = y, zz = z as Element of REAL by XREAL_0:def 1;

         <*xx, yy, zz*> is Element of (3 -tuples_on REAL ) by FINSEQ_2: 104;

        then (( proj (2,3)) . <*x, y, z*>) = ( <*x, y, z*> . 2) by PDIFF_1:def 1;

        hence (( proj (2,3)) . <*x, y, z*>) = y by FINSEQ_1: 45;

      end;

      hence thesis by A1, FUNCT_2: 10, FUNCT_2:def 1;

    end;

    theorem :: PDIFF_4:3

    

     Th3: ( dom ( proj (3,3))) = ( REAL 3) & ( rng ( proj (3,3))) = REAL & for x,y,z be Real holds (( proj (3,3)) . <*x, y, z*>) = z

    proof

      set f = ( proj (3,3));

      

       A1: for z be object st z in REAL holds ex u be object st u in ( REAL 3) & z = (f . u)

      proof

        let z be object;

        assume z in REAL ;

        then

        reconsider z1 = z as Element of REAL ;

        set x = the Element of REAL ;

        reconsider u = <*x, x, z1*> as Element of ( REAL 3) by FINSEQ_2: 104;

        (f . u) = (u . 3) by PDIFF_1:def 1;

        then (f . u) = z by FINSEQ_1: 45;

        hence thesis;

      end;

      now

        let x,y,z be Real;

        reconsider xx = x, yy = y, zz = z as Element of REAL by XREAL_0:def 1;

         <*xx, yy, zz*> is Element of (3 -tuples_on REAL ) by FINSEQ_2: 104;

        then (( proj (3,3)) . <*x, y, z*>) = ( <*x, y, z*> . 3) by PDIFF_1:def 1;

        hence (( proj (3,3)) . <*x, y, z*>) = z by FINSEQ_1: 45;

      end;

      hence thesis by A1, FUNCT_2: 10, FUNCT_2:def 1;

    end;

    begin

    theorem :: PDIFF_4:4

    

     Th4: u = <*x, y, z*> & f is_partial_differentiable_in (u,1) implies ( SVF1 (1,f,u)) is_differentiable_in x by Th1;

    theorem :: PDIFF_4:5

    

     Th5: u = <*x, y, z*> & f is_partial_differentiable_in (u,2) implies ( SVF1 (2,f,u)) is_differentiable_in y by Th2;

    theorem :: PDIFF_4:6

    

     Th6: u = <*x, y, z*> & f is_partial_differentiable_in (u,3) implies ( SVF1 (3,f,u)) is_differentiable_in z by Th3;

    theorem :: PDIFF_4:7

    

     Th7: for f be PartFunc of ( REAL 3), REAL holds for u be Element of ( REAL 3) holds (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (1,f,u)) is_differentiable_in x0) iff f is_partial_differentiable_in (u,1)

    proof

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

      let u be Element of ( REAL 3);

      thus (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (1,f,u)) is_differentiable_in x0) implies f is_partial_differentiable_in (u,1) by Th1;

      assume

       A1: f is_partial_differentiable_in (u,1);

      consider x0,y0,z0 be Element of REAL such that

       A2: u = <*x0, y0, z0*> by FINSEQ_2: 103;

      (( proj (1,3)) . u) = x0 by A2, Th1;

      then ( SVF1 (1,f,u)) is_differentiable_in x0 by A1;

      hence (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (1,f,u)) is_differentiable_in x0) by A2;

    end;

    theorem :: PDIFF_4:8

    

     Th8: for f be PartFunc of ( REAL 3), REAL holds for u be Element of ( REAL 3) holds (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (2,f,u)) is_differentiable_in y0) iff f is_partial_differentiable_in (u,2)

    proof

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

      let u be Element of ( REAL 3);

      thus (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (2,f,u)) is_differentiable_in y0) implies f is_partial_differentiable_in (u,2) by Th2;

      assume

       A1: f is_partial_differentiable_in (u,2);

      consider x0,y0,z0 be Element of REAL such that

       A2: u = <*x0, y0, z0*> by FINSEQ_2: 103;

      (( proj (2,3)) . u) = y0 by A2, Th2;

      then ( SVF1 (2,f,u)) is_differentiable_in y0 by A1;

      hence (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (2,f,u)) is_differentiable_in y0) by A2;

    end;

    theorem :: PDIFF_4:9

    

     Th9: for f be PartFunc of ( REAL 3), REAL holds for u be Element of ( REAL 3) holds (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (3,f,u)) is_differentiable_in z0) iff f is_partial_differentiable_in (u,3)

    proof

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

      let u be Element of ( REAL 3);

      thus (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (3,f,u)) is_differentiable_in z0) implies f is_partial_differentiable_in (u,3) by Th3;

      assume

       A1: f is_partial_differentiable_in (u,3);

      consider x0,y0,z0 be Element of REAL such that

       A2: u = <*x0, y0, z0*> by FINSEQ_2: 103;

      (( proj (3,3)) . u) = z0 by A2, Th3;

      then ( SVF1 (3,f,u)) is_differentiable_in z0 by A1;

      hence (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ( SVF1 (3,f,u)) is_differentiable_in z0) by A2;

    end;

    theorem :: PDIFF_4:10

    u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,1) implies ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0)))

    proof

      assume that

       A1: u = <*x0, y0, z0*> and

       A2: f is_partial_differentiable_in (u,1);

      consider x1, y1, z1 such that

       A3: u = <*x1, y1, z1*> & ( SVF1 (1,f,u)) is_differentiable_in x1 by A2, Th7;

      ( SVF1 (1,f,u)) is_differentiable_in x0 by A1, A3, FINSEQ_1: 78;

      hence thesis by FDIFF_1:def 4;

    end;

    theorem :: PDIFF_4:11

    u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,2) implies ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0)))

    proof

      assume that

       A1: u = <*x0, y0, z0*> and

       A2: f is_partial_differentiable_in (u,2);

      consider x1, y1, z1 such that

       A3: u = <*x1, y1, z1*> & ( SVF1 (2,f,u)) is_differentiable_in y1 by A2, Th8;

      ( SVF1 (2,f,u)) is_differentiable_in y0 by A1, A3, FINSEQ_1: 78;

      hence thesis by FDIFF_1:def 4;

    end;

    theorem :: PDIFF_4:12

    u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,3) implies ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0)))

    proof

      assume that

       A1: u = <*x0, y0, z0*> and

       A2: f is_partial_differentiable_in (u,3);

      consider x1, y1, z1 such that

       A3: u = <*x1, y1, z1*> & ( SVF1 (3,f,u)) is_differentiable_in z1 by A2, Th9;

      ( SVF1 (3,f,u)) is_differentiable_in z0 by A1, A3, FINSEQ_1: 78;

      hence thesis by FDIFF_1:def 4;

    end;

    theorem :: PDIFF_4:13

    

     Th13: for f be PartFunc of ( REAL 3), REAL holds for u be Element of ( REAL 3) holds f is_partial_differentiable_in (u,1) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0)))

    proof

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

      let u be Element of ( REAL 3);

      hereby

        assume

         A1: f is_partial_differentiable_in (u,1);

        thus (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))))

        proof

          consider x0, y0, z0 such that

           A2: u = <*x0, y0, z0*> & ( SVF1 (1,f,u)) is_differentiable_in x0 by A1, Th7;

          ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A2, FDIFF_1:def 4;

          hence thesis by A2;

        end;

      end;

      assume (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))));

      then

      consider x0, y0, z0 such that

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

      consider N be Neighbourhood of x0 such that

       A4: N c= ( dom ( SVF1 (1,f,u))) & ex L, R st for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3;

      ( SVF1 (1,f,u)) is_differentiable_in x0 by A4, FDIFF_1:def 4;

      hence thesis by A3, Th7;

    end;

    theorem :: PDIFF_4:14

    

     Th14: for f be PartFunc of ( REAL 3), REAL holds for u be Element of ( REAL 3) holds f is_partial_differentiable_in (u,2) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0)))

    proof

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

      let u be Element of ( REAL 3);

      hereby

        assume

         A1: f is_partial_differentiable_in (u,2);

        thus (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))))

        proof

          consider x0, y0, z0 such that

           A2: u = <*x0, y0, z0*> & ( SVF1 (2,f,u)) is_differentiable_in y0 by A1, Th8;

          ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A2, FDIFF_1:def 4;

          hence thesis by A2;

        end;

      end;

      assume (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))));

      then

      consider x0, y0, z0 such that

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

      consider N be Neighbourhood of y0 such that

       A4: N c= ( dom ( SVF1 (2,f,u))) & ex L, R st for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A3;

      ( SVF1 (2,f,u)) is_differentiable_in y0 by A4, FDIFF_1:def 4;

      hence thesis by A3, Th8;

    end;

    theorem :: PDIFF_4:15

    

     Th15: for f be PartFunc of ( REAL 3), REAL holds for u be Element of ( REAL 3) holds f is_partial_differentiable_in (u,3) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0)))

    proof

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

      let u be Element of ( REAL 3);

      hereby

        assume

         A1: f is_partial_differentiable_in (u,3);

        thus (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))))

        proof

          consider x0, y0, z0 such that

           A2: u = <*x0, y0, z0*> & ( SVF1 (3,f,u)) is_differentiable_in z0 by A1, Th9;

          ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A2, FDIFF_1:def 4;

          hence thesis by A2;

        end;

      end;

      assume (ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))));

      then

      consider x0, y0, z0 such that

       A3: u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0)));

      consider N be Neighbourhood of z0 such that

       A4: N c= ( dom ( SVF1 (3,f,u))) & ex L, R st for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A3;

      ( SVF1 (3,f,u)) is_differentiable_in z0 by A4, FDIFF_1:def 4;

      hence thesis by A3, Th9;

    end;

    

     Lm1: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,1) implies (r = ( diff (( SVF1 (1,f,u)),x0)) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))))

    proof

      set F1 = ( SVF1 (1,f,u));

      assume that

       A1: u = <*x0, y0, z0*> and

       A2: f is_partial_differentiable_in (u,1);

      hereby

        assume

         A3: r = ( diff (F1,x0));

        F1 is_differentiable_in x0 by A1, A2, Th4;

        then

        consider N be Neighbourhood of x0 such that

         A4: N c= ( dom F1) & ex L, R st r = (L . 1) & for x st x in N holds ((F1 . x) - (F1 . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3, FDIFF_1:def 5;

        thus ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A1, A4;

      end;

      given x1,y1,z1 be Real such that

       A5: u = <*x1, y1, z1*> & ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x1)) = ((L . (x - x1)) + (R . (x - x1)));

      

       A6: x1 = x0 by A5, A1, FINSEQ_1: 78;

      F1 is_differentiable_in x0 by A1, A2, Th4;

      hence thesis by A6, A5, FDIFF_1:def 5;

    end;

    

     Lm2: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,2) implies (r = ( diff (( SVF1 (2,f,u)),y0)) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))))

    proof

      set F1 = ( SVF1 (2,f,u));

      assume that

       A1: u = <*x0, y0, z0*> and

       A2: f is_partial_differentiable_in (u,2);

      hereby

        assume

         A3: r = ( diff (F1,y0));

        F1 is_differentiable_in y0 by A1, A2, Th5;

        then

        consider N be Neighbourhood of y0 such that

         A4: N c= ( dom F1) & ex L, R st r = (L . 1) & for y st y in N holds ((F1 . y) - (F1 . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A3, FDIFF_1:def 5;

        thus ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom F1) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1, A4;

      end;

      given x1,y1,z1 be Real such that

       A5: u = <*x1, y1, z1*> & ex N be Neighbourhood of y1 st N c= ( dom F1) & ex L, R st r = (L . 1) & for y st y in N holds ((F1 . y) - (F1 . y1)) = ((L . (y - y1)) + (R . (y - y1)));

      

       A6: y1 = y0 by A5, A1, FINSEQ_1: 78;

      F1 is_differentiable_in y0 by A1, A2, Th5;

      hence thesis by A6, A5, FDIFF_1:def 5;

    end;

    

     Lm3: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,3) implies (r = ( diff (( SVF1 (3,f,u)),z0)) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st r = (L . 1) & for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))))

    proof

      set F1 = ( SVF1 (3,f,u));

      assume that

       A1: u = <*x0, y0, z0*> and

       A2: f is_partial_differentiable_in (u,3);

      hereby

        assume

         A3: r = ( diff (F1,z0));

        F1 is_differentiable_in z0 by A1, A2, Th6;

        then

        consider N be Neighbourhood of z0 such that

         A4: N c= ( dom F1) & ex L, R st r = (L . 1) & for z st z in N holds ((F1 . z) - (F1 . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A3, FDIFF_1:def 5;

        thus ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom F1) & ex L, R st r = (L . 1) & for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A1, A4;

      end;

      given x1,y1,z1 be Real such that

       A5: u = <*x1, y1, z1*> & ex N be Neighbourhood of z1 st N c= ( dom F1) & ex L, R st r = (L . 1) & for z st z in N holds ((F1 . z) - (F1 . z1)) = ((L . (z - z1)) + (R . (z - z1)));

      

       A6: z1 = z0 by A5, A1, FINSEQ_1: 78;

      F1 is_differentiable_in z0 by A1, A2, Th6;

      hence thesis by A6, A5, FDIFF_1:def 5;

    end;

    theorem :: PDIFF_4:16

    

     Th16: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,1) implies (r = ( partdiff (f,u,1)) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))))

    proof

      assume

       A1: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,1);

      hereby

        assume r = ( partdiff (f,u,1));

        then r = ( diff (( SVF1 (1,f,u)),x0)) by Th1, A1;

        hence ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by Lm1, A1;

      end;

      given x1,y1,z1 be Real such that

       A2: u = <*x1, y1, z1*> & ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,f,u))) & ex L, R st r = (L . 1) & for x st x in N holds ((( SVF1 (1,f,u)) . x) - (( SVF1 (1,f,u)) . x1)) = ((L . (x - x1)) + (R . (x - x1)));

      r = ( diff (( SVF1 (1,f,u)),x0)) by A2, A1, Lm1;

      hence thesis by Th1, A1;

    end;

    theorem :: PDIFF_4:17

    

     Th17: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,2) implies (r = ( partdiff (f,u,2)) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))))

    proof

      assume

       A1: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,2);

      hereby

        assume r = ( partdiff (f,u,2));

        then r = ( diff (( SVF1 (2,f,u)),y0)) by Th2, A1;

        hence ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by Lm2, A1;

      end;

      given x1,y1,z1 be Real such that

       A2: u = <*x1, y1, z1*> & ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,f,u))) & ex L, R st r = (L . 1) & for y st y in N holds ((( SVF1 (2,f,u)) . y) - (( SVF1 (2,f,u)) . y1)) = ((L . (y - y1)) + (R . (y - y1)));

      r = ( diff (( SVF1 (2,f,u)),y0)) by A2, A1, Lm2;

      hence thesis by Th2, A1;

    end;

    theorem :: PDIFF_4:18

    

     Th18: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,3) implies (r = ( partdiff (f,u,3)) iff ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st r = (L . 1) & for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))))

    proof

      assume

       A1: u = <*x0, y0, z0*> & f is_partial_differentiable_in (u,3);

      hereby

        assume r = ( partdiff (f,u,3));

        then r = ( diff (( SVF1 (3,f,u)),z0)) by Th3, A1;

        hence ex x0,y0,z0 be Real st u = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st r = (L . 1) & for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by Lm3, A1;

      end;

      given x1,y1,z1 be Real such that

       A2: u = <*x1, y1, z1*> & ex N be Neighbourhood of z1 st N c= ( dom ( SVF1 (3,f,u))) & ex L, R st r = (L . 1) & for z st z in N holds ((( SVF1 (3,f,u)) . z) - (( SVF1 (3,f,u)) . z1)) = ((L . (z - z1)) + (R . (z - z1)));

      r = ( diff (( SVF1 (3,f,u)),z0)) by A2, A1, Lm3;

      hence thesis by Th3, A1;

    end;

    theorem :: PDIFF_4:19

    u = <*x0, y0, z0*> implies ( partdiff (f,u,1)) = ( diff (( SVF1 (1,f,u)),x0)) by Th1;

    theorem :: PDIFF_4:20

    u = <*x0, y0, z0*> implies ( partdiff (f,u,2)) = ( diff (( SVF1 (2,f,u)),y0)) by Th2;

    theorem :: PDIFF_4:21

    u = <*x0, y0, z0*> implies ( partdiff (f,u,3)) = ( diff (( SVF1 (3,f,u)),z0)) by Th3;

    definition

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

      let D be set;

      :: PDIFF_4:def1

      pred f is_partial_differentiable`1_on D means D c= ( dom f) & for u be Element of ( REAL 3) st u in D holds (f | D) is_partial_differentiable_in (u,1);

      :: PDIFF_4:def2

      pred f is_partial_differentiable`2_on D means D c= ( dom f) & for u be Element of ( REAL 3) st u in D holds (f | D) is_partial_differentiable_in (u,2);

      :: PDIFF_4:def3

      pred f is_partial_differentiable`3_on D means D c= ( dom f) & for u be Element of ( REAL 3) st u in D holds (f | D) is_partial_differentiable_in (u,3);

    end

    theorem :: PDIFF_4:22

    f is_partial_differentiable`1_on D implies D c= ( dom f) & for u st u in D holds f is_partial_differentiable_in (u,1)

    proof

      assume

       A1: f is_partial_differentiable`1_on D;

      hence D c= ( dom f);

      set g = (f | D);

      let u0 be Element of ( REAL 3);

      assume u0 in D;

      then g is_partial_differentiable_in (u0,1) by A1;

      then

      consider x0,y0,z0 be Real such that

       A2: u0 = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,g,u0))) & ex L, R st for x st x in N holds ((( SVF1 (1,g,u0)) . x) - (( SVF1 (1,g,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by Th13;

      consider N be Neighbourhood of x0 such that

       A3: N c= ( dom ( SVF1 (1,g,u0))) & ex L, R st for x st x in N holds ((( SVF1 (1,g,u0)) . x) - (( SVF1 (1,g,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A2;

      for x st x in ( dom ( SVF1 (1,g,u0))) holds x in ( dom ( SVF1 (1,f,u0)))

      proof

        let x;

        assume x in ( dom ( SVF1 (1,g,u0)));

        then

         A4: x in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . x) in ( dom (f | D)) by FUNCT_1: 11;

        ( dom (f | D)) = (( dom f) /\ D) by RELAT_1: 61;

        then ( dom (f | D)) c= ( dom f) by XBOOLE_1: 17;

        hence thesis by A4, FUNCT_1: 11;

      end;

      then for x be object st x in ( dom ( SVF1 (1,g,u0))) holds x in ( dom ( SVF1 (1,f,u0)));

      then ( dom ( SVF1 (1,g,u0))) c= ( dom ( SVF1 (1,f,u0)));

      then

       A5: N c= ( dom ( SVF1 (1,f,u0))) by A3;

      consider L, R such that

       A6: for x st x in N holds ((( SVF1 (1,g,u0)) . x) - (( SVF1 (1,g,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3;

      for x st x in N holds ((( SVF1 (1,f,u0)) . x) - (( SVF1 (1,f,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0)))

      proof

        let x;

        assume

         A7: x in N;

        

         A8: for x st x in ( dom ( SVF1 (1,g,u0))) holds (( SVF1 (1,g,u0)) . x) = (( SVF1 (1,f,u0)) . x)

        proof

          let x;

          assume

           A9: x in ( dom ( SVF1 (1,g,u0)));

          then

           A10: x in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . x) in ( dom (f | D)) by FUNCT_1: 11;

          (( SVF1 (1,g,u0)) . x) = ((f | D) . (( reproj (1,u0)) . x)) by A9, FUNCT_1: 12

          .= (f . (( reproj (1,u0)) . x)) by A10, FUNCT_1: 47

          .= (( SVF1 (1,f,u0)) . x) by A10, FUNCT_1: 13;

          hence thesis;

        end;

        

         A11: x0 in N by RCOMP_1: 16;

        ((L . (x - x0)) + (R . (x - x0))) = ((( SVF1 (1,g,u0)) . x) - (( SVF1 (1,g,u0)) . x0)) by A6, A7

        .= ((( SVF1 (1,f,u0)) . x) - (( SVF1 (1,g,u0)) . x0)) by A3, A7, A8

        .= ((( SVF1 (1,f,u0)) . x) - (( SVF1 (1,f,u0)) . x0)) by A3, A8, A11;

        hence thesis;

      end;

      hence thesis by A2, A5, Th13;

    end;

    theorem :: PDIFF_4:23

    f is_partial_differentiable`2_on D implies D c= ( dom f) & for u st u in D holds f is_partial_differentiable_in (u,2)

    proof

      assume

       A1: f is_partial_differentiable`2_on D;

      hence D c= ( dom f);

      set g = (f | D);

      let u0 be Element of ( REAL 3);

      assume u0 in D;

      then g is_partial_differentiable_in (u0,2) by A1;

      then

      consider x0,y0,z0 be Real such that

       A2: u0 = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,g,u0))) & ex L, R st for y st y in N holds ((( SVF1 (2,g,u0)) . y) - (( SVF1 (2,g,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by Th14;

      consider N be Neighbourhood of y0 such that

       A3: N c= ( dom ( SVF1 (2,g,u0))) & ex L, R st for y st y in N holds ((( SVF1 (2,g,u0)) . y) - (( SVF1 (2,g,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A2;

      for y st y in ( dom ( SVF1 (2,g,u0))) holds y in ( dom ( SVF1 (2,f,u0)))

      proof

        let y;

        assume y in ( dom ( SVF1 (2,g,u0)));

        then

         A4: y in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y) in ( dom (f | D)) by FUNCT_1: 11;

        ( dom (f | D)) = (( dom f) /\ D) by RELAT_1: 61;

        then ( dom (f | D)) c= ( dom f) by XBOOLE_1: 17;

        hence thesis by A4, FUNCT_1: 11;

      end;

      then for y be object st y in ( dom ( SVF1 (2,g,u0))) holds y in ( dom ( SVF1 (2,f,u0)));

      then ( dom ( SVF1 (2,g,u0))) c= ( dom ( SVF1 (2,f,u0)));

      then

       A5: N c= ( dom ( SVF1 (2,f,u0))) by A3;

      consider L, R such that

       A6: for y st y in N holds ((( SVF1 (2,g,u0)) . y) - (( SVF1 (2,g,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A3;

      for y st y in N holds ((( SVF1 (2,f,u0)) . y) - (( SVF1 (2,f,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0)))

      proof

        let y;

        assume

         A7: y in N;

        

         A8: for y st y in ( dom ( SVF1 (2,g,u0))) holds (( SVF1 (2,g,u0)) . y) = (( SVF1 (2,f,u0)) . y)

        proof

          let y;

          assume

           A9: y in ( dom ( SVF1 (2,g,u0)));

          then

           A10: y in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y) in ( dom (f | D)) by FUNCT_1: 11;

          (( SVF1 (2,g,u0)) . y) = ((f | D) . (( reproj (2,u0)) . y)) by A9, FUNCT_1: 12

          .= (f . (( reproj (2,u0)) . y)) by A10, FUNCT_1: 47

          .= (( SVF1 (2,f,u0)) . y) by A10, FUNCT_1: 13;

          hence thesis;

        end;

        

         A11: y0 in N by RCOMP_1: 16;

        ((L . (y - y0)) + (R . (y - y0))) = ((( SVF1 (2,g,u0)) . y) - (( SVF1 (2,g,u0)) . y0)) by A6, A7

        .= ((( SVF1 (2,f,u0)) . y) - (( SVF1 (2,g,u0)) . y0)) by A3, A7, A8

        .= ((( SVF1 (2,f,u0)) . y) - (( SVF1 (2,f,u0)) . y0)) by A3, A8, A11;

        hence thesis;

      end;

      hence thesis by A2, A5, Th14;

    end;

    theorem :: PDIFF_4:24

    f is_partial_differentiable`3_on D implies D c= ( dom f) & for u st u in D holds f is_partial_differentiable_in (u,3)

    proof

      assume

       A1: f is_partial_differentiable`3_on D;

      hence D c= ( dom f);

      set g = (f | D);

      let u0 be Element of ( REAL 3);

      assume u0 in D;

      then g is_partial_differentiable_in (u0,3) by A1;

      then

      consider x0,y0,z0 be Real such that

       A2: u0 = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,g,u0))) & ex L, R st for z st z in N holds ((( SVF1 (3,g,u0)) . z) - (( SVF1 (3,g,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by Th15;

      consider N be Neighbourhood of z0 such that

       A3: N c= ( dom ( SVF1 (3,g,u0))) & ex L, R st for z st z in N holds ((( SVF1 (3,g,u0)) . z) - (( SVF1 (3,g,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A2;

      for z st z in ( dom ( SVF1 (3,g,u0))) holds z in ( dom ( SVF1 (3,f,u0)))

      proof

        let z;

        assume z in ( dom ( SVF1 (3,g,u0)));

        then

         A4: z in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z) in ( dom (f | D)) by FUNCT_1: 11;

        ( dom (f | D)) = (( dom f) /\ D) by RELAT_1: 61;

        then ( dom (f | D)) c= ( dom f) by XBOOLE_1: 17;

        hence thesis by A4, FUNCT_1: 11;

      end;

      then for z be object st z in ( dom ( SVF1 (3,g,u0))) holds z in ( dom ( SVF1 (3,f,u0)));

      then ( dom ( SVF1 (3,g,u0))) c= ( dom ( SVF1 (3,f,u0)));

      then

       A5: N c= ( dom ( SVF1 (3,f,u0))) by A3;

      consider L, R such that

       A6: for z st z in N holds ((( SVF1 (3,g,u0)) . z) - (( SVF1 (3,g,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A3;

      for z st z in N holds ((( SVF1 (3,f,u0)) . z) - (( SVF1 (3,f,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0)))

      proof

        let z;

        assume

         A7: z in N;

        

         A8: for z st z in ( dom ( SVF1 (3,g,u0))) holds (( SVF1 (3,g,u0)) . z) = (( SVF1 (3,f,u0)) . z)

        proof

          let z;

          assume

           A9: z in ( dom ( SVF1 (3,g,u0)));

          then

           A10: z in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z) in ( dom (f | D)) by FUNCT_1: 11;

          (( SVF1 (3,g,u0)) . z) = ((f | D) . (( reproj (3,u0)) . z)) by A9, FUNCT_1: 12

          .= (f . (( reproj (3,u0)) . z)) by A10, FUNCT_1: 47

          .= (( SVF1 (3,f,u0)) . z) by A10, FUNCT_1: 13;

          hence thesis;

        end;

        

         A11: z0 in N by RCOMP_1: 16;

        ((L . (z - z0)) + (R . (z - z0))) = ((( SVF1 (3,g,u0)) . z) - (( SVF1 (3,g,u0)) . z0)) by A6, A7

        .= ((( SVF1 (3,f,u0)) . z) - (( SVF1 (3,g,u0)) . z0)) by A3, A7, A8

        .= ((( SVF1 (3,f,u0)) . z) - (( SVF1 (3,f,u0)) . z0)) by A3, A8, A11;

        hence thesis;

      end;

      hence thesis by A2, A5, Th15;

    end;

    definition

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

      let D be set;

      assume

       A1: f is_partial_differentiable`1_on D;

      :: PDIFF_4:def4

      func f `partial1| D -> PartFunc of ( REAL 3), REAL means ( dom it ) = D & for u be Element of ( REAL 3) st u in D holds (it . u) = ( partdiff (f,u,1));

      existence

      proof

        defpred P[ Element of ( REAL 3)] means $1 in D;

        deffunc F( Element of ( REAL 3)) = ( In (( partdiff (f,$1,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;

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

        hence ( dom F) = D by A3;

        let u be Element of ( REAL 3);

        assume u in D;

        then u in ( dom F) by A2;

        then (F . u) = F(u) by A2;

        hence thesis;

      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) = ( partdiff (f,u,1)) and

         A6: ( dom G) = D & for u be Element of ( REAL 3) st u in D holds (G . u) = ( partdiff (f,u,1));

        now

          let u be Element of ( REAL 3);

          assume

           A7: u in ( dom F);

          then (F . u) = ( partdiff (f,u,1)) 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_partial_differentiable`2_on D;

      :: PDIFF_4:def5

      func f `partial2| D -> PartFunc of ( REAL 3), REAL means ( dom it ) = D & for u be Element of ( REAL 3) st u in D holds (it . u) = ( partdiff (f,u,2));

      existence

      proof

        defpred P[ Element of ( REAL 3)] means $1 in D;

        deffunc F( Element of ( REAL 3)) = ( In (( partdiff (f,$1,2)), 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;

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

        hence ( dom F) = D by A3;

        let u be Element of ( REAL 3);

        assume u in D;

        then u in ( dom F) by A2;

        then (F . u) = F(u) by A2;

        hence thesis;

      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) = ( partdiff (f,u,2)) and

         A6: ( dom G) = D & for u be Element of ( REAL 3) st u in D holds (G . u) = ( partdiff (f,u,2));

        now

          let u be Element of ( REAL 3);

          assume

           A7: u in ( dom F);

          then (F . u) = ( partdiff (f,u,2)) 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_partial_differentiable`3_on D;

      :: PDIFF_4:def6

      func f `partial3| D -> PartFunc of ( REAL 3), REAL means ( dom it ) = D & for u be Element of ( REAL 3) st u in D holds (it . u) = ( partdiff (f,u,3));

      existence

      proof

        defpred P[ Element of ( REAL 3)] means $1 in D;

        deffunc F( Element of ( REAL 3)) = ( In (( partdiff (f,$1,3)), 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;

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

        hence ( dom F) = D by A3;

        let u be Element of ( REAL 3);

        assume u in D;

        then u in ( dom F) by A2;

        then (F . u) = F(u) by A2;

        hence thesis;

      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) = ( partdiff (f,u,3)) and

         A6: ( dom G) = D & for u be Element of ( REAL 3) st u in D holds (G . u) = ( partdiff (f,u,3));

        now

          let u be Element of ( REAL 3);

          assume

           A7: u in ( dom F);

          then (F . u) = ( partdiff (f,u,3)) by A5;

          hence (F . u) = (G . u) by A5, A6, A7;

        end;

        hence thesis by A5, A6, PARTFUN1: 5;

      end;

    end

    begin

    theorem :: PDIFF_4:25

    for u0 be Element of ( REAL 3) holds for N be Neighbourhood of (( proj (1,3)) . u0) st f is_partial_differentiable_in (u0,1) & N c= ( dom ( SVF1 (1,f,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,f,u0)) /* (h + c)) - (( SVF1 (1,f,u0)) /* c))) is convergent & ( partdiff (f,u0,1)) = ( lim ((h " ) (#) ((( SVF1 (1,f,u0)) /* (h + c)) - (( SVF1 (1,f,u0)) /* c))))

    proof

      let u0 be Element of ( REAL 3);

      let N be Neighbourhood of (( proj (1,3)) . u0);

      assume

       A1: f is_partial_differentiable_in (u0,1) & N c= ( dom ( SVF1 (1,f,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;

      consider x0,y0,z0 be Real such that

       A3: u0 = <*x0, y0, z0*> & ex N1 be Neighbourhood of x0 st N1 c= ( dom ( SVF1 (1,f,u0))) & ex L, R st for x st x in N1 holds ((( SVF1 (1,f,u0)) . x) - (( SVF1 (1,f,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A1, Th13;

      consider N1 be Neighbourhood of x0 such that

       A4: N1 c= ( dom ( SVF1 (1,f,u0))) & ex L, R st for x st x in N1 holds ((( SVF1 (1,f,u0)) . x) - (( SVF1 (1,f,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3;

      consider L, R such that

       A5: for x st x in N1 holds ((( SVF1 (1,f,u0)) . x) - (( SVF1 (1,f,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A4;

      

       A6: (( proj (1,3)) . u0) = x0 by A3, Th1;

      then

      consider N2 be Neighbourhood of x0 such that

       A7: N2 c= N & N2 c= N1 by RCOMP_1: 17;

      consider g be Real such that

       A8: 0 < g & N2 = ].(x0 - g), (x0 + g).[ by RCOMP_1:def 6;

      

       A9: x0 in N2

      proof

        

         A10: (x0 + 0 ) < (x0 + g) by A8, XREAL_1: 8;

        (x0 - g) < (x0 - 0 ) by A8, XREAL_1: 44;

        hence thesis by A8, A10;

      end;

      ex n st ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2

      proof

        x0 in ( rng c) by A2, A6, TARSKI:def 1;

        then

         A11: ( lim c) = x0 by SEQ_4: 25;

        h is convergent & ( lim h) = 0 ;

        

        then

         A12: ( lim (h + c)) = ( 0 + x0) by A11, SEQ_2: 6

        .= x0;

        consider n be Nat such that

         A13: for m be Nat st n <= m holds |.(((h + c) . m) - x0).| < g by A8, A12, SEQ_2:def 7;

        

         A14: ( rng (c ^\ n)) = {x0} by A2, A6, VALUED_0: 26;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        take n;

        thus ( rng (c ^\ n)) c= N2 by A9, A14, TARSKI:def 1;

        let y be object;

        assume y in ( rng ((h + c) ^\ n));

        then

        consider m such that

         A15: y = (((h + c) ^\ n) . m) by FUNCT_2: 113;

        (n + 0 ) <= (n + m) by XREAL_1: 7;

        then |.(((h + c) . (n + m)) - x0).| < g by A13;

        then ( - g) < (((h + c) . (m + n)) - x0) & (((h + c) . (m + n)) - x0) < g by SEQ_2: 1;

        then ( - g) < ((((h + c) ^\ n) . m) - x0) & ((((h + c) ^\ n) . m) - x0) < g by NAT_1:def 3;

        then (x0 + ( - g)) < (((h + c) ^\ n) . m) & (((h + c) ^\ n) . m) < (x0 + g) by XREAL_1: 19, XREAL_1: 20;

        hence thesis by A8, A15;

      end;

      then

      consider n such that

       A16: ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2;

      

       A17: ( rng (c ^\ n)) c= ( dom ( SVF1 (1,f,u0)))

      proof

        let y be object;

        

         A18: ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        assume y in ( rng (c ^\ n));

        then y = x0 by A2, A6, A18, TARSKI:def 1;

        then y in N by A7, A9;

        hence thesis by A1;

      end;

      

       A19: ( rng ((h + c) ^\ n)) c= ( dom ( SVF1 (1,f,u0))) by A16, A7, A1;

      

       A20: ( rng c) c= ( dom ( SVF1 (1,f,u0)))

      proof

        let y be object;

        assume y in ( rng c);

        then y = x0 by A2, A6, TARSKI:def 1;

        then y in N by A7, A9;

        hence thesis by A1;

      end;

      

       A21: ( rng (h + c)) c= ( dom ( SVF1 (1,f,u0))) by A2, A1;

      

       A22: for x st x in N2 holds ((( SVF1 (1,f,u0)) . x) - (( SVF1 (1,f,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A5, A7;

      

       A23: for k holds ((( SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - (( SVF1 (1,f,u0)) . ((c ^\ n) . k))) = ((L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)))

      proof

        let k;

        (((h + c) ^\ n) . k) in ( rng ((h + c) ^\ n)) by VALUED_0: 28;

        then

         A24: (((h + c) ^\ n) . k) in N2 by A16;

        

         A25: ((((h + c) ^\ n) . k) - ((c ^\ n) . k)) = ((((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k)) by SEQM_3: 15

        .= ((((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k)) by SEQ_1: 7

        .= ((h ^\ n) . k);

        

         A26: ((c ^\ n) . k) in ( rng (c ^\ n)) by VALUED_0: 28;

        ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        then ((c ^\ n) . k) = x0 by A2, A6, A26, TARSKI:def 1;

        hence thesis by A5, A7, A24, A25;

      end;

      

       A27: L is total by FDIFF_1:def 3;

      

       A28: R is total by FDIFF_1:def 2;

      

       A29: ((( SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - (( SVF1 (1,f,u0)) /* (c ^\ n))) = ((L /* (h ^\ n)) + (R /* (h ^\ n)))

      proof

        now

          let k;

          

          thus (((( SVF1 (1,f,u0)) /* ((h + c) ^\ n)) - (( SVF1 (1,f,u0)) /* (c ^\ n))) . k) = (((( SVF1 (1,f,u0)) /* ((h + c) ^\ n)) . k) - ((( SVF1 (1,f,u0)) /* (c ^\ n)) . k)) by RFUNCT_2: 1

          .= ((( SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - ((( SVF1 (1,f,u0)) /* (c ^\ n)) . k)) by A19, FUNCT_2: 108

          .= ((( SVF1 (1,f,u0)) . (((h + c) ^\ n) . k)) - (( SVF1 (1,f,u0)) . ((c ^\ n) . k))) by A17, FUNCT_2: 108

          .= ((L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))) by A23

          .= (((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k))) by A27, FUNCT_2: 115

          .= (((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k)) by A28, FUNCT_2: 115

          .= (((L /* (h ^\ n)) + (R /* (h ^\ n))) . k) by SEQ_1: 7;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      

       A30: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent & ( lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ))) = (L . 1)

      proof

        deffunc F( Nat) = ((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . $1));

        consider s1 be Real_Sequence such that

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

        consider s such that

         A32: for p1 be Real holds (L . p1) = (s * p1) by FDIFF_1:def 3;

        

         A33: (L . 1) = (s * 1) by A32

        .= s;

        now

          let m;

          

           A34: ((h ^\ n) . m) <> 0 by SEQ_1: 5;

          

          thus ((((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) . m) = ((((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) " ) . m)) by SEQ_1: 8

          .= ((((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) " ) . m)) by SEQ_1: 7

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)))

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by SEQ_1: 8

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by VALUED_1: 10

          .= (((L . ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A27, FUNCT_2: 115

          .= (((s * ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A32

          .= ((s * (((h ^\ n) . m) * (((h ^\ n) . m) " ))) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m))

          .= ((s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A34, XCMPLX_0:def 7

          .= (s1 . m) by A31, A33;

        end;

        then

         A35: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = s1 by FUNCT_2: 63;

         A36:

        now

          let r be Real such that

           A37: 0 < r;

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

          then

          consider m be Nat such that

           A38: for k be Nat st m <= k holds |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ).| < r by A37, SEQ_2:def 7;

          take n1 = m;

          let k be Nat such that

           A39: n1 <= k;

           |.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . k)) - (L . 1)).| by A31

          .= |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ).|;

          hence |.((s1 . k) - (L . 1)).| < r by A38, A39;

        end;

        hence (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent by A35, SEQ_2:def 6;

        hence thesis by A35, A36, SEQ_2:def 7;

      end;

      

       A40: N2 c= ( dom ( SVF1 (1,f,u0))) by A1, A7;

      

       A41: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = ((((( SVF1 (1,f,u0)) /* (h + c)) ^\ n) - (( SVF1 (1,f,u0)) /* (c ^\ n))) (#) ((h ^\ n) " )) by A21, A29, VALUED_0: 27

      .= ((((( SVF1 (1,f,u0)) /* (h + c)) ^\ n) - ((( SVF1 (1,f,u0)) /* c) ^\ n)) (#) ((h ^\ n) " )) by A20, VALUED_0: 27

      .= ((((( SVF1 (1,f,u0)) /* (h + c)) - (( SVF1 (1,f,u0)) /* c)) ^\ n) (#) ((h ^\ n) " )) by SEQM_3: 17

      .= ((((( SVF1 (1,f,u0)) /* (h + c)) - (( SVF1 (1,f,u0)) /* c)) ^\ n) (#) ((h " ) ^\ n)) by SEQM_3: 18

      .= ((((( SVF1 (1,f,u0)) /* (h + c)) - (( SVF1 (1,f,u0)) /* c)) (#) (h " )) ^\ n) by SEQM_3: 19;

      then

       A42: (L . 1) = ( lim ((h " ) (#) ((( SVF1 (1,f,u0)) /* (h + c)) - (( SVF1 (1,f,u0)) /* c)))) by A30, SEQ_4: 22;

      thus ((h " ) (#) ((( SVF1 (1,f,u0)) /* (h + c)) - (( SVF1 (1,f,u0)) /* c))) is convergent by A30, A41, SEQ_4: 21;

      thus thesis by A1, A3, A22, A40, A42, Th16;

    end;

    theorem :: PDIFF_4:26

    for u0 be Element of ( REAL 3) holds for N be Neighbourhood of (( proj (2,3)) . u0) st f is_partial_differentiable_in (u0,2) & N c= ( dom ( SVF1 (2,f,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,f,u0)) /* (h + c)) - (( SVF1 (2,f,u0)) /* c))) is convergent & ( partdiff (f,u0,2)) = ( lim ((h " ) (#) ((( SVF1 (2,f,u0)) /* (h + c)) - (( SVF1 (2,f,u0)) /* c))))

    proof

      let u0 be Element of ( REAL 3);

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

      assume

       A1: f is_partial_differentiable_in (u0,2) & N c= ( dom ( SVF1 (2,f,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;

      consider x0,y0,z0 be Real such that

       A3: u0 = <*x0, y0, z0*> & ex N1 be Neighbourhood of y0 st N1 c= ( dom ( SVF1 (2,f,u0))) & ex L, R st for y st y in N1 holds ((( SVF1 (2,f,u0)) . y) - (( SVF1 (2,f,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1, Th14;

      consider N1 be Neighbourhood of y0 such that

       A4: N1 c= ( dom ( SVF1 (2,f,u0))) & ex L, R st for y st y in N1 holds ((( SVF1 (2,f,u0)) . y) - (( SVF1 (2,f,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A3;

      consider L, R such that

       A5: for y st y in N1 holds ((( SVF1 (2,f,u0)) . y) - (( SVF1 (2,f,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A4;

      

       A6: (( proj (2,3)) . u0) = y0 by A3, Th2;

      then

      consider N2 be Neighbourhood of y0 such that

       A7: N2 c= N & N2 c= N1 by RCOMP_1: 17;

      consider g be Real such that

       A8: 0 < g & N2 = ].(y0 - g), (y0 + g).[ by RCOMP_1:def 6;

      

       A9: y0 in N2

      proof

        

         A10: (y0 + 0 ) < (y0 + g) by A8, XREAL_1: 8;

        (y0 - g) < (y0 - 0 ) by A8, XREAL_1: 44;

        hence thesis by A8, A10;

      end;

      ex n st ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2

      proof

        y0 in ( rng c) by A2, A6, TARSKI:def 1;

        then

         A11: ( lim c) = y0 by SEQ_4: 25;

        h is convergent & ( lim h) = 0 ;

        

        then

         A12: ( lim (h + c)) = ( 0 + y0) by A11, SEQ_2: 6

        .= y0;

        consider n be Nat such that

         A13: for m be Nat st n <= m holds |.(((h + c) . m) - y0).| < g by A8, A12, SEQ_2:def 7;

        

         A14: ( rng (c ^\ n)) = {y0} by A2, A6, VALUED_0: 26;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        take n;

        thus ( rng (c ^\ n)) c= N2 by A9, A14, TARSKI:def 1;

        let y be object;

        assume y in ( rng ((h + c) ^\ n));

        then

        consider m such that

         A15: y = (((h + c) ^\ n) . m) by FUNCT_2: 113;

        (n + 0 ) <= (n + m) by XREAL_1: 7;

        then |.(((h + c) . (n + m)) - y0).| < g by A13;

        then ( - g) < (((h + c) . (m + n)) - y0) & (((h + c) . (m + n)) - y0) < g by SEQ_2: 1;

        then ( - g) < ((((h + c) ^\ n) . m) - y0) & ((((h + c) ^\ n) . m) - y0) < g by NAT_1:def 3;

        then (y0 + ( - g)) < (((h + c) ^\ n) . m) & (((h + c) ^\ n) . m) < (y0 + g) by XREAL_1: 19, XREAL_1: 20;

        hence thesis by A8, A15;

      end;

      then

      consider n such that

       A16: ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2;

      

       A17: ( rng (c ^\ n)) c= ( dom ( SVF1 (2,f,u0)))

      proof

        let y be object;

        

         A18: ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        assume y in ( rng (c ^\ n));

        then y = y0 by A2, A6, A18, TARSKI:def 1;

        then y in N by A7, A9;

        hence thesis by A1;

      end;

      

       A19: ( rng ((h + c) ^\ n)) c= ( dom ( SVF1 (2,f,u0))) by A16, A7, A1;

      

       A20: ( rng c) c= ( dom ( SVF1 (2,f,u0)))

      proof

        let y be object;

        assume y in ( rng c);

        then y = y0 by A2, A6, TARSKI:def 1;

        then y in N by A7, A9;

        hence thesis by A1;

      end;

      

       A21: ( rng (h + c)) c= ( dom ( SVF1 (2,f,u0))) by A2, A1;

      

       A22: for y st y in N2 holds ((( SVF1 (2,f,u0)) . y) - (( SVF1 (2,f,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A5, A7;

      

       A23: for k holds ((( SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - (( SVF1 (2,f,u0)) . ((c ^\ n) . k))) = ((L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)))

      proof

        let k;

        (((h + c) ^\ n) . k) in ( rng ((h + c) ^\ n)) by VALUED_0: 28;

        then

         A24: (((h + c) ^\ n) . k) in N2 by A16;

        

         A25: ((((h + c) ^\ n) . k) - ((c ^\ n) . k)) = ((((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k)) by SEQM_3: 15

        .= ((((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k)) by SEQ_1: 7

        .= ((h ^\ n) . k);

        

         A26: ((c ^\ n) . k) in ( rng (c ^\ n)) by VALUED_0: 28;

        ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        then ((c ^\ n) . k) = y0 by A2, A6, A26, TARSKI:def 1;

        hence thesis by A5, A7, A24, A25;

      end;

      

       A27: L is total by FDIFF_1:def 3;

      

       A28: R is total by FDIFF_1:def 2;

      

       A29: ((( SVF1 (2,f,u0)) /* ((h + c) ^\ n)) - (( SVF1 (2,f,u0)) /* (c ^\ n))) = ((L /* (h ^\ n)) + (R /* (h ^\ n)))

      proof

        now

          let k;

          

          thus (((( SVF1 (2,f,u0)) /* ((h + c) ^\ n)) - (( SVF1 (2,f,u0)) /* (c ^\ n))) . k) = (((( SVF1 (2,f,u0)) /* ((h + c) ^\ n)) . k) - ((( SVF1 (2,f,u0)) /* (c ^\ n)) . k)) by RFUNCT_2: 1

          .= ((( SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - ((( SVF1 (2,f,u0)) /* (c ^\ n)) . k)) by A19, FUNCT_2: 108

          .= ((( SVF1 (2,f,u0)) . (((h + c) ^\ n) . k)) - (( SVF1 (2,f,u0)) . ((c ^\ n) . k))) by A17, FUNCT_2: 108

          .= ((L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))) by A23

          .= (((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k))) by A27, FUNCT_2: 115

          .= (((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k)) by A28, FUNCT_2: 115

          .= (((L /* (h ^\ n)) + (R /* (h ^\ n))) . k) by SEQ_1: 7;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      

       A30: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent & ( lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ))) = (L . 1)

      proof

        deffunc F( Nat) = ((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . $1));

        consider s1 be Real_Sequence such that

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

        consider s such that

         A32: for p1 be Real holds (L . p1) = (s * p1) by FDIFF_1:def 3;

        

         A33: (L . 1) = (s * 1) by A32

        .= s;

        now

          let m;

          

           A34: ((h ^\ n) . m) <> 0 by SEQ_1: 5;

          

          thus ((((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) . m) = ((((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) " ) . m)) by SEQ_1: 8

          .= ((((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) " ) . m)) by SEQ_1: 7

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)))

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by SEQ_1: 8

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by VALUED_1: 10

          .= (((L . ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A27, FUNCT_2: 115

          .= (((s * ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A32

          .= ((s * (((h ^\ n) . m) * (((h ^\ n) . m) " ))) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m))

          .= ((s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A34, XCMPLX_0:def 7

          .= (s1 . m) by A31, A33;

        end;

        then

         A35: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = s1 by FUNCT_2: 63;

         A36:

        now

          let r be Real such that

           A37: 0 < r;

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

          then

          consider m be Nat such that

           A38: for k be Nat st m <= k holds |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ).| < r by A37, SEQ_2:def 7;

          take n1 = m;

          let k be Nat such that

           A39: n1 <= k;

           |.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . k)) - (L . 1)).| by A31

          .= |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ).|;

          hence |.((s1 . k) - (L . 1)).| < r by A38, A39;

        end;

        hence (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent by A35, SEQ_2:def 6;

        hence thesis by A35, A36, SEQ_2:def 7;

      end;

      

       A40: N2 c= ( dom ( SVF1 (2,f,u0))) by A1, A7;

      

       A41: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = ((((( SVF1 (2,f,u0)) /* (h + c)) ^\ n) - (( SVF1 (2,f,u0)) /* (c ^\ n))) (#) ((h ^\ n) " )) by A21, A29, VALUED_0: 27

      .= ((((( SVF1 (2,f,u0)) /* (h + c)) ^\ n) - ((( SVF1 (2,f,u0)) /* c) ^\ n)) (#) ((h ^\ n) " )) by A20, VALUED_0: 27

      .= ((((( SVF1 (2,f,u0)) /* (h + c)) - (( SVF1 (2,f,u0)) /* c)) ^\ n) (#) ((h ^\ n) " )) by SEQM_3: 17

      .= ((((( SVF1 (2,f,u0)) /* (h + c)) - (( SVF1 (2,f,u0)) /* c)) ^\ n) (#) ((h " ) ^\ n)) by SEQM_3: 18

      .= ((((( SVF1 (2,f,u0)) /* (h + c)) - (( SVF1 (2,f,u0)) /* c)) (#) (h " )) ^\ n) by SEQM_3: 19;

      then

       A42: (L . 1) = ( lim ((h " ) (#) ((( SVF1 (2,f,u0)) /* (h + c)) - (( SVF1 (2,f,u0)) /* c)))) by A30, SEQ_4: 22;

      thus ((h " ) (#) ((( SVF1 (2,f,u0)) /* (h + c)) - (( SVF1 (2,f,u0)) /* c))) is convergent by A30, A41, SEQ_4: 21;

      thus thesis by A1, A3, A22, A40, A42, Th17;

    end;

    theorem :: PDIFF_4:27

    for u0 be Element of ( REAL 3) holds for N be Neighbourhood of (( proj (3,3)) . u0) st f is_partial_differentiable_in (u0,3) & N c= ( dom ( SVF1 (3,f,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,f,u0)) /* (h + c)) - (( SVF1 (3,f,u0)) /* c))) is convergent & ( partdiff (f,u0,3)) = ( lim ((h " ) (#) ((( SVF1 (3,f,u0)) /* (h + c)) - (( SVF1 (3,f,u0)) /* c))))

    proof

      let u0 be Element of ( REAL 3);

      let N be Neighbourhood of (( proj (3,3)) . u0);

      assume

       A1: f is_partial_differentiable_in (u0,3) & N c= ( dom ( SVF1 (3,f,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;

      consider x0,y0,z0 be Real such that

       A3: u0 = <*x0, y0, z0*> & ex N1 be Neighbourhood of z0 st N1 c= ( dom ( SVF1 (3,f,u0))) & ex L, R st for z st z in N1 holds ((( SVF1 (3,f,u0)) . z) - (( SVF1 (3,f,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A1, Th15;

      consider N1 be Neighbourhood of z0 such that

       A4: N1 c= ( dom ( SVF1 (3,f,u0))) & ex L, R st for z st z in N1 holds ((( SVF1 (3,f,u0)) . z) - (( SVF1 (3,f,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A3;

      consider L, R such that

       A5: for z st z in N1 holds ((( SVF1 (3,f,u0)) . z) - (( SVF1 (3,f,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A4;

      

       A6: (( proj (3,3)) . u0) = z0 by A3, Th3;

      then

      consider N2 be Neighbourhood of z0 such that

       A7: N2 c= N & N2 c= N1 by RCOMP_1: 17;

      consider g be Real such that

       A8: 0 < g & N2 = ].(z0 - g), (z0 + g).[ by RCOMP_1:def 6;

      

       A9: z0 in N2

      proof

        

         A10: (z0 + 0 ) < (z0 + g) by A8, XREAL_1: 8;

        (z0 - g) < (z0 - 0 ) by A8, XREAL_1: 44;

        hence thesis by A8, A10;

      end;

      ex n st ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2

      proof

        z0 in ( rng c) by A2, A6, TARSKI:def 1;

        then

         A11: ( lim c) = z0 by SEQ_4: 25;

        h is convergent & ( lim h) = 0 ;

        

        then

         A12: ( lim (h + c)) = ( 0 + z0) by A11, SEQ_2: 6

        .= z0;

        consider n be Nat such that

         A13: for m be Nat st n <= m holds |.(((h + c) . m) - z0).| < g by A8, A12, SEQ_2:def 7;

        

         A14: ( rng (c ^\ n)) = {z0} by A2, A6, VALUED_0: 26;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        take n;

        thus ( rng (c ^\ n)) c= N2 by A9, A14, TARSKI:def 1;

        let z be object;

        assume z in ( rng ((h + c) ^\ n));

        then

        consider m such that

         A15: z = (((h + c) ^\ n) . m) by FUNCT_2: 113;

        (n + 0 ) <= (n + m) by XREAL_1: 7;

        then |.(((h + c) . (n + m)) - z0).| < g by A13;

        then ( - g) < (((h + c) . (m + n)) - z0) & (((h + c) . (m + n)) - z0) < g by SEQ_2: 1;

        then ( - g) < ((((h + c) ^\ n) . m) - z0) & ((((h + c) ^\ n) . m) - z0) < g by NAT_1:def 3;

        then (z0 + ( - g)) < (((h + c) ^\ n) . m) & (((h + c) ^\ n) . m) < (z0 + g) by XREAL_1: 19, XREAL_1: 20;

        hence thesis by A8, A15;

      end;

      then

      consider n such that

       A16: ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2;

      

       A17: ( rng (c ^\ n)) c= ( dom ( SVF1 (3,f,u0)))

      proof

        let z be object;

        

         A18: ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        assume z in ( rng (c ^\ n));

        then z = z0 by A2, A6, A18, TARSKI:def 1;

        then z in N by A7, A9;

        hence thesis by A1;

      end;

      

       A19: ( rng ((h + c) ^\ n)) c= ( dom ( SVF1 (3,f,u0))) by A16, A7, A1;

      

       A20: ( rng c) c= ( dom ( SVF1 (3,f,u0)))

      proof

        let z be object;

        assume z in ( rng c);

        then z = z0 by A2, A6, TARSKI:def 1;

        then z in N by A7, A9;

        hence thesis by A1;

      end;

      

       A21: ( rng (h + c)) c= ( dom ( SVF1 (3,f,u0))) by A2, A1;

      

       A22: for z st z in N2 holds ((( SVF1 (3,f,u0)) . z) - (( SVF1 (3,f,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A5, A7;

      

       A23: for k holds ((( SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - (( SVF1 (3,f,u0)) . ((c ^\ n) . k))) = ((L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k)))

      proof

        let k;

        (((h + c) ^\ n) . k) in ( rng ((h + c) ^\ n)) by VALUED_0: 28;

        then

         A24: (((h + c) ^\ n) . k) in N2 by A16;

        

         A25: ((((h + c) ^\ n) . k) - ((c ^\ n) . k)) = ((((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k)) by SEQM_3: 15

        .= ((((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k)) by SEQ_1: 7

        .= ((h ^\ n) . k);

        

         A26: ((c ^\ n) . k) in ( rng (c ^\ n)) by VALUED_0: 28;

        ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        then ((c ^\ n) . k) = z0 by A2, A6, A26, TARSKI:def 1;

        hence thesis by A5, A7, A24, A25;

      end;

      

       A27: L is total by FDIFF_1:def 3;

      

       A28: R is total by FDIFF_1:def 2;

      

       A29: ((( SVF1 (3,f,u0)) /* ((h + c) ^\ n)) - (( SVF1 (3,f,u0)) /* (c ^\ n))) = ((L /* (h ^\ n)) + (R /* (h ^\ n)))

      proof

        now

          let k;

          

          thus (((( SVF1 (3,f,u0)) /* ((h + c) ^\ n)) - (( SVF1 (3,f,u0)) /* (c ^\ n))) . k) = (((( SVF1 (3,f,u0)) /* ((h + c) ^\ n)) . k) - ((( SVF1 (3,f,u0)) /* (c ^\ n)) . k)) by RFUNCT_2: 1

          .= ((( SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - ((( SVF1 (3,f,u0)) /* (c ^\ n)) . k)) by A19, FUNCT_2: 108

          .= ((( SVF1 (3,f,u0)) . (((h + c) ^\ n) . k)) - (( SVF1 (3,f,u0)) . ((c ^\ n) . k))) by A17, FUNCT_2: 108

          .= ((L . ((h ^\ n) . k)) + (R . ((h ^\ n) . k))) by A23

          .= (((L /* (h ^\ n)) . k) + (R . ((h ^\ n) . k))) by A27, FUNCT_2: 115

          .= (((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k)) by A28, FUNCT_2: 115

          .= (((L /* (h ^\ n)) + (R /* (h ^\ n))) . k) by SEQ_1: 7;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      

       A30: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent & ( lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ))) = (L . 1)

      proof

        deffunc F( Nat) = ((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . $1));

        consider s1 be Real_Sequence such that

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

        consider s such that

         A32: for p1 be Real holds (L . p1) = (s * p1) by FDIFF_1:def 3;

        

         A33: (L . 1) = (s * 1) by A32

        .= s;

        now

          let m;

          

           A34: ((h ^\ n) . m) <> 0 by SEQ_1: 5;

          

          thus ((((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) . m) = ((((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) " ) . m)) by SEQ_1: 8

          .= ((((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) " ) . m)) by SEQ_1: 7

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)))

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by SEQ_1: 8

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by VALUED_1: 10

          .= (((L . ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A27, FUNCT_2: 115

          .= (((s * ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A32

          .= ((s * (((h ^\ n) . m) * (((h ^\ n) . m) " ))) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m))

          .= ((s * 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A34, XCMPLX_0:def 7

          .= (s1 . m) by A31, A33;

        end;

        then

         A35: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = s1 by FUNCT_2: 63;

         A36:

        now

          let r be Real such that

           A37: 0 < r;

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

          then

          consider m be Nat such that

           A38: for k be Nat st m <= k holds |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ).| < r by A37, SEQ_2:def 7;

          take n1 = m;

          let k be Nat such that

           A39: n1 <= k;

           |.((s1 . k) - (L . 1)).| = |.(((L . 1) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . k)) - (L . 1)).| by A31

          .= |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0 ).|;

          hence |.((s1 . k) - (L . 1)).| < r by A38, A39;

        end;

        hence (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent by A35, SEQ_2:def 6;

        hence thesis by A35, A36, SEQ_2:def 7;

      end;

      

       A40: N2 c= ( dom ( SVF1 (3,f,u0))) by A1, A7;

      

       A41: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = ((((( SVF1 (3,f,u0)) /* (h + c)) ^\ n) - (( SVF1 (3,f,u0)) /* (c ^\ n))) (#) ((h ^\ n) " )) by A21, A29, VALUED_0: 27

      .= ((((( SVF1 (3,f,u0)) /* (h + c)) ^\ n) - ((( SVF1 (3,f,u0)) /* c) ^\ n)) (#) ((h ^\ n) " )) by A20, VALUED_0: 27

      .= ((((( SVF1 (3,f,u0)) /* (h + c)) - (( SVF1 (3,f,u0)) /* c)) ^\ n) (#) ((h ^\ n) " )) by SEQM_3: 17

      .= ((((( SVF1 (3,f,u0)) /* (h + c)) - (( SVF1 (3,f,u0)) /* c)) ^\ n) (#) ((h " ) ^\ n)) by SEQM_3: 18

      .= ((((( SVF1 (3,f,u0)) /* (h + c)) - (( SVF1 (3,f,u0)) /* c)) (#) (h " )) ^\ n) by SEQM_3: 19;

      then

       A42: (L . 1) = ( lim ((h " ) (#) ((( SVF1 (3,f,u0)) /* (h + c)) - (( SVF1 (3,f,u0)) /* c)))) by A30, SEQ_4: 22;

      thus ((h " ) (#) ((( SVF1 (3,f,u0)) /* (h + c)) - (( SVF1 (3,f,u0)) /* c))) is convergent by A30, A41, SEQ_4: 21;

      thus thesis by A1, A3, A22, A40, A42, Th18;

    end;

    theorem :: PDIFF_4:28

    f1 is_partial_differentiable_in (u0,1) & f2 is_partial_differentiable_in (u0,1) implies (f1 (#) f2) is_partial_differentiable_in (u0,1)

    proof

      assume that

       A1: f1 is_partial_differentiable_in (u0,1) and

       A2: f2 is_partial_differentiable_in (u0,1);

      consider x0,y0,z0 be Real such that

       A3: u0 = <*x0, y0, z0*> & ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f1,u0))) & ex L, R st for x st x in N holds ((( SVF1 (1,f1,u0)) . x) - (( SVF1 (1,f1,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A1, Th13;

      consider N1 be Neighbourhood of x0 such that

       A4: N1 c= ( dom ( SVF1 (1,f1,u0))) & ex L, R st for x st x in N1 holds ((( SVF1 (1,f1,u0)) . x) - (( SVF1 (1,f1,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3;

      consider L1, R1 such that

       A5: for x st x in N1 holds ((( SVF1 (1,f1,u0)) . x) - (( SVF1 (1,f1,u0)) . x0)) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A4;

      consider x1,y1,z1 be Real such that

       A6: u0 = <*x1, y1, z1*> & ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,f2,u0))) & ex L, R st for x st x in N holds ((( SVF1 (1,f2,u0)) . x) - (( SVF1 (1,f2,u0)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A2, Th13;

      x0 = x1 & y0 = y1 & z0 = z1 by A3, A6, FINSEQ_1: 78;

      then

      consider N2 be Neighbourhood of x0 such that

       A7: N2 c= ( dom ( SVF1 (1,f2,u0))) & ex L, R st for x st x in N2 holds ((( SVF1 (1,f2,u0)) . x) - (( SVF1 (1,f2,u0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A6;

      consider L2, R2 such that

       A8: for x st x in N2 holds ((( SVF1 (1,f2,u0)) . x) - (( SVF1 (1,f2,u0)) . x0)) = ((L2 . (x - x0)) + (R2 . (x - x0))) by A7;

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 & N c= N2 by RCOMP_1: 17;

      reconsider L11 = ((( SVF1 (1,f2,u0)) . x0) (#) L1), L12 = ((( SVF1 (1,f1,u0)) . x0) (#) L2) as LinearFunc by FDIFF_1: 3;

      

       A10: L11 is total & L12 is total & L1 is total & L2 is total by FDIFF_1:def 3;

      reconsider L = (L11 + L12) as LinearFunc by FDIFF_1: 2;

      reconsider R11 = ((( SVF1 (1,f2,u0)) . x0) (#) R1) as RestFunc by FDIFF_1: 5;

      reconsider R12 = ((( SVF1 (1,f1,u0)) . x0) (#) R2) as RestFunc by FDIFF_1: 5;

      reconsider R13 = (R11 + R12) as RestFunc by FDIFF_1: 4;

      reconsider R14 = (L1 (#) L2) as RestFunc by FDIFF_1: 6;

      reconsider R15 = (R13 + R14) as RestFunc by FDIFF_1: 4;

      reconsider R16 = (R1 (#) L2), R18 = (R2 (#) L1) as RestFunc by FDIFF_1: 7;

      reconsider R17 = (R1 (#) R2) as RestFunc by FDIFF_1: 4;

      reconsider R19 = (R16 + R17) as RestFunc by FDIFF_1: 4;

      reconsider R20 = (R19 + R18) as RestFunc by FDIFF_1: 4;

      reconsider R = (R15 + R20) as RestFunc by FDIFF_1: 4;

      

       A11: R1 is total & R2 is total & R11 is total & R12 is total & R13 is total & R14 is total & R15 is total & R16 is total & R17 is total & R18 is total & R19 is total & R20 is total by FDIFF_1:def 2;

      

       A12: N c= ( dom ( SVF1 (1,f1,u0))) by A4, A9;

      

       A13: N c= ( dom ( SVF1 (1,f2,u0))) by A7, A9;

      

       A14: for y st y in N holds y in ( dom ( SVF1 (1,(f1 (#) f2),u0)))

      proof

        let y;

        assume

         A15: y in N;

        then

         A16: y in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . y) in ( dom f1) by A12, FUNCT_1: 11;

        y in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . y) in ( dom f2) by A13, A15, FUNCT_1: 11;

        then y in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . y) in (( dom f1) /\ ( dom f2)) by A16, XBOOLE_0:def 4;

        then y in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . y) in ( dom (f1 (#) f2)) by VALUED_1:def 4;

        hence thesis by FUNCT_1: 11;

      end;

      then for y be object st y in N holds y in ( dom ( SVF1 (1,(f1 (#) f2),u0)));

      then

       A17: N c= ( dom ( SVF1 (1,(f1 (#) f2),u0)));

      now

        let x;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume

         A18: x in N;

        then

         A19: (((( SVF1 (1,f1,u0)) . x) - (( SVF1 (1,f1,u0)) . x0)) + (( SVF1 (1,f1,u0)) . x0)) = (((L1 . (x - x0)) + (R1 . (x - x0))) + (( SVF1 (1,f1,u0)) . x0)) by A5, A9;

        x in ( dom ((f1 (#) f2) * ( reproj (1,u0)))) by A14, A18;

        then

         A20: x in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . x) in ( dom (f1 (#) f2)) by FUNCT_1: 11;

        then (( reproj (1,u0)) . x) in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then (( reproj (1,u0)) . x) in ( dom f1) & (( reproj (1,u0)) . x) in ( dom f2) by XBOOLE_0:def 4;

        then

         A21: x in ( dom (f1 * ( reproj (1,u0)))) & x in ( dom (f2 * ( reproj (1,u0)))) by A20, FUNCT_1: 11;

        

         A22: x0 in N by RCOMP_1: 16;

        x0 in ( dom ((f1 (#) f2) * ( reproj (1,u0)))) by A14, RCOMP_1: 16;

        then

         A23: x0 in ( dom ( reproj (1,u0))) & (( reproj (1,u0)) . x0) in ( dom (f1 (#) f2)) by FUNCT_1: 11;

        then (( reproj (1,u0)) . x0) in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then (( reproj (1,u0)) . x0) in ( dom f1) & (( reproj (1,u0)) . x0) in ( dom f2) by XBOOLE_0:def 4;

        then

         A24: x0 in ( dom (f1 * ( reproj (1,u0)))) & x0 in ( dom (f2 * ( reproj (1,u0)))) by A23, FUNCT_1: 11;

        

        thus ((( SVF1 (1,(f1 (#) f2),u0)) . x) - (( SVF1 (1,(f1 (#) f2),u0)) . x0)) = (((f1 (#) f2) . (( reproj (1,u0)) . x)) - (( SVF1 (1,(f1 (#) f2),u0)) . x0)) by A17, A18, FUNCT_1: 12

        .= (((f1 . (( reproj (1,u0)) . x)) * (f2 . (( reproj (1,u0)) . x))) - (( SVF1 (1,(f1 (#) f2),u0)) . x0)) by VALUED_1: 5

        .= (((( SVF1 (1,f1,u0)) . x) * (f2 . (( reproj (1,u0)) . x))) - (( SVF1 (1,(f1 (#) f2),u0)) . x0)) by A21, FUNCT_1: 12

        .= (((( SVF1 (1,f1,u0)) . x) * (( SVF1 (1,f2,u0)) . x)) - (((f1 (#) f2) * ( reproj (1,u0))) . x0)) by A21, FUNCT_1: 12

        .= (((( SVF1 (1,f1,u0)) . x) * (( SVF1 (1,f2,u0)) . x)) - ((f1 (#) f2) . (( reproj (1,u0)) . x0))) by A17, A22, FUNCT_1: 12

        .= (((( SVF1 (1,f1,u0)) . x) * (( SVF1 (1,f2,u0)) . x)) - ((f1 . (( reproj (1,u0)) . x0)) * (f2 . (( reproj (1,u0)) . x0)))) by VALUED_1: 5

        .= (((( SVF1 (1,f1,u0)) . x) * (( SVF1 (1,f2,u0)) . x)) - ((( SVF1 (1,f1,u0)) . x0) * (f2 . (( reproj (1,u0)) . x0)))) by A24, FUNCT_1: 12

        .= (((((( SVF1 (1,f1,u0)) . x) * (( SVF1 (1,f2,u0)) . x)) + ( - ((( SVF1 (1,f1,u0)) . x) * (( SVF1 (1,f2,u0)) . x0)))) + ((( SVF1 (1,f1,u0)) . x) * (( SVF1 (1,f2,u0)) . x0))) - ((( SVF1 (1,f1,u0)) . x0) * (( SVF1 (1,f2,u0)) . x0))) by A24, FUNCT_1: 12

        .= (((( SVF1 (1,f1,u0)) . x) * ((( SVF1 (1,f2,u0)) . x) - (( SVF1 (1,f2,u0)) . x0))) + (((( SVF1 (1,f1,u0)) . x) - (( SVF1 (1,f1,u0)) . x0)) * (( SVF1 (1,f2,u0)) . x0)))

        .= (((( SVF1 (1,f1,u0)) . x) * ((( SVF1 (1,f2,u0)) . x) - (( SVF1 (1,f2,u0)) . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * (( SVF1 (1,f2,u0)) . x0))) by A5, A9, A18

        .= (((( SVF1 (1,f1,u0)) . x) * ((( SVF1 (1,f2,u0)) . x) - (( SVF1 (1,f2,u0)) . x0))) + (((( SVF1 (1,f2,u0)) . x0) * (L1 . (x - x0))) + ((( SVF1 (1,f2,u0)) . x0) * (R1 . (x - x0)))))

        .= (((( SVF1 (1,f1,u0)) . x) * ((( SVF1 (1,f2,u0)) . x) - (( SVF1 (1,f2,u0)) . x0))) + ((L11 . (xx - x0)) + ((( SVF1 (1,f2,u0)) . x0) * (R1 . (xx - xx0))))) by A10, RFUNCT_1: 57

        .= (((((L1 . (x - x0)) + (R1 . (xx - x0))) + (( SVF1 (1,f1,u0)) . x0)) * ((( SVF1 (1,f2,u0)) . xx) - (( SVF1 (1,f2,u0)) . x0))) + ((L11 . (x - x0)) + (R11 . (xx - x0)))) by A11, A19, RFUNCT_1: 57

        .= (((((L1 . (x - x0)) + (R1 . (x - x0))) + (( SVF1 (1,f1,u0)) . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))) by A8, A9, A18

        .= (((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((( SVF1 (1,f1,u0)) . x0) * (L2 . (x - x0))) + ((( SVF1 (1,f1,u0)) . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0))))

        .= (((((L1 . (xx - x0)) + (R1 . (xx - x0))) * ((L2 . (xx - x0)) + (R2 . (xx - xx0)))) + ((L12 . (x - x0)) + ((( SVF1 (1,f1,u0)) . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0)))) by A10, RFUNCT_1: 57

        .= (((((L1 . (x - x0)) + (R1 . (xx - xx0))) * ((L2 . (xx - x0)) + (R2 . (x - x0)))) + ((L12 . (xx - x0)) + (R12 . (x - x0)))) + ((L11 . (xx - x0)) + (R11 . (x - x0)))) by A11, RFUNCT_1: 57

        .= ((((L1 . (xx - x0)) + (R1 . (x - x0))) * ((L2 . (xx - x0)) + (R2 . (x - x0)))) + ((L12 . (xx - x0)) + ((L11 . (x - x0)) + ((R11 . (xx - x0)) + (R12 . (x - x0))))))

        .= ((((L1 . (xx - x0)) + (R1 . (x - x0))) * ((L2 . (xx - xx0)) + (R2 . (xx - x0)))) + ((L12 . (xx - x0)) + ((L11 . (xx - x0)) + (R13 . (xx - x0))))) by A11, RFUNCT_1: 56

        .= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((L11 . (x - x0)) + (L12 . (x - x0))) + (R13 . (x - x0))))

        .= (((((L1 . (xx - x0)) * (L2 . (xx - x0))) + ((L1 . (xx - x0)) * (R2 . (xx - x0)))) + ((R1 . (xx - xx0)) * ((L2 . (xx - x0)) + (R2 . (xx - x0))))) + ((L . (xx - x0)) + (R13 . (xx - x0)))) by A10, RFUNCT_1: 56

        .= ((((R14 . (xx - x0)) + ((R2 . (xx - x0)) * (L1 . (xx - x0)))) + ((R1 . (xx - x0)) * ((L2 . (xx - x0)) + (R2 . (xx - x0))))) + ((L . (xx - x0)) + (R13 . (xx - xx0)))) by A10, RFUNCT_1: 56

        .= ((((R14 . (xx - x0)) + (R18 . (xx - x0))) + (((R1 . (xx - x0)) * (L2 . (x - x0))) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - xx0)))) by A10, A11, RFUNCT_1: 56

        .= ((((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (xx - xx0)))) by A10, A11, RFUNCT_1: 56

        .= ((((R14 . (xx - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A11, RFUNCT_1: 56

        .= ((((R14 . (xx - xx0)) + (R18 . (x - x0))) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A11, RFUNCT_1: 56

        .= (((R14 . (xx - x0)) + ((R19 . (x - x0)) + (R18 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0))))

        .= (((L . (xx - xx0)) + (R13 . (x - x0))) + ((R14 . (x - x0)) + (R20 . (x - x0)))) by A11, RFUNCT_1: 56

        .= ((L . (xx - x0)) + (((R13 . (x - x0)) + (R14 . (x - x0))) + (R20 . (x - x0))))

        .= ((L . (xx - xx0)) + ((R15 . (x - x0)) + (R20 . (x - x0)))) by A11, RFUNCT_1: 56

        .= ((L . (x - x0)) + (R . (x - x0))) by A11, RFUNCT_1: 56;

      end;

      hence thesis by A3, A17, Th13;

    end;

    theorem :: PDIFF_4:29

    f1 is_partial_differentiable_in (u0,2) & f2 is_partial_differentiable_in (u0,2) implies (f1 (#) f2) is_partial_differentiable_in (u0,2)

    proof

      assume that

       A1: f1 is_partial_differentiable_in (u0,2) and

       A2: f2 is_partial_differentiable_in (u0,2);

      consider x0,y0,z0 be Real such that

       A3: u0 = <*x0, y0, z0*> & ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f1,u0))) & ex L, R st for y st y in N holds ((( SVF1 (2,f1,u0)) . y) - (( SVF1 (2,f1,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1, Th14;

      consider N1 be Neighbourhood of y0 such that

       A4: N1 c= ( dom ( SVF1 (2,f1,u0))) & ex L, R st for y st y in N1 holds ((( SVF1 (2,f1,u0)) . y) - (( SVF1 (2,f1,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A3;

      consider L1, R1 such that

       A5: for y st y in N1 holds ((( SVF1 (2,f1,u0)) . y) - (( SVF1 (2,f1,u0)) . y0)) = ((L1 . (y - y0)) + (R1 . (y - y0))) by A4;

      consider x1,y1,z1 be Real such that

       A6: u0 = <*x1, y1, z1*> & ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,f2,u0))) & ex L, R st for y st y in N holds ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A2, Th14;

      x0 = x1 & y0 = y1 & z0 = z1 by A3, A6, FINSEQ_1: 78;

      then

      consider N2 be Neighbourhood of y0 such that

       A7: N2 c= ( dom ( SVF1 (2,f2,u0))) & ex L, R st for y st y in N2 holds ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A6;

      consider L2, R2 such that

       A8: for y st y in N2 holds ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y0)) = ((L2 . (y - y0)) + (R2 . (y - y0))) by A7;

      consider N be Neighbourhood of y0 such that

       A9: N c= N1 & N c= N2 by RCOMP_1: 17;

      reconsider L11 = ((( SVF1 (2,f2,u0)) . y0) (#) L1) as LinearFunc by FDIFF_1: 3;

      reconsider L12 = ((( SVF1 (2,f1,u0)) . y0) (#) L2) as LinearFunc by FDIFF_1: 3;

      

       A10: L11 is total & L12 is total & L1 is total & L2 is total by FDIFF_1:def 3;

      reconsider L = (L11 + L12) as LinearFunc by FDIFF_1: 2;

      reconsider R11 = ((( SVF1 (2,f2,u0)) . y0) (#) R1), R12 = ((( SVF1 (2,f1,u0)) . y0) (#) R2) as RestFunc by FDIFF_1: 5;

      reconsider R13 = (R11 + R12) as RestFunc by FDIFF_1: 4;

      reconsider R14 = (L1 (#) L2) as RestFunc by FDIFF_1: 6;

      reconsider R15 = (R13 + R14), R17 = (R1 (#) R2) as RestFunc by FDIFF_1: 4;

      reconsider R16 = (R1 (#) L2), R18 = (R2 (#) L1) as RestFunc by FDIFF_1: 7;

      reconsider R19 = (R16 + R17) as RestFunc by FDIFF_1: 4;

      reconsider R20 = (R19 + R18) as RestFunc by FDIFF_1: 4;

      reconsider R = (R15 + R20) as RestFunc by FDIFF_1: 4;

      

       A11: R1 is total & R2 is total & R11 is total & R12 is total & R13 is total & R14 is total & R15 is total & R16 is total & R17 is total & R18 is total & R19 is total & R20 is total by FDIFF_1:def 2;

      

       A12: N c= ( dom ( SVF1 (2,f1,u0))) by A4, A9;

      

       A13: N c= ( dom ( SVF1 (2,f2,u0))) by A7, A9;

      

       A14: for y st y in N holds y in ( dom ( SVF1 (2,(f1 (#) f2),u0)))

      proof

        let y;

        assume

         A15: y in N;

        then

         A16: y in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y) in ( dom f1) by A12, FUNCT_1: 11;

        y in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y) in ( dom f2) by A13, A15, FUNCT_1: 11;

        then y in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y) in (( dom f1) /\ ( dom f2)) by A16, XBOOLE_0:def 4;

        then y in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y) in ( dom (f1 (#) f2)) by VALUED_1:def 4;

        hence thesis by FUNCT_1: 11;

      end;

      then for y be object st y in N holds y in ( dom ( SVF1 (2,(f1 (#) f2),u0)));

      then

       A17: N c= ( dom ( SVF1 (2,(f1 (#) f2),u0)));

      now

        let yy be Real;

        assume

         A18: yy in N;

        reconsider y = yy, yy0 = y0 as Element of REAL by XREAL_0:def 1;

        

         A19: (((( SVF1 (2,f1,u0)) . y) - (( SVF1 (2,f1,u0)) . y0)) + (( SVF1 (2,f1,u0)) . y0)) = (((L1 . (y - y0)) + (R1 . (y - y0))) + (( SVF1 (2,f1,u0)) . y0)) by A5, A9, A18;

        y in ( dom ((f1 (#) f2) * ( reproj (2,u0)))) by A14, A18;

        then

         A20: y in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y) in ( dom (f1 (#) f2)) by FUNCT_1: 11;

        then (( reproj (2,u0)) . y) in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then (( reproj (2,u0)) . y) in ( dom f1) & (( reproj (2,u0)) . y) in ( dom f2) by XBOOLE_0:def 4;

        then

         A21: y in ( dom (f1 * ( reproj (2,u0)))) & y in ( dom (f2 * ( reproj (2,u0)))) by A20, FUNCT_1: 11;

        

         A22: y0 in N by RCOMP_1: 16;

        y0 in ( dom ((f1 (#) f2) * ( reproj (2,u0)))) by A14, RCOMP_1: 16;

        then

         A23: y0 in ( dom ( reproj (2,u0))) & (( reproj (2,u0)) . y0) in ( dom (f1 (#) f2)) by FUNCT_1: 11;

        then (( reproj (2,u0)) . y0) in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then (( reproj (2,u0)) . y0) in ( dom f1) & (( reproj (2,u0)) . y0) in ( dom f2) by XBOOLE_0:def 4;

        then

         A24: y0 in ( dom (f1 * ( reproj (2,u0)))) & y0 in ( dom (f2 * ( reproj (2,u0)))) by A23, FUNCT_1: 11;

        

        thus ((( SVF1 (2,(f1 (#) f2),u0)) . yy) - (( SVF1 (2,(f1 (#) f2),u0)) . y0)) = (((f1 (#) f2) . (( reproj (2,u0)) . y)) - (( SVF1 (2,(f1 (#) f2),u0)) . y0)) by A17, A18, FUNCT_1: 12

        .= (((f1 . (( reproj (2,u0)) . y)) * (f2 . (( reproj (2,u0)) . y))) - (( SVF1 (2,(f1 (#) f2),u0)) . y0)) by VALUED_1: 5

        .= (((( SVF1 (2,f1,u0)) . y) * (f2 . (( reproj (2,u0)) . y))) - (( SVF1 (2,(f1 (#) f2),u0)) . y0)) by A21, FUNCT_1: 12

        .= (((( SVF1 (2,f1,u0)) . y) * (( SVF1 (2,f2,u0)) . y)) - (((f1 (#) f2) * ( reproj (2,u0))) . y0)) by A21, FUNCT_1: 12

        .= (((( SVF1 (2,f1,u0)) . y) * (( SVF1 (2,f2,u0)) . y)) - ((f1 (#) f2) . (( reproj (2,u0)) . y0))) by A17, A22, FUNCT_1: 12

        .= (((( SVF1 (2,f1,u0)) . y) * (( SVF1 (2,f2,u0)) . y)) - ((f1 . (( reproj (2,u0)) . y0)) * (f2 . (( reproj (2,u0)) . y0)))) by VALUED_1: 5

        .= (((( SVF1 (2,f1,u0)) . y) * (( SVF1 (2,f2,u0)) . y)) - ((( SVF1 (2,f1,u0)) . y0) * (f2 . (( reproj (2,u0)) . y0)))) by A24, FUNCT_1: 12

        .= (((((( SVF1 (2,f1,u0)) . y) * (( SVF1 (2,f2,u0)) . y)) + ( - ((( SVF1 (2,f1,u0)) . y) * (( SVF1 (2,f2,u0)) . y0)))) + ((( SVF1 (2,f1,u0)) . y) * (( SVF1 (2,f2,u0)) . y0))) - ((( SVF1 (2,f1,u0)) . y0) * (( SVF1 (2,f2,u0)) . y0))) by A24, FUNCT_1: 12

        .= (((( SVF1 (2,f1,u0)) . y) * ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y0))) + (((( SVF1 (2,f1,u0)) . y) - (( SVF1 (2,f1,u0)) . y0)) * (( SVF1 (2,f2,u0)) . y0)))

        .= (((( SVF1 (2,f1,u0)) . y) * ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y0))) + (((L1 . (y - y0)) + (R1 . (y - y0))) * (( SVF1 (2,f2,u0)) . y0))) by A5, A9, A18

        .= (((( SVF1 (2,f1,u0)) . y) * ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y0))) + (((( SVF1 (2,f2,u0)) . y0) * (L1 . (y - y0))) + ((( SVF1 (2,f2,u0)) . y0) * (R1 . (y - y0)))))

        .= (((( SVF1 (2,f1,u0)) . y) * ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y0))) + ((L11 . (y - yy0)) + ((( SVF1 (2,f2,u0)) . y0) * (R1 . (y - yy0))))) by A10, RFUNCT_1: 57

        .= (((((L1 . (y - yy0)) + (R1 . (y - yy0))) + (( SVF1 (2,f1,u0)) . y0)) * ((( SVF1 (2,f2,u0)) . y) - (( SVF1 (2,f2,u0)) . y0))) + ((L11 . (y - y0)) + (R11 . (y - y0)))) by A11, A19, RFUNCT_1: 57

        .= (((((L1 . (y - y0)) + (R1 . (y - y0))) + (( SVF1 (2,f1,u0)) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0)))) by A8, A9, A18

        .= (((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + (((( SVF1 (2,f1,u0)) . y0) * (L2 . (y - y0))) + ((( SVF1 (2,f1,u0)) . y0) * (R2 . (y - y0))))) + ((L11 . (y - y0)) + (R11 . (y - y0))))

        .= (((((L1 . (y - yy0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((( SVF1 (2,f1,u0)) . y0) * (R2 . (y - y0))))) + ((L11 . (y - y0)) + (R11 . (y - y0)))) by A10, RFUNCT_1: 57

        .= (((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + (R12 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0)))) by A11, RFUNCT_1: 57

        .= ((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((L11 . (y - y0)) + ((R11 . (y - y0)) + (R12 . (y - y0))))))

        .= ((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - yy0)) + ((L11 . (y - y0)) + (R13 . (y - y0))))) by A11, RFUNCT_1: 56

        .= ((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + (((L11 . (y - y0)) + (L12 . (y - y0))) + (R13 . (y - y0))))

        .= (((((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0)))) + ((R1 . (y - yy0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0)))) by A10, RFUNCT_1: 56

        .= ((((R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((L . (y - yy0)) + (R13 . (y - y0)))) by A10, RFUNCT_1: 56

        .= ((((R14 . (y - y0)) + (R18 . (y - y0))) + (((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((L . (y - yy0)) + (R13 . (y - y0)))) by A10, A11, RFUNCT_1: 56

        .= ((((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((L . (y - yy0)) + (R13 . (y - y0)))) by A10, A11, RFUNCT_1: 56

        .= ((((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + (R17 . (y - y0)))) + ((L . (y - y0)) + (R13 . (y - y0)))) by A11, RFUNCT_1: 56

        .= ((((R14 . (y - yy0)) + (R18 . (y - y0))) + (R19 . (y - y0))) + ((L . (y - y0)) + (R13 . (y - y0)))) by A11, RFUNCT_1: 56

        .= (((R14 . (y - y0)) + ((R19 . (y - y0)) + (R18 . (y - y0)))) + ((L . (y - y0)) + (R13 . (y - y0))))

        .= (((L . (y - yy0)) + (R13 . (y - y0))) + ((R14 . (y - y0)) + (R20 . (y - y0)))) by A11, RFUNCT_1: 56

        .= ((L . (y - y0)) + (((R13 . (y - y0)) + (R14 . (y - y0))) + (R20 . (y - y0))))

        .= ((L . (y - yy0)) + ((R15 . (y - y0)) + (R20 . (y - y0)))) by A11, RFUNCT_1: 56

        .= ((L . (yy - y0)) + (R . (yy - y0))) by A11, RFUNCT_1: 56;

      end;

      hence thesis by A3, A17, Th14;

    end;

    theorem :: PDIFF_4:30

    f1 is_partial_differentiable_in (u0,3) & f2 is_partial_differentiable_in (u0,3) implies (f1 (#) f2) is_partial_differentiable_in (u0,3)

    proof

      assume that

       A1: f1 is_partial_differentiable_in (u0,3) and

       A2: f2 is_partial_differentiable_in (u0,3);

      consider x0,y0,z0 be Real such that

       A3: u0 = <*x0, y0, z0*> & ex N be Neighbourhood of z0 st N c= ( dom ( SVF1 (3,f1,u0))) & ex L, R st for z st z in N holds ((( SVF1 (3,f1,u0)) . z) - (( SVF1 (3,f1,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A1, Th15;

      consider N1 be Neighbourhood of z0 such that

       A4: N1 c= ( dom ( SVF1 (3,f1,u0))) & ex L, R st for z st z in N1 holds ((( SVF1 (3,f1,u0)) . z) - (( SVF1 (3,f1,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A3;

      consider L1, R1 such that

       A5: for z st z in N1 holds ((( SVF1 (3,f1,u0)) . z) - (( SVF1 (3,f1,u0)) . z0)) = ((L1 . (z - z0)) + (R1 . (z - z0))) by A4;

      consider x1,y1,z1 be Real such that

       A6: u0 = <*x1, y1, z1*> & ex N be Neighbourhood of z1 st N c= ( dom ( SVF1 (3,f2,u0))) & ex L, R st for z st z in N holds ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z1)) = ((L . (z - z1)) + (R . (z - z1))) by A2, Th15;

      x0 = x1 & y0 = y1 & z0 = z1 by A3, A6, FINSEQ_1: 78;

      then

      consider N2 be Neighbourhood of z0 such that

       A7: N2 c= ( dom ( SVF1 (3,f2,u0))) & ex L, R st for z st z in N2 holds ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z0)) = ((L . (z - z0)) + (R . (z - z0))) by A6;

      consider L2, R2 such that

       A8: for z st z in N2 holds ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z0)) = ((L2 . (z - z0)) + (R2 . (z - z0))) by A7;

      consider N be Neighbourhood of z0 such that

       A9: N c= N1 & N c= N2 by RCOMP_1: 17;

      reconsider L11 = ((( SVF1 (3,f2,u0)) . z0) (#) L1) as LinearFunc by FDIFF_1: 3;

      reconsider L12 = ((( SVF1 (3,f1,u0)) . z0) (#) L2) as LinearFunc by FDIFF_1: 3;

      

       A10: L11 is total & L12 is total & L1 is total & L2 is total by FDIFF_1:def 3;

      reconsider L = (L11 + L12) as LinearFunc by FDIFF_1: 2;

      reconsider R11 = ((( SVF1 (3,f2,u0)) . z0) (#) R1), R12 = ((( SVF1 (3,f1,u0)) . z0) (#) R2) as RestFunc by FDIFF_1: 5;

      reconsider R13 = (R11 + R12) as RestFunc by FDIFF_1: 4;

      reconsider R14 = (L1 (#) L2) as RestFunc by FDIFF_1: 6;

      reconsider R15 = (R13 + R14), R17 = (R1 (#) R2) as RestFunc by FDIFF_1: 4;

      reconsider R16 = (R1 (#) L2), R18 = (R2 (#) L1) as RestFunc by FDIFF_1: 7;

      reconsider R19 = (R16 + R17) as RestFunc by FDIFF_1: 4;

      reconsider R20 = (R19 + R18) as RestFunc by FDIFF_1: 4;

      reconsider R = (R15 + R20) as RestFunc by FDIFF_1: 4;

      

       A11: R1 is total & R2 is total & R11 is total & R12 is total & R13 is total & R14 is total & R15 is total & R16 is total & R17 is total & R18 is total & R19 is total & R20 is total by FDIFF_1:def 2;

      

       A12: N c= ( dom ( SVF1 (3,f1,u0))) by A4, A9;

      

       A13: N c= ( dom ( SVF1 (3,f2,u0))) by A7, A9;

      

       A14: for z st z in N holds z in ( dom ( SVF1 (3,(f1 (#) f2),u0)))

      proof

        let z;

        assume

         A15: z in N;

        then

         A16: z in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z) in ( dom f1) by A12, FUNCT_1: 11;

        z in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z) in ( dom f2) by A13, A15, FUNCT_1: 11;

        then z in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z) in (( dom f1) /\ ( dom f2)) by A16, XBOOLE_0:def 4;

        then z in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z) in ( dom (f1 (#) f2)) by VALUED_1:def 4;

        hence thesis by FUNCT_1: 11;

      end;

      then for z be object st z in N holds z in ( dom ( SVF1 (3,(f1 (#) f2),u0)));

      then

       A17: N c= ( dom ( SVF1 (3,(f1 (#) f2),u0)));

      now

        let zz be Real;

        assume

         A18: zz in N;

        reconsider z = zz, zz0 = z0 as Element of REAL by XREAL_0:def 1;

        

         A19: (((( SVF1 (3,f1,u0)) . z) - (( SVF1 (3,f1,u0)) . z0)) + (( SVF1 (3,f1,u0)) . z0)) = (((L1 . (z - z0)) + (R1 . (z - z0))) + (( SVF1 (3,f1,u0)) . z0)) by A5, A9, A18;

        z in ( dom ((f1 (#) f2) * ( reproj (3,u0)))) by A14, A18;

        then

         A20: z in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z) in ( dom (f1 (#) f2)) by FUNCT_1: 11;

        then (( reproj (3,u0)) . z) in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then (( reproj (3,u0)) . z) in ( dom f1) & (( reproj (3,u0)) . z) in ( dom f2) by XBOOLE_0:def 4;

        then

         A21: z in ( dom (f1 * ( reproj (3,u0)))) & z in ( dom (f2 * ( reproj (3,u0)))) by A20, FUNCT_1: 11;

        

         A22: z0 in N by RCOMP_1: 16;

        z0 in ( dom ((f1 (#) f2) * ( reproj (3,u0)))) by A14, RCOMP_1: 16;

        then

         A23: z0 in ( dom ( reproj (3,u0))) & (( reproj (3,u0)) . z0) in ( dom (f1 (#) f2)) by FUNCT_1: 11;

        then (( reproj (3,u0)) . z0) in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then (( reproj (3,u0)) . z0) in ( dom f1) & (( reproj (3,u0)) . z0) in ( dom f2) by XBOOLE_0:def 4;

        then

         A24: z0 in ( dom (f1 * ( reproj (3,u0)))) & z0 in ( dom (f2 * ( reproj (3,u0)))) by A23, FUNCT_1: 11;

        

        thus ((( SVF1 (3,(f1 (#) f2),u0)) . zz) - (( SVF1 (3,(f1 (#) f2),u0)) . z0)) = (((f1 (#) f2) . (( reproj (3,u0)) . z)) - (( SVF1 (3,(f1 (#) f2),u0)) . z0)) by A17, A18, FUNCT_1: 12

        .= (((f1 . (( reproj (3,u0)) . z)) * (f2 . (( reproj (3,u0)) . z))) - (( SVF1 (3,(f1 (#) f2),u0)) . z0)) by VALUED_1: 5

        .= (((( SVF1 (3,f1,u0)) . z) * (f2 . (( reproj (3,u0)) . z))) - (( SVF1 (3,(f1 (#) f2),u0)) . z0)) by A21, FUNCT_1: 12

        .= (((( SVF1 (3,f1,u0)) . z) * (( SVF1 (3,f2,u0)) . z)) - (((f1 (#) f2) * ( reproj (3,u0))) . z0)) by A21, FUNCT_1: 12

        .= (((( SVF1 (3,f1,u0)) . z) * (( SVF1 (3,f2,u0)) . z)) - ((f1 (#) f2) . (( reproj (3,u0)) . z0))) by A17, A22, FUNCT_1: 12

        .= (((( SVF1 (3,f1,u0)) . z) * (( SVF1 (3,f2,u0)) . z)) - ((f1 . (( reproj (3,u0)) . z0)) * (f2 . (( reproj (3,u0)) . z0)))) by VALUED_1: 5

        .= (((( SVF1 (3,f1,u0)) . z) * (( SVF1 (3,f2,u0)) . z)) - ((( SVF1 (3,f1,u0)) . z0) * (f2 . (( reproj (3,u0)) . z0)))) by A24, FUNCT_1: 12

        .= (((((( SVF1 (3,f1,u0)) . z) * (( SVF1 (3,f2,u0)) . z)) + ( - ((( SVF1 (3,f1,u0)) . z) * (( SVF1 (3,f2,u0)) . z0)))) + ((( SVF1 (3,f1,u0)) . z) * (( SVF1 (3,f2,u0)) . z0))) - ((( SVF1 (3,f1,u0)) . z0) * (( SVF1 (3,f2,u0)) . z0))) by A24, FUNCT_1: 12

        .= (((( SVF1 (3,f1,u0)) . z) * ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z0))) + (((( SVF1 (3,f1,u0)) . z) - (( SVF1 (3,f1,u0)) . z0)) * (( SVF1 (3,f2,u0)) . z0)))

        .= (((( SVF1 (3,f1,u0)) . z) * ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z0))) + (((L1 . (z - z0)) + (R1 . (z - z0))) * (( SVF1 (3,f2,u0)) . z0))) by A5, A9, A18

        .= (((( SVF1 (3,f1,u0)) . z) * ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z0))) + (((( SVF1 (3,f2,u0)) . z0) * (L1 . (z - z0))) + ((( SVF1 (3,f2,u0)) . z0) * (R1 . (z - z0)))))

        .= (((( SVF1 (3,f1,u0)) . z) * ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z0))) + ((L11 . (z - z0)) + ((( SVF1 (3,f2,u0)) . z0) * (R1 . (z - zz0))))) by A10, RFUNCT_1: 57

        .= (((((L1 . (z - z0)) + (R1 . (z - z0))) + (( SVF1 (3,f1,u0)) . z0)) * ((( SVF1 (3,f2,u0)) . z) - (( SVF1 (3,f2,u0)) . z0))) + ((L11 . (z - z0)) + (R11 . (z - zz0)))) by A11, A19, RFUNCT_1: 57

        .= (((((L1 . (z - z0)) + (R1 . (z - z0))) + (( SVF1 (3,f1,u0)) . z0)) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L11 . (z - z0)) + (R11 . (z - z0)))) by A8, A9, A18

        .= (((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + (((( SVF1 (3,f1,u0)) . z0) * (L2 . (z - z0))) + ((( SVF1 (3,f1,u0)) . z0) * (R2 . (z - z0))))) + ((L11 . (z - z0)) + (R11 . (z - z0))))

        .= (((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - zz0)))) + ((L12 . (z - z0)) + ((( SVF1 (3,f1,u0)) . z0) * (R2 . (z - z0))))) + ((L11 . (z - z0)) + (R11 . (z - z0)))) by A10, RFUNCT_1: 57

        .= (((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - zz0)))) + ((L12 . (z - z0)) + (R12 . (z - z0)))) + ((L11 . (z - z0)) + (R11 . (z - z0)))) by A11, RFUNCT_1: 57

        .= ((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + ((L12 . (z - z0)) + ((L11 . (z - z0)) + ((R11 . (z - z0)) + (R12 . (z - z0))))))

        .= ((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - zz0)))) + ((L12 . (z - z0)) + ((L11 . (z - z0)) + (R13 . (z - z0))))) by A11, RFUNCT_1: 56

        .= ((((L1 . (z - z0)) + (R1 . (z - z0))) * ((L2 . (z - z0)) + (R2 . (z - z0)))) + (((L11 . (z - z0)) + (L12 . (z - z0))) + (R13 . (z - z0))))

        .= (((((L1 . (z - z0)) * (L2 . (z - z0))) + ((L1 . (z - z0)) * (R2 . (z - z0)))) + ((R1 . (z - zz0)) * ((L2 . (z - z0)) + (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - z0)))) by A10, RFUNCT_1: 56

        .= ((((R14 . (z - z0)) + ((R2 . (z - z0)) * (L1 . (z - z0)))) + ((R1 . (z - z0)) * ((L2 . (z - z0)) + (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - zz0)))) by A10, RFUNCT_1: 56

        .= ((((R14 . (z - z0)) + (R18 . (z - z0))) + (((R1 . (z - z0)) * (L2 . (z - z0))) + ((R1 . (z - z0)) * (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - zz0)))) by A10, A11, RFUNCT_1: 56

        .= ((((R14 . (z - z0)) + (R18 . (z - z0))) + ((R16 . (z - z0)) + ((R1 . (z - z0)) * (R2 . (z - z0))))) + ((L . (z - z0)) + (R13 . (z - zz0)))) by A10, A11, RFUNCT_1: 56

        .= ((((R14 . (z - z0)) + (R18 . (z - z0))) + ((R16 . (z - z0)) + (R17 . (z - z0)))) + ((L . (z - z0)) + (R13 . (z - z0)))) by A11, RFUNCT_1: 56

        .= ((((R14 . (z - zz0)) + (R18 . (z - z0))) + (R19 . (z - z0))) + ((L . (z - z0)) + (R13 . (z - z0)))) by A11, RFUNCT_1: 56

        .= (((R14 . (z - z0)) + ((R19 . (z - z0)) + (R18 . (z - z0)))) + ((L . (z - z0)) + (R13 . (z - z0))))

        .= (((L . (z - zz0)) + (R13 . (z - z0))) + ((R14 . (z - z0)) + (R20 . (z - z0)))) by A11, RFUNCT_1: 56

        .= ((L . (z - z0)) + (((R13 . (z - z0)) + (R14 . (z - z0))) + (R20 . (z - z0))))

        .= ((L . (z - zz0)) + ((R15 . (z - z0)) + (R20 . (z - zz0)))) by A11, RFUNCT_1: 56

        .= ((L . (zz - z0)) + (R . (zz - z0))) by A11, RFUNCT_1: 56;

      end;

      hence thesis by A3, A17, Th15;

    end;

    theorem :: PDIFF_4:31

    for u0 be Element of ( REAL 3) holds f is_partial_differentiable_in (u0,1) implies ( SVF1 (1,f,u0)) is_continuous_in (( proj (1,3)) . u0) by FDIFF_1: 24;

    theorem :: PDIFF_4:32

    for u0 be Element of ( REAL 3) holds f is_partial_differentiable_in (u0,2) implies ( SVF1 (2,f,u0)) is_continuous_in (( proj (2,3)) . u0) by FDIFF_1: 24;

    theorem :: PDIFF_4:33

    for u0 be Element of ( REAL 3) holds f is_partial_differentiable_in (u0,3) implies ( SVF1 (3,f,u0)) is_continuous_in (( proj (3,3)) . u0) by FDIFF_1: 24;

    begin

    

     Lm4: ( |[x1, y1, z1]| + |[x2, y2, z2]|) = |[(x1 + x2), (y1 + y2), (z1 + z2)]|

    proof

      

       A1: ( |[x2, y2, z2]| . 1) = x2 by FINSEQ_1: 45;

      

       A2: ( |[x2, y2, z2]| . 2) = y2 by FINSEQ_1: 45;

      

       A3: ( |[x2, y2, z2]| . 3) = z2 by FINSEQ_1: 45;

      

       A4: (( |[x1, y1, z1]| . 1) + ( |[x2, y2, z2]| . 1)) = (x1 + x2) by A1, FINSEQ_1: 45;

      

       A5: (( |[x1, y1, z1]| . 2) + ( |[x2, y2, z2]| . 2)) = (y1 + y2) by A2, FINSEQ_1: 45;

      (( |[x1, y1, z1]| . 3) + ( |[x2, y2, z2]| . 3)) = (z1 + z2) by A3, FINSEQ_1: 45;

      hence thesis by A4, A5, EUCLID_8: 55;

    end;

    definition

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

      let p be Element of ( REAL 3);

      :: PDIFF_4:def7

      func grad (f,p) -> Element of ( REAL 3) equals (((( partdiff (f,p,1)) * <e1> ) + (( partdiff (f,p,2)) * <e2> )) + (( partdiff (f,p,3)) * <e3> ));

      coherence ;

    end

    reconsider jj = 1 as Real;

    theorem :: PDIFF_4:34

    

     Th34: ( grad (f,p)) = |[( partdiff (f,p,1)), ( partdiff (f,p,2)), ( partdiff (f,p,3))]|

    proof

      ( grad (f,p)) = (( |[(( partdiff (f,p,1)) * 1), (( partdiff (f,p,1)) * 0 ), (( partdiff (f,p,1)) * 0 )]| + (( partdiff (f,p,2)) * |[ 0 , jj, 0 ]|)) + (( partdiff (f,p,3)) * |[ 0 , 0 , jj]|)) by EUCLID_8: 59

      .= (( |[( partdiff (f,p,1)), 0 , 0 ]| + |[(( partdiff (f,p,2)) * 0 ), (( partdiff (f,p,2)) * 1), (( partdiff (f,p,2)) * 0 )]|) + (( partdiff (f,p,3)) * |[ 0 , 0 , jj]|)) by EUCLID_8: 59

      .= (( |[( partdiff (f,p,1)), 0 , 0 ]| + |[ 0 , ( partdiff (f,p,2)), 0 ]|) + |[(( partdiff (f,p,3)) * 0 ), (( partdiff (f,p,3)) * 0 ), (( partdiff (f,p,3)) * 1)]|) by EUCLID_8: 59

      .= ( |[(( partdiff (f,p,1)) + 0 ), ( 0 + ( partdiff (f,p,2))), ( 0 + 0 )]| + |[ 0 , 0 , ( partdiff (f,p,3))]|) by Lm4

      .= |[(( partdiff (f,p,1)) + 0 ), (( partdiff (f,p,2)) + 0 ), ( 0 + ( partdiff (f,p,3)))]| by Lm4

      .= |[( partdiff (f,p,1)), ( partdiff (f,p,2)), ( partdiff (f,p,3))]|;

      hence thesis;

    end;

    theorem :: PDIFF_4:35

    

     Th35: (f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3) & g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3)) implies ( grad ((f + g),p)) = (( grad (f,p)) + ( grad (g,p)))

    proof

      assume that

       A1: f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3) and

       A2: g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3);

      ( grad ((f + g),p)) = |[( partdiff ((f + g),p,1)), ( partdiff ((f + g),p,2)), ( partdiff ((f + g),p,3))]| by Th34

      .= |[(( partdiff (f,p,1)) + ( partdiff (g,p,1))), ( partdiff ((f + g),p,2)), ( partdiff ((f + g),p,3))]| by A1, A2, PDIFF_1: 29

      .= |[(( partdiff (f,p,1)) + ( partdiff (g,p,1))), (( partdiff (f,p,2)) + ( partdiff (g,p,2))), ( partdiff ((f + g),p,3))]| by A1, A2, PDIFF_1: 29

      .= |[(( partdiff (f,p,1)) + ( partdiff (g,p,1))), (( partdiff (f,p,2)) + ( partdiff (g,p,2))), (( partdiff (f,p,3)) + ( partdiff (g,p,3)))]| by A1, A2, PDIFF_1: 29

      .= ( |[( partdiff (f,p,1)), ( partdiff (f,p,2)), ( partdiff (f,p,3))]| + |[( partdiff (g,p,1)), ( partdiff (g,p,2)), ( partdiff (g,p,3))]|) by Lm4

      .= (( grad (f,p)) + |[( partdiff (g,p,1)), ( partdiff (g,p,2)), ( partdiff (g,p,3))]|) by Th34

      .= (( grad (f,p)) + ( grad (g,p))) by Th34;

      hence thesis;

    end;

    theorem :: PDIFF_4:36

    

     Th36: (f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3) & g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3)) implies ( grad ((f - g),p)) = (( grad (f,p)) - ( grad (g,p)))

    proof

      assume that

       A1: f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3) and

       A2: g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3);

      ( grad ((f - g),p)) = |[( partdiff ((f - g),p,1)), ( partdiff ((f - g),p,2)), ( partdiff ((f - g),p,3))]| by Th34

      .= |[(( partdiff (f,p,1)) - ( partdiff (g,p,1))), ( partdiff ((f - g),p,2)), ( partdiff ((f - g),p,3))]| by A1, A2, PDIFF_1: 31

      .= |[(( partdiff (f,p,1)) - ( partdiff (g,p,1))), (( partdiff (f,p,2)) - ( partdiff (g,p,2))), ( partdiff ((f - g),p,3))]| by A1, A2, PDIFF_1: 31

      .= |[(( partdiff (f,p,1)) - ( partdiff (g,p,1))), (( partdiff (f,p,2)) - ( partdiff (g,p,2))), (( partdiff (f,p,3)) - ( partdiff (g,p,3)))]| by A1, A2, PDIFF_1: 31

      .= |[(( partdiff (f,p,1)) + ( - ( partdiff (g,p,1)))), (( partdiff (f,p,2)) + ( - ( partdiff (g,p,2)))), (( partdiff (f,p,3)) + ( - ( partdiff (g,p,3))))]|

      .= ( |[( partdiff (f,p,1)), ( partdiff (f,p,2)), ( partdiff (f,p,3))]| + |[( - ( partdiff (g,p,1))), ( - ( partdiff (g,p,2))), ( - ( partdiff (g,p,3)))]|) by Lm4

      .= (( grad (f,p)) + |[(( - 1) * ( partdiff (g,p,1))), (( - 1) * ( partdiff (g,p,2))), (( - 1) * ( partdiff (g,p,3)))]|) by Th34

      .= (( grad (f,p)) + (( - 1) * |[( partdiff (g,p,1)), ( partdiff (g,p,2)), ( partdiff (g,p,3))]|)) by EUCLID_8: 59

      .= (( grad (f,p)) - ( grad (g,p))) by Th34;

      hence thesis;

    end;

    theorem :: PDIFF_4:37

    

     Th37: (f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3)) implies ( grad ((r (#) f),p)) = (r * ( grad (f,p)))

    proof

      assume

       A1: f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3);

      reconsider r as Real;

      ( grad ((r (#) f),p)) = |[( partdiff ((r (#) f),p,1)), ( partdiff ((r (#) f),p,2)), ( partdiff ((r (#) f),p,3))]| by Th34

      .= |[(r * ( partdiff (f,p,1))), ( partdiff ((r (#) f),p,2)), ( partdiff ((r (#) f),p,3))]| by A1, PDIFF_1: 33

      .= |[(r * ( partdiff (f,p,1))), (r * ( partdiff (f,p,2))), ( partdiff ((r (#) f),p,3))]| by A1, PDIFF_1: 33

      .= |[(r * ( partdiff (f,p,1))), (r * ( partdiff (f,p,2))), (r * ( partdiff (f,p,3)))]| by A1, PDIFF_1: 33

      .= (r * |[( partdiff (f,p,1)), ( partdiff (f,p,2)), ( partdiff (f,p,3))]|) by EUCLID_8: 59

      .= (r * ( grad (f,p))) by Th34;

      hence thesis;

    end;

    theorem :: PDIFF_4:38

    (f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3)) & (g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3)) implies ( grad (((s (#) f) + (t (#) g)),p)) = ((s * ( grad (f,p))) + (t * ( grad (g,p))))

    proof

      assume that

       A1: f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3) and

       A2: g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3);

      reconsider s, t as Real;

      

       A3: (s (#) f) is_partial_differentiable_in (p,1) & (s (#) f) is_partial_differentiable_in (p,2) & (s (#) f) is_partial_differentiable_in (p,3) by A1, PDIFF_1: 33;

      (t (#) g) is_partial_differentiable_in (p,1) & (t (#) g) is_partial_differentiable_in (p,2) & (t (#) g) is_partial_differentiable_in (p,3) by A2, PDIFF_1: 33;

      

      then ( grad (((s (#) f) + (t (#) g)),p)) = (( grad ((s (#) f),p)) + ( grad ((t (#) g),p))) by A3, Th35

      .= ((s * ( grad (f,p))) + ( grad ((t (#) g),p))) by A1, Th37

      .= ((s * ( grad (f,p))) + (t * ( grad (g,p)))) by A2, Th37;

      hence thesis;

    end;

    theorem :: PDIFF_4:39

    (f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3)) & (g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3)) implies ( grad (((s (#) f) - (t (#) g)),p)) = ((s * ( grad (f,p))) - (t * ( grad (g,p))))

    proof

      assume that

       A1: f is_partial_differentiable_in (p,1) & f is_partial_differentiable_in (p,2) & f is_partial_differentiable_in (p,3) and

       A2: g is_partial_differentiable_in (p,1) & g is_partial_differentiable_in (p,2) & g is_partial_differentiable_in (p,3);

      reconsider s, t as Real;

      

       A3: (s (#) f) is_partial_differentiable_in (p,1) & (s (#) f) is_partial_differentiable_in (p,2) & (s (#) f) is_partial_differentiable_in (p,3) by A1, PDIFF_1: 33;

      (t (#) g) is_partial_differentiable_in (p,1) & (t (#) g) is_partial_differentiable_in (p,2) & (t (#) g) is_partial_differentiable_in (p,3) by A2, PDIFF_1: 33;

      

      then ( grad (((s (#) f) - (t (#) g)),p)) = (( grad ((s (#) f),p)) - ( grad ((t (#) g),p))) by A3, Th36

      .= ((s * ( grad (f,p))) - ( grad ((t (#) g),p))) by A1, Th37

      .= ((s * ( grad (f,p))) - (t * ( grad (g,p)))) by A2, Th37;

      hence thesis;

    end;

    theorem :: PDIFF_4:40

    f is total & f is constant implies ( grad (f,p)) = ( 0.REAL 3)

    proof

      assume

       A1: f is total & f is constant;

      then

       A2: ( dom f) = ( REAL 3) by FUNCT_2:def 1;

       REAL = ( [#] REAL );

      then

      reconsider W = REAL as open Subset of REAL ;

      consider a be Element of REAL such that

       A3: for p st p in ( REAL 3) holds (f . p) = a by A1, A2, PARTFUN2:def 1;

      now

        let x be Element of REAL ;

        assume x in ( dom (f * ( reproj (1,p))));

        then ((f * ( reproj (1,p))) . x) = (f . (( reproj (1,p)) . x)) by FUNCT_1: 12;

        hence ((f * ( reproj (1,p))) . x) = a by A3;

      end;

      then

       A4: (f * ( reproj (1,p))) is constant by PARTFUN2:def 1;

      set g1 = (f * ( reproj (1,p)));

      

       A5: ( dom g1) = W by A1, FUNCT_2:def 1;

      

       A6: (g1 | W) is constant by A4;

      then

       A7: g1 is_differentiable_on REAL by A5, FDIFF_1: 22;

      for x st x in REAL holds ( diff (g1,x)) = 0

      proof

        let x;

        assume x in REAL ;

        reconsider x as Element of REAL by XREAL_0:def 1;

        ( diff (g1,x)) = ((g1 `| W) . x) by A7, FDIFF_1:def 7

        .= 0 by A5, A6, FDIFF_1: 22;

        hence thesis;

      end;

      then

       A8: ( partdiff (f,p,1)) = 0 ;

      now

        let y be Element of REAL ;

        assume y in ( dom (f * ( reproj (2,p))));

        then ((f * ( reproj (2,p))) . y) = (f . (( reproj (2,p)) . y)) by FUNCT_1: 12;

        hence ((f * ( reproj (2,p))) . y) = a by A3;

      end;

      then

       A9: (f * ( reproj (2,p))) is constant by PARTFUN2:def 1;

      set g2 = (f * ( reproj (2,p)));

      

       A10: ( dom g2) = W by A1, FUNCT_2:def 1;

      

       A11: (g2 | W) is constant by A9;

      then

       A12: g2 is_differentiable_on REAL & for y be Real st y in REAL holds ((g2 `| W) . y) = 0 by A10, FDIFF_1: 22;

      for y st y in REAL holds ( diff (g2,y)) = 0

      proof

        let y;

        assume y in REAL ;

        reconsider y as Element of REAL by XREAL_0:def 1;

        ( diff (g2,y)) = ((g2 `| W) . y) by A12, FDIFF_1:def 7

        .= 0 by A10, A11, FDIFF_1: 22;

        hence thesis;

      end;

      then

       A13: ( partdiff (f,p,2)) = 0 ;

      now

        let z be Element of REAL ;

        assume z in ( dom (f * ( reproj (3,p))));

        then ((f * ( reproj (3,p))) . z) = (f . (( reproj (3,p)) . z)) by FUNCT_1: 12;

        hence ((f * ( reproj (3,p))) . z) = a by A3;

      end;

      then

       A14: (f * ( reproj (3,p))) is constant by PARTFUN2:def 1;

      set g3 = (f * ( reproj (3,p)));

      

       A15: ( dom g3) = W by A1, FUNCT_2:def 1;

      

       A16: (g3 | W) is constant by A14;

      then

       A17: g3 is_differentiable_on REAL & for z be Real st z in REAL holds ((g3 `| W) . z) = 0 by A15, FDIFF_1: 22;

      for z st z in REAL holds ( diff (g3,z)) = 0

      proof

        let z;

        assume z in REAL ;

        reconsider z as Element of REAL by XREAL_0:def 1;

        ( diff (g3,z)) = ((g3 `| W) . z) by A17, FDIFF_1:def 7

        .= 0 by A15, A16, FDIFF_1: 22;

        hence thesis;

      end;

      then ( partdiff (f,p,3)) = 0 ;

      

      then ( grad (f,p)) = |[ 0 , 0 , 0 ]| by A8, A13, Th34

      .= ( 0.REAL 3) by FINSEQ_2: 62;

      hence thesis;

    end;

    definition

      let a be Element of ( REAL 3);

      :: PDIFF_4:def8

      func unitvector (a) -> Element of ( REAL 3) equals |[((a . 1) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))), ((a . 2) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))), ((a . 3) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))]|;

      coherence ;

    end

    definition

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

      let p,a be Element of ( REAL 3);

      :: PDIFF_4:def9

      func Directiondiff (f,p,a) -> Real equals (((( partdiff (f,p,1)) * (( unitvector a) . 1)) + (( partdiff (f,p,2)) * (( unitvector a) . 2))) + (( partdiff (f,p,3)) * (( unitvector a) . 3)));

      coherence ;

    end

    theorem :: PDIFF_4:41

    a = <*x0, y0, z0*> implies ( Directiondiff (f,p,a)) = ((((( partdiff (f,p,1)) * x0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + ((( partdiff (f,p,2)) * y0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + ((( partdiff (f,p,3)) * z0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))))

    proof

      assume

       A1: a = <*x0, y0, z0*>;

      

      then

       A2: ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))) = ( sqrt (((x0 ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))) by FINSEQ_1: 45

      .= ( sqrt (((x0 ^2 ) + (y0 ^2 )) + ((a . 3) ^2 ))) by A1, FINSEQ_1: 45

      .= ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))) by A1, FINSEQ_1: 45;

      ( Directiondiff (f,p,a)) = (((( partdiff (f,p,1)) * ((a . 1) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + (( partdiff (f,p,2)) * (( unitvector a) . 2))) + (( partdiff (f,p,3)) * (( unitvector a) . 3))) by FINSEQ_1: 45

      .= ((((( partdiff (f,p,1)) * (a . 1)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + (( partdiff (f,p,2)) * (( unitvector a) . 2))) + (( partdiff (f,p,3)) * (( unitvector a) . 3))) by XCMPLX_1: 74

      .= ((((( partdiff (f,p,1)) * (a . 1)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + (( partdiff (f,p,2)) * ((a . 2) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))))) + (( partdiff (f,p,3)) * (( unitvector a) . 3))) by FINSEQ_1: 45

      .= ((((( partdiff (f,p,1)) * (a . 1)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + ((( partdiff (f,p,2)) * (a . 2)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + (( partdiff (f,p,3)) * (( unitvector a) . 3))) by XCMPLX_1: 74

      .= ((((( partdiff (f,p,1)) * (a . 1)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + ((( partdiff (f,p,2)) * (a . 2)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + (( partdiff (f,p,3)) * ((a . 3) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))))) by FINSEQ_1: 45

      .= ((((( partdiff (f,p,1)) * (a . 1)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + ((( partdiff (f,p,2)) * (a . 2)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + ((( partdiff (f,p,3)) * (a . 3)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) by XCMPLX_1: 74

      .= ((((( partdiff (f,p,1)) * x0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + ((( partdiff (f,p,2)) * (a . 2)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + ((( partdiff (f,p,3)) * (a . 3)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) by A1, A2, FINSEQ_1: 45

      .= ((((( partdiff (f,p,1)) * x0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + ((( partdiff (f,p,2)) * y0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + ((( partdiff (f,p,3)) * (a . 3)) / ( sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) by A1, A2, FINSEQ_1: 45

      .= ((((( partdiff (f,p,1)) * x0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + ((( partdiff (f,p,2)) * y0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + ((( partdiff (f,p,3)) * z0) / ( sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) by A1, A2, FINSEQ_1: 45;

      hence thesis;

    end;

    theorem :: PDIFF_4:42

    ( Directiondiff (f,p,a)) = |(( grad (f,p)), ( unitvector a))|

    proof

      set p0 = ( grad (f,p));

      reconsider g1 = p0, g2 = ( unitvector a) as FinSequence of REAL ;

      

       A1: ( len g1) = ( len <*(p0 . 1), (p0 . 2), (p0 . 3)*>) by EUCLID_8: 1

      .= 3 by FINSEQ_1: 45;

      

       A2: ( len g2) = 3 by FINSEQ_1: 45;

      

       A3: p0 = |[( partdiff (f,p,1)), ( partdiff (f,p,2)), ( partdiff (f,p,3))]| by Th34;

       |(( grad (f,p)), ( unitvector a))| = ( Sum <*((g1 . 1) * (g2 . 1)), ((g1 . 2) * (g2 . 2)), ((g1 . 3) * (g2 . 3))*>) by A1, A2, EUCLID_5: 28

      .= ((((p0 . 1) * (g2 . 1)) + ((p0 . 2) * (g2 . 2))) + ((p0 . 3) * (g2 . 3))) by RVSUM_1: 78

      .= (((( partdiff (f,p,1)) * (g2 . 1)) + ((p0 . 2) * (g2 . 2))) + ((p0 . 3) * (g2 . 3))) by A3, FINSEQ_1: 45

      .= (((( partdiff (f,p,1)) * (g2 . 1)) + (( partdiff (f,p,2)) * (g2 . 2))) + ((p0 . 3) * (g2 . 3))) by A3, FINSEQ_1: 45

      .= ( Directiondiff (f,p,a)) by A3, FINSEQ_1: 45;

      hence thesis;

    end;

    definition

      let f1,f2,f3 be PartFunc of ( REAL 3), REAL ;

      let p be Element of ( REAL 3);

      :: PDIFF_4:def10

      func curl (f1,f2,f3,p) -> Element of ( REAL 3) equals ((((( partdiff (f3,p,2)) - ( partdiff (f2,p,3))) * <e1> ) + ((( partdiff (f1,p,3)) - ( partdiff (f3,p,1))) * <e2> )) + ((( partdiff (f2,p,1)) - ( partdiff (f1,p,2))) * <e3> ));

      coherence ;

    end

    theorem :: PDIFF_4:43

    ( curl (f1,f2,f3,p)) = |[(( partdiff (f3,p,2)) - ( partdiff (f2,p,3))), (( partdiff (f1,p,3)) - ( partdiff (f3,p,1))), (( partdiff (f2,p,1)) - ( partdiff (f1,p,2)))]|

    proof

      ( curl (f1,f2,f3,p)) = (( |[((( partdiff (f3,p,2)) - ( partdiff (f2,p,3))) * 1), ((( partdiff (f3,p,2)) - ( partdiff (f2,p,3))) * 0 ), ((( partdiff (f3,p,2)) - ( partdiff (f2,p,3))) * 0 )]| + ((( partdiff (f1,p,3)) - ( partdiff (f3,p,1))) * |[ 0 , jj, 0 ]|)) + ((( partdiff (f2,p,1)) - ( partdiff (f1,p,2))) * |[ 0 , 0 , jj]|)) by EUCLID_8: 59

      .= (( |[(( partdiff (f3,p,2)) - ( partdiff (f2,p,3))), 0 , 0 ]| + |[((( partdiff (f1,p,3)) - ( partdiff (f3,p,1))) * 0 ), ((( partdiff (f1,p,3)) - ( partdiff (f3,p,1))) * 1), ((( partdiff (f1,p,3)) - ( partdiff (f3,p,1))) * 0 )]|) + ((( partdiff (f2,p,1)) - ( partdiff (f1,p,2))) * |[ 0 , 0 , jj]|)) by EUCLID_8: 59

      .= (( |[(( partdiff (f3,p,2)) - ( partdiff (f2,p,3))), 0 , 0 ]| + |[ 0 , (( partdiff (f1,p,3)) - ( partdiff (f3,p,1))), 0 ]|) + |[((( partdiff (f2,p,1)) - ( partdiff (f1,p,2))) * 0 ), ((( partdiff (f2,p,1)) - ( partdiff (f1,p,2))) * 0 ), ((( partdiff (f2,p,1)) - ( partdiff (f1,p,2))) * 1)]|) by EUCLID_8: 59

      .= ( |[((( partdiff (f3,p,2)) - ( partdiff (f2,p,3))) + 0 ), ( 0 + (( partdiff (f1,p,3)) - ( partdiff (f3,p,1)))), ( 0 + 0 )]| + |[ 0 , 0 , (( partdiff (f2,p,1)) - ( partdiff (f1,p,2)))]|) by Lm4

      .= |[((( partdiff (f3,p,2)) - ( partdiff (f2,p,3))) + 0 ), ((( partdiff (f1,p,3)) - ( partdiff (f3,p,1))) + 0 ), ( 0 + (( partdiff (f2,p,1)) - ( partdiff (f1,p,2))))]| by Lm4

      .= |[(( partdiff (f3,p,2)) - ( partdiff (f2,p,3))), (( partdiff (f1,p,3)) - ( partdiff (f3,p,1))), (( partdiff (f2,p,1)) - ( partdiff (f1,p,2)))]|;

      hence thesis;

    end;