pdiff_2.miz

    begin

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

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

    reserve n,m,k for Element of NAT ;

    reserve Z for Subset of ( REAL 2);

    reserve s1 for Real_Sequence;

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

    reserve R,R1,R2 for RestFunc;

    reserve L,L1,L2 for LinearFunc;

    theorem :: PDIFF_2:1



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

    proof

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

      for x be object st x in REAL holds ex z be object st z in ( REAL 2) & x = (f . z)

      proof

        set y = the Element of REAL ;

        let x be object;

        assume x in REAL ;

        then

        reconsider x1 = x as Element of REAL ;

        reconsider z = <*x1, y*> as Element of ( REAL 2) by FINSEQ_2: 101;

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

        then (f . z) = x by FINSEQ_1: 44;

        hence thesis;

      end;

      hence ( dom ( proj (1,2))) = ( REAL 2) & ( rng ( proj (1,2))) = REAL by FUNCT_2: 10, FUNCT_2:def 1;

      let x,y be Real;

      reconsider x, y as Element of REAL by XREAL_0:def 1;

      now

        let x,y be Element of REAL ;

         <*x, y*> is Element of (2 -tuples_on REAL ) by FINSEQ_2: 101;

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

        hence (( proj (1,2)) . <*x, y*>) = x by FINSEQ_1: 44;

      end;

      then (( proj (1,2)) . <*x, y*>) = x;

      hence thesis;

    end;

    theorem :: PDIFF_2:2



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

    proof

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

      for y be object st y in REAL holds ex z be object st z in ( REAL 2) & y = (f . z)

      proof

        set x = the Element of REAL ;

        let y be object;

        assume y in REAL ;

        then

        reconsider y1 = y as Element of REAL ;

        reconsider z = <*x, y1*> as Element of ( REAL 2) by FINSEQ_2: 101;

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

        then (f . z) = y by FINSEQ_1: 44;

        hence thesis;

      end;

      hence ( dom ( proj (2,2))) = ( REAL 2) & ( rng ( proj (2,2))) = REAL by FUNCT_2: 10, FUNCT_2:def 1;

      let x,y be Real;

      reconsider x, y as Element of REAL by XREAL_0:def 1;

      now

        let x,y be Element of REAL ;

         <*x, y*> is Element of (2 -tuples_on REAL ) by FINSEQ_2: 101;

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

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

      end;

      then (( proj (2,2)) . <*x, y*>) = y;

      hence thesis;

    end;

    begin

    definition

      let n,i be Element of NAT ;

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

      let z be Element of ( REAL n);

      :: PDIFF_2:def1

      func SVF1 (i,f,z) -> PartFunc of REAL , REAL equals (f * ( reproj (i,z)));

      coherence ;

    end

    theorem :: PDIFF_2:3



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

    theorem :: PDIFF_2:4



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

    theorem :: PDIFF_2:5



     Th5: for f be PartFunc of ( REAL 2), REAL holds for z be Element of ( REAL 2) holds (ex x0,y0 be Real st z = <*x0, y0*> & ( SVF1 (1,f,z)) is_differentiable_in x0) iff f is_partial_differentiable_in (z,1)

    proof

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

      let z be Element of ( REAL 2);

      consider x0,y0 be Element of REAL such that

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

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

      assume

       A2: f is_partial_differentiable_in (z,1);

      (( proj (1,2)) . z) = x0 by A1, Th1;

      then ( SVF1 (1,f,z)) is_differentiable_in x0 by A2;

      hence thesis by A1;

    end;

    theorem :: PDIFF_2:6



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

    proof

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

      let z be Element of ( REAL 2);

      consider x0,y0 be Element of REAL such that

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

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

      assume

       A2: f is_partial_differentiable_in (z,2);

      (( proj (2,2)) . z) = y0 by A1, Th2;

      then ( SVF1 (2,f,z)) is_differentiable_in y0 by A2;

      hence thesis by A1;

    end;

    theorem :: PDIFF_2:7

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

    proof

      assume that

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

       A2: f is_partial_differentiable_in (z,1);

      ex x1, y1 st z = <*x1, y1*> & ( SVF1 (1,f,z)) is_differentiable_in x1 by A2, Th5;

      then ( SVF1 (1,f,z)) is_differentiable_in x0 by A1, FINSEQ_1: 77;

      hence thesis by FDIFF_1:def 4;

    end;

    theorem :: PDIFF_2:8

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

    proof

      assume that

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

       A2: f is_partial_differentiable_in (z,2);

      ex x1, y1 st z = <*x1, y1*> & ( SVF1 (2,f,z)) is_differentiable_in y1 by A2, Th6;

      then ( SVF1 (2,f,z)) is_differentiable_in y0 by A1, FINSEQ_1: 77;

      hence thesis by FDIFF_1:def 4;

    end;

    theorem :: PDIFF_2:9



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

    proof

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

      let z be Element of ( REAL 2);

      hereby

        assume

         A1: f is_partial_differentiable_in (z,1);

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

        proof

          consider x0, y0 such that

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

           A3: ( SVF1 (1,f,z)) is_differentiable_in x0 by A1, Th5;

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

          hence thesis by A2;

        end;

      end;

      given x0,y0 be Real such that

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

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

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

      hence thesis by A4, Th5;

    end;

    theorem :: PDIFF_2:10



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

    proof

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

      let z be Element of ( REAL 2);

      hereby

        assume

         A1: f is_partial_differentiable_in (z,2);

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

        proof

          consider x0, y0 such that

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

           A3: ( SVF1 (2,f,z)) is_differentiable_in y0 by A1, Th6;

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

          hence thesis by A2;

        end;

      end;

      given x0, y0 such that

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

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

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

      hence thesis by A4, Th6;

    end;



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

    proof

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

      assume that

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

       A2: f is_partial_differentiable_in (z,1);



       A3: F1 is_differentiable_in x0 by A1, A2, Th3;

      hereby

        assume

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

        F1 is_differentiable_in x0 by A1, A2, Th3;

        then ex N be Neighbourhood of x0 st 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 A4, FDIFF_1:def 5;

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

      end;

      given x1,y1 be Real such that

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

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

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

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

    end;



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

    proof

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

      assume that

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

       A2: f is_partial_differentiable_in (z,2);



       A3: F1 is_differentiable_in y0 by A1, A2, Th4;

      hereby

        assume

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

        F1 is_differentiable_in y0 by A1, A2, Th4;

        then 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 ((F1 . y) - (F1 . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A4, FDIFF_1:def 5;

        hence ex x0,y0 be Real st z = <*x0, y0*> & 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,z)) . y) - (( SVF1 (2,f,z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1;

      end;

      given x1,y1 be Real such that

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

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

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

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

    end;

    theorem :: PDIFF_2:11



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

    proof

      assume that

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

       A2: f is_partial_differentiable_in (z,1);

      hereby

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

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

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

      end;

      given x1,y1 be Real such that

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

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

      hence thesis by A1, Th1;

    end;

    theorem :: PDIFF_2:12



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

    proof

      assume that

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

       A2: f is_partial_differentiable_in (z,2);

      hereby

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

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

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

      end;

      given x1,y1 be Real such that

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

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

      hence thesis by A1, Th2;

    end;

    theorem :: PDIFF_2:13

    z = <*x0, y0*> & f is_partial_differentiable_in (z,1) implies ( partdiff (f,z,1)) = ( diff (( SVF1 (1,f,z)),x0))

    proof

      set r = ( partdiff (f,z,1));

      assume that

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

       A2: f is_partial_differentiable_in (z,1);

      consider x1,y1 be Real such that

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

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

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

      then

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

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

      consider L, R such that

       A6: r = (L . 1) and

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

      consider r1 such that

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



       A9: r = (r1 * 1) by A6, A8;

      consider x2, y2 such that

       A10: z = <*x2, y2*> and

       A11: ( SVF1 (1,f,z)) is_differentiable_in x2 by A2, Th5;

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

       A12: ex L, R st ( diff (( SVF1 (1,f,z)),x2)) = (L . 1) & for x st x in N1 holds ((( SVF1 (1,f,z)) . x) - (( SVF1 (1,f,z)) . x2)) = ((L . (x - x2)) + (R . (x - x2))) by A11, FDIFF_1:def 5;

      consider L1, R1 such that

       A13: ( diff (( SVF1 (1,f,z)),x2)) = (L1 . 1) and

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

      consider p1 such that

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



       A16: x0 = x2 by A1, A10, FINSEQ_1: 77;

      then

      consider N0 be Neighbourhood of x0 such that

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

      consider g be Real such that

       A18: 0 < g and

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

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

      consider s1 such that

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

      now

        let n be Nat;

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

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

      end;

      then

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

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

      then

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



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

      proof

        let n;

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

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

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

        then

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

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

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

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

        hence thesis by A17, A19, A20;

      end;



       A24: ( diff (( SVF1 (1,f,z)),x2)) = (p1 * 1) by A13, A15;

       A25:

      now

        let x;

        assume that

         A26: x in N and

         A27: x in N1;

        ((( SVF1 (1,f,z)) . x) - (( SVF1 (1,f,z)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A7, A26;

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

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

        hence ((r * (x - x0)) + (R . (x - x0))) = ((( diff (( SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0))) by A15, A9, A24;

      end;

      reconsider rd = (r - ( diff (( SVF1 (1,f,z)),x2))) as Element of REAL by XREAL_0:def 1;

      now

        R1 is total by FDIFF_1:def 2;

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

        then

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

        let n be Nat;

        R is total by FDIFF_1:def 2;

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

        then

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



         A30: n in NAT by ORDINAL1:def 12;

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

        then ((r * (h . n)) + (R . (h . n))) = ((( diff (( SVF1 (1,f,z)),x2)) * (h . n)) + (R1 . (h . n))) by A25;

        then

         A31: (((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n))) = (((( diff (( SVF1 (1,f,z)),x2)) * (h . n)) + (R1 . (h . n))) / (h . n)) by XCMPLX_1: 62;



         A32: ((R . (h . n)) / (h . n)) = ((R . (h . n)) * ((h . n) " )) by XCMPLX_0:def 9

        .= ((R . (h . n)) * ((h " ) . n)) by VALUED_1: 10

        .= (((R /* h) . n) * ((h " ) . n)) by A30, A29, FUNCT_2: 108

        .= (((h " ) (#) (R /* h)) . n) by SEQ_1: 8;



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



         A34: ((R1 . (h . n)) / (h . n)) = ((R1 . (h . n)) * ((h . n) " )) by XCMPLX_0:def 9

        .= ((R1 . (h . n)) * ((h " ) . n)) by VALUED_1: 10

        .= (((R1 /* h) . n) * ((h " ) . n)) by A30, A28, FUNCT_2: 108

        .= (((h " ) (#) (R1 /* h)) . n) by SEQ_1: 8;



         A35: ((( diff (( SVF1 (1,f,z)),x2)) * (h . n)) / (h . n)) = (( diff (( SVF1 (1,f,z)),x2)) * ((h . n) / (h . n))) by XCMPLX_1: 74

        .= (( diff (( SVF1 (1,f,z)),x2)) * 1) by A33, XCMPLX_1: 60

        .= ( diff (( SVF1 (1,f,z)),x2));

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

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

        .= r;

        then (r + ((R . (h . n)) / (h . n))) = (( diff (( SVF1 (1,f,z)),x2)) + ((R1 . (h . n)) / (h . n))) by A31, A35, XCMPLX_1: 62;

        then r = (( diff (( SVF1 (1,f,z)),x2)) + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by A32, A34;

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

      end;

      then (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) is constant & ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1) = (r - ( diff (( SVF1 (1,f,z)),x2))) by VALUED_0:def 18;

      then

       A36: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - ( diff (( SVF1 (1,f,z)),x2))) by SEQ_4: 25;



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

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

      then (r - ( diff (( SVF1 (1,f,z)),x2))) = ( 0 - 0 ) by A36, A37, SEQ_2: 12;

      hence thesis by A1, A10, FINSEQ_1: 77;

    end;

    theorem :: PDIFF_2:14

    z = <*x0, y0*> & f is_partial_differentiable_in (z,2) implies ( partdiff (f,z,2)) = ( diff (( SVF1 (2,f,z)),y0))

    proof

      set r = ( partdiff (f,z,2));

      assume that

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

       A2: f is_partial_differentiable_in (z,2);

      consider x1,y1 be Real such that

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

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

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

      then

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

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

      consider L, R such that

       A6: r = (L . 1) and

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

      consider r1 such that

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



       A9: r = (r1 * 1) by A6, A8;

      consider x2, y2 such that

       A10: z = <*x2, y2*> and

       A11: ( SVF1 (2,f,z)) is_differentiable_in y2 by A2, Th6;

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

       A12: ex L, R st ( diff (( SVF1 (2,f,z)),y2)) = (L . 1) & for y st y in N1 holds ((( SVF1 (2,f,z)) . y) - (( SVF1 (2,f,z)) . y2)) = ((L . (y - y2)) + (R . (y - y2))) by A11, FDIFF_1:def 5;

      consider L1, R1 such that

       A13: ( diff (( SVF1 (2,f,z)),y2)) = (L1 . 1) and

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

      consider p1 such that

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



       A16: y0 = y2 by A1, A10, FINSEQ_1: 77;

      then

      consider N0 be Neighbourhood of y0 such that

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

      consider g be Real such that

       A18: 0 < g and

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

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

      consider s1 such that

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

      now

        let n be Nat;

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

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

      end;

      then

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

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

      then

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



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

      proof

        let n;

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

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

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

        then

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

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

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

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

        hence thesis by A17, A19, A20;

      end;



       A24: ( diff (( SVF1 (2,f,z)),y2)) = (p1 * 1) by A13, A15;

       A25:

      now

        let y;

        assume that

         A26: y in N and

         A27: y in N1;

        ((( SVF1 (2,f,z)) . y) - (( SVF1 (2,f,z)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A7, A26;

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

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

        hence ((r * (y - y0)) + (R . (y - y0))) = ((( diff (( SVF1 (2,f,z)),y2)) * (y - y0)) + (R1 . (y - y0))) by A15, A9, A24;

      end;

      reconsider rd = (r - ( diff (( SVF1 (2,f,z)),y2))) as Element of REAL by XREAL_0:def 1;

      now

        R1 is total by FDIFF_1:def 2;

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

        then

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

        let n be Nat;

        R is total by FDIFF_1:def 2;

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

        then

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



         A30: n in NAT by ORDINAL1:def 12;

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

        then ((r * (h . n)) + (R . (h . n))) = ((( diff (( SVF1 (2,f,z)),y2)) * (h . n)) + (R1 . (h . n))) by A25;

        then

         A31: (((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n))) = (((( diff (( SVF1 (2,f,z)),y2)) * (h . n)) + (R1 . (h . n))) / (h . n)) by XCMPLX_1: 62;



         A32: ((R . (h . n)) / (h . n)) = ((R . (h . n)) * ((h . n) " )) by XCMPLX_0:def 9

        .= ((R . (h . n)) * ((h " ) . n)) by VALUED_1: 10

        .= (((R /* h) . n) * ((h " ) . n)) by A30, A29, FUNCT_2: 108

        .= (((h " ) (#) (R /* h)) . n) by SEQ_1: 8;



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



         A34: ((R1 . (h . n)) / (h . n)) = ((R1 . (h . n)) * ((h . n) " )) by XCMPLX_0:def 9

        .= ((R1 . (h . n)) * ((h " ) . n)) by VALUED_1: 10

        .= (((R1 /* h) . n) * ((h " ) . n)) by A30, A28, FUNCT_2: 108

        .= (((h " ) (#) (R1 /* h)) . n) by SEQ_1: 8;



         A35: ((( diff (( SVF1 (2,f,z)),y2)) * (h . n)) / (h . n)) = (( diff (( SVF1 (2,f,z)),y2)) * ((h . n) / (h . n))) by XCMPLX_1: 74

        .= (( diff (( SVF1 (2,f,z)),y2)) * 1) by A33, XCMPLX_1: 60

        .= ( diff (( SVF1 (2,f,z)),y2));

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

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

        .= r;

        then (r + ((R . (h . n)) / (h . n))) = (( diff (( SVF1 (2,f,z)),y2)) + ((R1 . (h . n)) / (h . n))) by A31, A35, XCMPLX_1: 62;

        then r = (( diff (( SVF1 (2,f,z)),y2)) + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by A32, A34;

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

      end;

      then (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) is constant & ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1) = (r - ( diff (( SVF1 (2,f,z)),y2))) by VALUED_0:def 18;

      then

       A36: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - ( diff (( SVF1 (2,f,z)),y2))) by SEQ_4: 25;



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

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

      then (r - ( diff (( SVF1 (2,f,z)),y2))) = ( 0 - 0 ) by A36, A37, SEQ_2: 12;

      hence thesis by A1, A10, FINSEQ_1: 77;

    end;

    definition

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

      let Z be set;

      :: PDIFF_2:def2

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

      :: PDIFF_2:def3

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

    end

    theorem :: PDIFF_2:15

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

    proof

      set g = (f | Z);

      assume

       A1: f is_partial_differentiable`1_on Z;

      hence Z c= ( dom f);

      let z0 be Element of ( REAL 2);

      assume z0 in Z;

      then g is_partial_differentiable_in (z0,1) by A1;

      then

      consider x0,y0 be Real such that

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

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

      consider N be Neighbourhood of x0 such that

       A4: N c= ( dom ( SVF1 (1,g,z0))) and

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

      consider L, R such that

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



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

      proof

        let x;



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

        proof

          let x;

          assume

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

          then

           A10: x in ( dom ( reproj (1,z0))) by FUNCT_1: 11;



           A11: (( reproj (1,z0)) . x) in ( dom (f | Z)) by A9, FUNCT_1: 11;

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

          .= (f . (( reproj (1,z0)) . x)) by A11, FUNCT_1: 47

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

          hence thesis;

        end;



         A12: x0 in N by RCOMP_1: 16;

        assume

         A13: x in N;



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

        .= ((( SVF1 (1,f,z0)) . x) - (( SVF1 (1,g,z0)) . x0)) by A4, A13, A8

        .= ((( SVF1 (1,f,z0)) . x) - (( SVF1 (1,f,z0)) . x0)) by A4, A8, A12;

        hence thesis;

      end;

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

      proof

        let x;

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

        then

         A14: ( dom (f | Z)) c= ( dom f) by XBOOLE_1: 17;

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

        then x in ( dom ( reproj (1,z0))) & (( reproj (1,z0)) . x) in ( dom (f | Z)) by FUNCT_1: 11;

        hence thesis by A14, FUNCT_1: 11;

      end;

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

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

      then N c= ( dom ( SVF1 (1,f,z0))) by A4;

      hence thesis by A2, A7, Th9;

    end;

    theorem :: PDIFF_2:16

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

    proof

      set g = (f | Z);

      assume

       A1: f is_partial_differentiable`2_on Z;

      hence Z c= ( dom f);

      let z0 be Element of ( REAL 2);

      assume z0 in Z;

      then g is_partial_differentiable_in (z0,2) by A1;

      then

      consider x0,y0 be Real such that

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

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

      consider N be Neighbourhood of y0 such that

       A4: N c= ( dom ( SVF1 (2,g,z0))) and

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

      consider L, R such that

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



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

      proof

        let y;



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

        proof

          let y;

          assume

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

          then

           A10: y in ( dom ( reproj (2,z0))) by FUNCT_1: 11;



           A11: (( reproj (2,z0)) . y) in ( dom (f | Z)) by A9, FUNCT_1: 11;

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

          .= (f . (( reproj (2,z0)) . y)) by A11, FUNCT_1: 47

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

          hence thesis;

        end;



         A12: y0 in N by RCOMP_1: 16;

        assume

         A13: y in N;



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

        .= ((( SVF1 (2,f,z0)) . y) - (( SVF1 (2,g,z0)) . y0)) by A4, A13, A8

        .= ((( SVF1 (2,f,z0)) . y) - (( SVF1 (2,f,z0)) . y0)) by A4, A8, A12;

        hence thesis;

      end;

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

      proof

        let y;

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

        then

         A14: ( dom (f | Z)) c= ( dom f) by XBOOLE_1: 17;

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

        then y in ( dom ( reproj (2,z0))) & (( reproj (2,z0)) . y) in ( dom (f | Z)) by FUNCT_1: 11;

        hence thesis by A14, FUNCT_1: 11;

      end;

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

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

      then N c= ( dom ( SVF1 (2,f,z0))) by A4;

      hence thesis by A2, A7, Th10;

    end;

    definition

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

      let Z be set;

      assume

       A1: f is_partial_differentiable`1_on Z;

      :: PDIFF_2:def4

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

      existence

      proof

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

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

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

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

        take F;

        now

          Z c= ( dom f) by A1;

          then

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

          let y be object;

          assume y in Z;

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

        end;

        then

         A4: Z c= ( dom F);

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

        then ( dom F) c= Z;

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

        let z be Element of ( REAL 2);

        assume z in Z;

        then z in ( dom F) by A2;

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

        hence thesis;

      end;

      uniqueness

      proof

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

        assume that

         A5: ( dom F) = Z and

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

         A7: ( dom G) = Z and

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

        now

          let z be Element of ( REAL 2);

          assume

           A9: z in ( dom F);

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

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

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

    definition

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

      let Z be set;

      assume

       A1: f is_partial_differentiable`2_on Z;

      :: PDIFF_2:def5

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

      existence

      proof

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

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

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

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

        take F;

        now

          Z c= ( dom f) by A1;

          then

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

          let y be object;

          assume y in Z;

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

        end;

        then

         A4: Z c= ( dom F);

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

        then ( dom F) c= Z;

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

        let z be Element of ( REAL 2);

        assume z in Z;

        then z in ( dom F) by A2;

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

        hence thesis;

      end;

      uniqueness

      proof

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

        assume that

         A5: ( dom F) = Z and

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

         A7: ( dom G) = Z and

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

        now

          let z be Element of ( REAL 2);

          assume

           A9: z in ( dom F);

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

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

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

    begin

    theorem :: PDIFF_2:17

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

    proof

      let z0 be Element of ( REAL 2);

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

      assume that

       A1: f is_partial_differentiable_in (z0,1) and

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

      consider x0,y0 be Real such that

       A3: z0 = <*x0, y0*> and

       A4: ex N1 be Neighbourhood of x0 st N1 c= ( dom ( SVF1 (1,f,z0))) & ex L, R st for x st x in N1 holds ((( SVF1 (1,f,z0)) . x) - (( SVF1 (1,f,z0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A1, Th9;

      consider N1 be Neighbourhood of x0 such that N1 c= ( dom ( SVF1 (1,f,z0))) and

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



       A6: (( proj (1,2)) . z0) = x0 by A3, Th1;

      then

      consider N2 be Neighbourhood of x0 such that

       A7: N2 c= N and

       A8: N2 c= N1 by RCOMP_1: 17;



       A9: N2 c= ( dom ( SVF1 (1,f,z0))) by A2, A7;

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

       A10: ( rng c) = {(( proj (1,2)) . z0)} and

       A11: ( rng (h + c)) c= N;

      consider g be Real such that

       A12: 0 < g and

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

      (x0 + 0 ) < (x0 + g) & (x0 - g) < (x0 - 0 ) by A12, XREAL_1: 8, XREAL_1: 44;

      then

       A14: x0 in N2 by A13;



       A15: ( rng c) c= ( dom ( SVF1 (1,f,z0)))

      proof

        let y be object;

        assume y in ( rng c);

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

        then y in N by A7, A14;

        hence thesis by A2;

      end;

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

      proof

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

        then

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

        ( lim h) = 0 ;



        then ( lim (h + c)) = ( 0 + x0) by A16, SEQ_2: 6

        .= x0;

        then

        consider n be Nat such that

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

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

        take n;



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

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

        let y be object;

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

        then

        consider m such that

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

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

        then

         A20: |.(((h + c) . (n + m)) - x0).| < g by A17;

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

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

        then

         A21: (((h + c) ^\ n) . m) < (x0 + g) by XREAL_1: 19;

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

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

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

        hence thesis by A13, A19, A21;

      end;

      then

      consider n such that ( rng (c ^\ n)) c= N2 and

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

      consider L, R such that

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



       A24: ( rng (c ^\ n)) c= ( dom ( SVF1 (1,f,z0)))

      proof

        let y be object;

        assume

         A25: y in ( rng (c ^\ n));

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

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

        then y in N by A7, A14;

        hence thesis by A2;

      end;



       A26: L is total by FDIFF_1:def 3;



       A27: (((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 such that

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

         A29:

        now



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

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

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

          take n1 = m;

          let k be Nat such that

           A32: n1 <= k;

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

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

          hence |.((s1 . k) - (L . 1)).| < r by A31, A32;

        end;

        consider s such that

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



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

        .= s;

        now

          let m;



           A35: ((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 A26, FUNCT_2: 115

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

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

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

          .= (s1 . m) by A28, A34;

        end;

        then

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

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

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

      end;



       A37: ( rng ((h + c) ^\ n)) c= ( dom ( SVF1 (1,f,z0))) by A22, A7, A2;



       A38: ( rng (h + c)) c= ( dom ( SVF1 (1,f,z0))) by A11, A2;



       A39: for k holds ((( SVF1 (1,f,z0)) . (((h + c) ^\ n) . k)) - (( SVF1 (1,f,z0)) . ((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

         A40: (((h + c) ^\ n) . k) in N2 by A22;

        ((c ^\ n) . k) in ( rng (c ^\ n)) & ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26, VALUED_0: 28;

        then

         A41: ((c ^\ n) . k) = x0 by A10, A6, TARSKI:def 1;

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

        hence thesis by A23, A8, A40, A41;

      end;



       A42: R is total by FDIFF_1:def 2;

      now

        let k;



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

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

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

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

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

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

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

      end;

      then ((( SVF1 (1,f,z0)) /* ((h + c) ^\ n)) - (( SVF1 (1,f,z0)) /* (c ^\ n))) = ((L /* (h ^\ n)) + (R /* (h ^\ n))) by FUNCT_2: 63;



      then

       A43: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = ((((( SVF1 (1,f,z0)) /* (h + c)) ^\ n) - (( SVF1 (1,f,z0)) /* (c ^\ n))) (#) ((h ^\ n) " )) by A38, VALUED_0: 27

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

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

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

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

      then

       A44: (L . 1) = ( lim ((h " ) (#) ((( SVF1 (1,f,z0)) /* (h + c)) - (( SVF1 (1,f,z0)) /* c)))) by A27, SEQ_4: 22;

      thus ((h " ) (#) ((( SVF1 (1,f,z0)) /* (h + c)) - (( SVF1 (1,f,z0)) /* c))) is convergent by A27, A43, SEQ_4: 21;

      for x st x in N2 holds ((( SVF1 (1,f,z0)) . x) - (( SVF1 (1,f,z0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A23, A8;

      hence thesis by A1, A3, A9, A44, Th11;

    end;

    theorem :: PDIFF_2:18

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

    proof

      let z0 be Element of ( REAL 2);

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

      assume that

       A1: f is_partial_differentiable_in (z0,2) and

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

      consider x0,y0 be Real such that

       A3: z0 = <*x0, y0*> and

       A4: ex N1 be Neighbourhood of y0 st N1 c= ( dom ( SVF1 (2,f,z0))) & ex L, R st for y st y in N1 holds ((( SVF1 (2,f,z0)) . y) - (( SVF1 (2,f,z0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1, Th10;

      consider N1 be Neighbourhood of y0 such that N1 c= ( dom ( SVF1 (2,f,z0))) and

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



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

      then

      consider N2 be Neighbourhood of y0 such that

       A7: N2 c= N and

       A8: N2 c= N1 by RCOMP_1: 17;



       A9: N2 c= ( dom ( SVF1 (2,f,z0))) by A2, A7;

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

       A10: ( rng c) = {(( proj (2,2)) . z0)} and

       A11: ( rng (h + c)) c= N;

      consider g be Real such that

       A12: 0 < g and

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

      (y0 + 0 ) < (y0 + g) & (y0 - g) < (y0 - 0 ) by A12, XREAL_1: 8, XREAL_1: 44;

      then

       A14: y0 in N2 by A13;



       A15: ( rng c) c= ( dom ( SVF1 (2,f,z0)))

      proof

        let y be object;

        assume y in ( rng c);

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

        then y in N by A7, A14;

        hence thesis by A2;

      end;

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

      proof

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

        then

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

        ( lim h) = 0 ;



        then ( lim (h + c)) = ( 0 + y0) by A16, SEQ_2: 6

        .= y0;

        then

        consider n be Nat such that

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

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

        take n;



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

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

        let y be object;

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

        then

        consider m such that

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

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

        then

         A20: |.(((h + c) . (n + m)) - y0).| < g by A17;

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

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

        then

         A21: (((h + c) ^\ n) . m) < (y0 + g) by XREAL_1: 19;

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

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

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

        hence thesis by A13, A19, A21;

      end;

      then

      consider n such that ( rng (c ^\ n)) c= N2 and

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

      consider L, R such that

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



       A24: ( rng (c ^\ n)) c= ( dom ( SVF1 (2,f,z0)))

      proof

        let y be object;

        assume

         A25: y in ( rng (c ^\ n));

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

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

        then y in N by A7, A14;

        hence thesis by A2;

      end;



       A26: L is total by FDIFF_1:def 3;



       A27: (((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 such that

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

         A29:

        now



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

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

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

          take n1 = m;

          let k be Nat such that

           A32: n1 <= k;

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

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

          hence |.((s1 . k) - (L . 1)).| < r by A31, A32;

        end;

        consider s such that

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



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

        .= s;

        now

          let m;



           A35: ((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 A26, FUNCT_2: 115

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

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

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

          .= (s1 . m) by A28, A34;

        end;

        then

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

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

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

      end;



       A37: ( rng ((h + c) ^\ n)) c= ( dom ( SVF1 (2,f,z0))) by A22, A7, A2;



       A38: ( rng (h + c)) c= ( dom ( SVF1 (2,f,z0))) by A11, A2;



       A39: for k holds ((( SVF1 (2,f,z0)) . (((h + c) ^\ n) . k)) - (( SVF1 (2,f,z0)) . ((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

         A40: (((h + c) ^\ n) . k) in N2 by A22;

        ((c ^\ n) . k) in ( rng (c ^\ n)) & ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26, VALUED_0: 28;

        then

         A41: ((c ^\ n) . k) = y0 by A10, A6, TARSKI:def 1;

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

        hence thesis by A23, A8, A40, A41;

      end;



       A42: R is total by FDIFF_1:def 2;

      now

        let k;



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

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

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

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

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

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

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

      end;

      then ((( SVF1 (2,f,z0)) /* ((h + c) ^\ n)) - (( SVF1 (2,f,z0)) /* (c ^\ n))) = ((L /* (h ^\ n)) + (R /* (h ^\ n))) by FUNCT_2: 63;



      then

       A43: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = ((((( SVF1 (2,f,z0)) /* (h + c)) ^\ n) - (( SVF1 (2,f,z0)) /* (c ^\ n))) (#) ((h ^\ n) " )) by A38, VALUED_0: 27

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

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

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

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

      then

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

      thus ((h " ) (#) ((( SVF1 (2,f,z0)) /* (h + c)) - (( SVF1 (2,f,z0)) /* c))) is convergent by A27, A43, SEQ_4: 21;

      for y st y in N2 holds ((( SVF1 (2,f,z0)) . y) - (( SVF1 (2,f,z0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A23, A8;

      hence thesis by A1, A3, A9, A44, Th12;

    end;

    theorem :: PDIFF_2:19

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

    proof

      assume that

       A1: f1 is_partial_differentiable_in (z0,1) and

       A2: f2 is_partial_differentiable_in (z0,1);

      consider x0,y0 be Real such that

       A3: z0 = <*x0, y0*> and

       A4: ex N be Neighbourhood of x0 st N c= ( dom ( SVF1 (1,f1,z0))) & ex L, R st for x st x in N holds ((( SVF1 (1,f1,z0)) . x) - (( SVF1 (1,f1,z0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A1, Th9;

      reconsider x0, y0 as Element of REAL by XREAL_0:def 1;

      consider N1 be Neighbourhood of x0 such that

       A5: N1 c= ( dom ( SVF1 (1,f1,z0))) and

       A6: ex L, R st for x st x in N1 holds ((( SVF1 (1,f1,z0)) . x) - (( SVF1 (1,f1,z0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A4;

      consider L1, R1 such that

       A7: for x st x in N1 holds ((( SVF1 (1,f1,z0)) . x) - (( SVF1 (1,f1,z0)) . x0)) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A6;

      consider x1,y1 be Real such that

       A8: z0 = <*x1, y1*> and

       A9: ex N be Neighbourhood of x1 st N c= ( dom ( SVF1 (1,f2,z0))) & ex L, R st for x st x in N holds ((( SVF1 (1,f2,z0)) . x) - (( SVF1 (1,f2,z0)) . x1)) = ((L . (x - x1)) + (R . (x - x1))) by A2, Th9;

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

      then

      consider N2 be Neighbourhood of x0 such that

       A10: N2 c= ( dom ( SVF1 (1,f2,z0))) and

       A11: ex L, R st for x st x in N2 holds ((( SVF1 (1,f2,z0)) . x) - (( SVF1 (1,f2,z0)) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A9;

      consider L2, R2 such that

       A12: for x st x in N2 holds ((( SVF1 (1,f2,z0)) . x) - (( SVF1 (1,f2,z0)) . x0)) = ((L2 . (x - x0)) + (R2 . (x - x0))) by A11;

      consider N be Neighbourhood of x0 such that

       A13: N c= N1 and

       A14: N c= N2 by RCOMP_1: 17;



       A15: N c= ( dom ( SVF1 (1,f2,z0))) by A10, A14;



       A16: N c= ( dom ( SVF1 (1,f1,z0))) by A5, A13;



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

      proof

        let y;

        assume

         A18: y in N;

        then (( reproj (1,z0)) . y) in ( dom f1) & (( reproj (1,z0)) . y) in ( dom f2) by A16, A15, FUNCT_1: 11;

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

        then

         A19: (( reproj (1,z0)) . y) in ( dom (f1 (#) f2)) by VALUED_1:def 4;

        y in ( dom ( reproj (1,z0))) by A15, A18, FUNCT_1: 11;

        hence thesis by A19, FUNCT_1: 11;

      end;

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

      then

       A20: N c= ( dom ( SVF1 (1,(f1 (#) f2),z0)));

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



       A21: L2 is total by FDIFF_1:def 3;

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



       A22: L1 is total by FDIFF_1:def 3;



       A23: R1 is total by FDIFF_1:def 2;

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

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

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

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

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



       A24: R14 is total by FDIFF_1:def 2;



       A25: R18 is total by FDIFF_1:def 2;



       A26: R2 is total by FDIFF_1:def 2;

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

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

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

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

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



       A27: R16 is total by FDIFF_1:def 2;



       A28: L11 is total & L12 is total by FDIFF_1:def 3;

      now



         A29: x0 in ( dom ((f1 (#) f2) * ( reproj (1,z0)))) by A17, RCOMP_1: 16;

        then

         A30: x0 in ( dom ( reproj (1,z0))) by FUNCT_1: 11;

        (( reproj (1,z0)) . x0) in ( dom (f1 (#) f2)) by A29, FUNCT_1: 11;

        then

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

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

        then

         A32: x0 in ( dom (f1 * ( reproj (1,z0)))) by A30, FUNCT_1: 11;

        (( reproj (1,z0)) . x0) in ( dom f2) by A31, XBOOLE_0:def 4;

        then

         A33: x0 in ( dom (f2 * ( reproj (1,z0)))) by A30, FUNCT_1: 11;

        let x;



         A34: x0 in N by RCOMP_1: 16;

        assume

         A35: x in N;

        then

         A36: (((( SVF1 (1,f1,z0)) . x) - (( SVF1 (1,f1,z0)) . x0)) + (( SVF1 (1,f1,z0)) . x0)) = (((L1 . (x - x0)) + (R1 . (x - x0))) + (( SVF1 (1,f1,z0)) . x0)) by A7, A13;



         A37: x in ( dom ((f1 (#) f2) * ( reproj (1,z0)))) by A17, A35;

        then

         A38: x in ( dom ( reproj (1,z0))) by FUNCT_1: 11;

        (( reproj (1,z0)) . x) in ( dom (f1 (#) f2)) by A37, FUNCT_1: 11;

        then

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

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

        then

         A40: x in ( dom (f1 * ( reproj (1,z0)))) by A38, FUNCT_1: 11;

        reconsider xx0 = (x - x0) as Element of REAL by XREAL_0:def 1;

        (( reproj (1,z0)) . x) in ( dom f2) by A39, XBOOLE_0:def 4;

        then

         A41: x in ( dom (f2 * ( reproj (1,z0)))) by A38, FUNCT_1: 11;



        thus ((( SVF1 (1,(f1 (#) f2),z0)) . x) - (( SVF1 (1,(f1 (#) f2),z0)) . x0)) = (((f1 (#) f2) . (( reproj (1,z0)) . x)) - (( SVF1 (1,(f1 (#) f2),z0)) . x0)) by A20, A35, FUNCT_1: 12

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

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

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

        .= (((( SVF1 (1,f1,z0)) . x) * (( SVF1 (1,f2,z0)) . x)) - ((f1 (#) f2) . (( reproj (1,z0)) . x0))) by A20, A34, FUNCT_1: 12

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

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

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

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

        .= (((( SVF1 (1,f1,z0)) . x) * ((( SVF1 (1,f2,z0)) . x) - (( SVF1 (1,f2,z0)) . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * (( SVF1 (1,f2,z0)) . x0))) by A7, A13, A35

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

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

        .= (((((L1 . (x - x0)) + (R1 . xx0)) + (( SVF1 (1,f1,z0)) . x0)) * ((( SVF1 (1,f2,z0)) . x) - (( SVF1 (1,f2,z0)) . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0)))) by A23, A36, RFUNCT_1: 57

        .= (((((L1 . (x - x0)) + (R1 . (x - x0))) + (( SVF1 (1,f1,z0)) . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))) by A12, A14, A35

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

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

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

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

        .= ((((L1 . (x - x0)) + (R1 . xx0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + (R13 . (x - x0))))) by A23, A26, 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 . (x - x0)) * (L2 . (x - x0))) + ((L1 . xx0) * (R2 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A28, RFUNCT_1: 56

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

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

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

        .= ((((R14 . (x - x0)) + (R18 . xx0)) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A23, A26, RFUNCT_1: 56

        .= ((((R14 . (x - x0)) + (R18 . xx0)) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A23, A26, A27, RFUNCT_1: 56

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

        .= (((L . (x - x0)) + (R13 . xx0)) + ((R14 . (x - x0)) + (R20 . (x - x0)))) by A23, A26, A27, A25, RFUNCT_1: 56

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

        .= ((L . (x - x0)) + ((R15 . xx0) + (R20 . (x - x0)))) by A23, A26, A24, RFUNCT_1: 56

        .= ((L . (x - x0)) + (R . (x - x0))) by A23, A26, A24, A27, A25, RFUNCT_1: 56;

      end;

      hence thesis by A3, A20, Th9;

    end;

    theorem :: PDIFF_2:20

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

    proof

      assume that

       A1: f1 is_partial_differentiable_in (z0,2) and

       A2: f2 is_partial_differentiable_in (z0,2);

      consider x0,y0 be Real such that

       A3: z0 = <*x0, y0*> and

       A4: ex N be Neighbourhood of y0 st N c= ( dom ( SVF1 (2,f1,z0))) & ex L, R st for y st y in N holds ((( SVF1 (2,f1,z0)) . y) - (( SVF1 (2,f1,z0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A1, Th10;

      reconsider x0, y0 as Real;

      consider N1 be Neighbourhood of y0 such that

       A5: N1 c= ( dom ( SVF1 (2,f1,z0))) and

       A6: ex L, R st for y st y in N1 holds ((( SVF1 (2,f1,z0)) . y) - (( SVF1 (2,f1,z0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A4;

      consider L1, R1 such that

       A7: for y st y in N1 holds ((( SVF1 (2,f1,z0)) . y) - (( SVF1 (2,f1,z0)) . y0)) = ((L1 . (y - y0)) + (R1 . (y - y0))) by A6;

      consider x1,y1 be Real such that

       A8: z0 = <*x1, y1*> and

       A9: ex N be Neighbourhood of y1 st N c= ( dom ( SVF1 (2,f2,z0))) & ex L, R st for y st y in N holds ((( SVF1 (2,f2,z0)) . y) - (( SVF1 (2,f2,z0)) . y1)) = ((L . (y - y1)) + (R . (y - y1))) by A2, Th10;

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

      then

      consider N2 be Neighbourhood of y0 such that

       A10: N2 c= ( dom ( SVF1 (2,f2,z0))) and

       A11: ex L, R st for y st y in N2 holds ((( SVF1 (2,f2,z0)) . y) - (( SVF1 (2,f2,z0)) . y0)) = ((L . (y - y0)) + (R . (y - y0))) by A9;

      consider L2, R2 such that

       A12: for y st y in N2 holds ((( SVF1 (2,f2,z0)) . y) - (( SVF1 (2,f2,z0)) . y0)) = ((L2 . (y - y0)) + (R2 . (y - y0))) by A11;

      consider N be Neighbourhood of y0 such that

       A13: N c= N1 and

       A14: N c= N2 by RCOMP_1: 17;



       A15: N c= ( dom ( SVF1 (2,f2,z0))) by A10, A14;



       A16: N c= ( dom ( SVF1 (2,f1,z0))) by A5, A13;



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

      proof

        let y;

        assume

         A18: y in N;

        then (( reproj (2,z0)) . y) in ( dom f1) & (( reproj (2,z0)) . y) in ( dom f2) by A16, A15, FUNCT_1: 11;

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

        then

         A19: (( reproj (2,z0)) . y) in ( dom (f1 (#) f2)) by VALUED_1:def 4;

        y in ( dom ( reproj (2,z0))) by A15, A18, FUNCT_1: 11;

        hence thesis by A19, FUNCT_1: 11;

      end;

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

      then

       A20: N c= ( dom ( SVF1 (2,(f1 (#) f2),z0)));

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



       A21: L2 is total by FDIFF_1:def 3;

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



       A22: L1 is total by FDIFF_1:def 3;

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



       A23: R1 is total by FDIFF_1:def 2;

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

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

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

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

      reconsider R15 = (R13 + R14), 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;



       A24: R14 is total by FDIFF_1:def 2;



       A25: R16 is total by FDIFF_1:def 2;



       A26: R18 is total by FDIFF_1:def 2;



       A27: R2 is total by FDIFF_1:def 2;



       A28: L11 is total & L12 is total by FDIFF_1:def 3;

      now



         A29: y0 in ( dom ((f1 (#) f2) * ( reproj (2,z0)))) by A17, RCOMP_1: 16;

        then

         A30: y0 in ( dom ( reproj (2,z0))) by FUNCT_1: 11;

        (( reproj (2,z0)) . y0) in ( dom (f1 (#) f2)) by A29, FUNCT_1: 11;

        then

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

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

        then

         A32: y0 in ( dom (f1 * ( reproj (2,z0)))) by A30, FUNCT_1: 11;

        (( reproj (2,z0)) . y0) in ( dom f2) by A31, XBOOLE_0:def 4;

        then

         A33: y0 in ( dom (f2 * ( reproj (2,z0)))) by A30, FUNCT_1: 11;

        let y;



         A34: y0 in N by RCOMP_1: 16;

        reconsider yy0 = (y - y0) as Element of REAL by XREAL_0:def 1;

        assume

         A35: y in N;

        then

         A36: (((( SVF1 (2,f1,z0)) . y) - (( SVF1 (2,f1,z0)) . y0)) + (( SVF1 (2,f1,z0)) . y0)) = (((L1 . (y - y0)) + (R1 . (y - y0))) + (( SVF1 (2,f1,z0)) . y0)) by A7, A13;



         A37: y in ( dom ((f1 (#) f2) * ( reproj (2,z0)))) by A17, A35;

        then

         A38: y in ( dom ( reproj (2,z0))) by FUNCT_1: 11;

        (( reproj (2,z0)) . y) in ( dom (f1 (#) f2)) by A37, FUNCT_1: 11;

        then

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

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

        then

         A40: y in ( dom (f1 * ( reproj (2,z0)))) by A38, FUNCT_1: 11;

        (( reproj (2,z0)) . y) in ( dom f2) by A39, XBOOLE_0:def 4;

        then

         A41: y in ( dom (f2 * ( reproj (2,z0)))) by A38, FUNCT_1: 11;



        thus ((( SVF1 (2,(f1 (#) f2),z0)) . y) - (( SVF1 (2,(f1 (#) f2),z0)) . y0)) = (((f1 (#) f2) . (( reproj (2,z0)) . y)) - (( SVF1 (2,(f1 (#) f2),z0)) . y0)) by A20, A35, FUNCT_1: 12

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

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

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

        .= (((( SVF1 (2,f1,z0)) . y) * (( SVF1 (2,f2,z0)) . y)) - ((f1 (#) f2) . (( reproj (2,z0)) . y0))) by A20, A34, FUNCT_1: 12

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

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

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

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

        .= (((( SVF1 (2,f1,z0)) . y) * ((( SVF1 (2,f2,z0)) . y) - (( SVF1 (2,f2,z0)) . y0))) + (((L1 . (y - y0)) + (R1 . (y - y0))) * (( SVF1 (2,f2,z0)) . y0))) by A7, A13, A35

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

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

        .= (((((L1 . (y - y0)) + (R1 . (y - y0))) + (( SVF1 (2,f1,z0)) . y0)) * ((( SVF1 (2,f2,z0)) . y) - (( SVF1 (2,f2,z0)) . y0))) + ((L11 . (y - y0)) + (R11 . yy0))) by A23, A36, RFUNCT_1: 57

        .= (((((L1 . (y - y0)) + (R1 . (y - y0))) + (( SVF1 (2,f1,z0)) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0)))) by A12, A14, A35

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

        .= (((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((( SVF1 (2,f1,z0)) . y0) * (R2 . (y - y0))))) + ((L11 . yy0) + (R11 . (y - y0)))) by A21, 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 . yy0))) by A27, 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 . yy0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((L11 . (y - y0)) + (R13 . (y - y0))))) by A23, A27, 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 - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . yy0))) by A28, RFUNCT_1: 56

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

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

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

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

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

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

        .= (((L . yy0) + (R13 . (y - y0))) + ((R14 . (y - y0)) + (R20 . (y - y0)))) by A23, A27, A25, A26, RFUNCT_1: 56

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

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

        .= ((L . (y - y0)) + (R . (y - y0))) by A23, A27, A24, A25, A26, RFUNCT_1: 56;

      end;

      hence thesis by A3, A20, Th10;

    end;

    theorem :: PDIFF_2:21

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

    theorem :: PDIFF_2:22

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