pdiff_1.miz



    begin

    definition

      let i,n be Nat;

      :: PDIFF_1:def1

      func proj (i,n) -> Function of ( REAL n), REAL means

      : Def1: for x be Element of ( REAL n) holds (it . x) = (x . i);

      existence

      proof

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

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

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

        take f;

        let x be Element of ( REAL n);

        (f . x) = F(x) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of ( REAL n), REAL ;

        assume that

         A2: for x be Element of ( REAL n) holds (f . x) = (x . i) and

         A3: for x be Element of ( REAL n) holds (g . x) = (x . i);

        now

          let x be Element of ( REAL n);

          (f . x) = (x . i) by A2;

          hence (f . x) = (g . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    set W = (( proj (1,1)) qua Function " );

    

     Lm1: ( proj (1,1)) is bijective & ( dom ( proj (1,1))) = ( REAL 1) & ( rng ( proj (1,1))) = REAL & for x be Real holds (( proj (1,1)) . <*x*>) = x & ((( proj (1,1)) qua Function " ) . x) = <*x*>

    proof

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

      for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A1: x1 in ( dom f) and

         A2: x2 in ( dom f) and

         A3: (f . x1) = (f . x2);

        reconsider y1 = x1, y2 = x2 as Element of ( REAL 1) by A1, A2;

        x1 is Tuple of 1, REAL by A1, FINSEQ_2: 131;

        then

        consider d1 be Element of REAL such that

         A4: x1 = <*d1*> by FINSEQ_2: 97;

        d1 = ( <*d1*> . 1) by FINSEQ_1: 40;

        then d1 = (f . y1) by A4, Def1;

        then

         A5: d1 = (y2 . 1) by A3, Def1;

        x2 is Tuple of 1, REAL by A2, FINSEQ_2: 131;

        then ex d2 be Element of REAL st x2 = <*d2*> by FINSEQ_2: 97;

        hence thesis by A4, A5, FINSEQ_1: 40;

      end;

      then

       A6: f is one-to-one by FUNCT_1:def 4;

      

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

       A8:

      now

        let x be Real;

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

        

         A9: <*xx*> is Element of (1 -tuples_on REAL ) by FINSEQ_2: 98;

        then (( proj (1,1)) . <*x*>) = ( <*x*> . 1) by Def1;

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

        hence ((( proj (1,1)) qua Function " ) . x) = <*x*> by A7, A6, A9, FUNCT_1: 34;

      end;

      

       A10: for y be object st y in REAL holds ex x be object st x in ( REAL 1) & y = (f . x)

      proof

        let y be object;

        assume y in REAL ;

        then

        reconsider y1 = y as Element of REAL ;

        reconsider x = <*y1*> as Element of ( REAL 1) by FINSEQ_2: 98;

        (f . x) = (x . 1) by Def1;

        then (f . x) = y by FINSEQ_1: 40;

        hence thesis;

      end;

      then ( rng f) = REAL by FUNCT_2: 10;

      then f is onto by FUNCT_2:def 3;

      hence thesis by A6, A10, A8, FUNCT_2: 10, FUNCT_2:def 1;

    end;

    

     Lm2: for i,n be Nat st i in ( Seg n) holds ( proj (i,n)) is onto

    proof

      let i,n be Nat;

      set f = ( proj (i,n));

      assume

       A1: i in ( Seg n);

      for y be object st y in REAL holds ex x be object st x in ( REAL n) & y = (f . x)

      proof

        let y be object;

        assume y in REAL ;

        then

        reconsider y1 = y as Element of REAL ;

        reconsider x = (n |-> y1) as Element of ( REAL n);

        (f . x) = (x . i) by Def1;

        then (f . x) = y by A1, FINSEQ_2: 57;

        hence thesis;

      end;

      then ( rng f) = REAL by FUNCT_2: 10;

      hence thesis by FUNCT_2:def 3;

    end;

    theorem :: PDIFF_1:1

    (for i,n be Nat st i in ( Seg n) holds ( dom ( proj (i,n))) = ( REAL n) & ( rng ( proj (i,n))) = REAL ) & for x be Real holds (( proj (1,1)) . <*x*>) = x & ((( proj (1,1)) qua Function " ) . x) = <*x*>

    proof

      now

        let i,n be Nat;

        assume

         A1: i in ( Seg n);

        thus ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

        ( proj (i,n)) is onto by A1, Lm2;

        hence ( rng ( proj (i,n))) = REAL by FUNCT_2:def 3;

      end;

      hence thesis by Lm1;

    end;

    theorem :: PDIFF_1:2

    

     Th2: (( proj (1,1)) qua Function " ) is Function of REAL , ( REAL 1) & (( proj (1,1)) qua Function " ) is one-to-one & ( dom (( proj (1,1)) qua Function " )) = REAL & ( rng (( proj (1,1)) qua Function " )) = ( REAL 1) & ex g be Function of REAL , ( REAL 1) st g is bijective & (( proj (1,1)) qua Function " ) = g

    proof

      

       A1: ( REAL 1) = ( rng W) by Lm1, FUNCT_1: 33;

       REAL = ( dom W) by Lm1, FUNCT_1: 33;

      then

      reconsider g = W as Function of REAL , ( REAL 1) by A1, FUNCT_2: 1;

      g is onto by A1, FUNCT_2:def 3;

      hence thesis by Lm1, FUNCT_1: 33;

    end;

    registration

      cluster ( proj (1,1)) -> bijective;

      coherence by Lm1;

    end

    definition

      let g be PartFunc of REAL , REAL ;

      :: PDIFF_1:def2

      func <>* g -> PartFunc of ( REAL 1), ( REAL 1) equals (((( proj (1,1)) qua Function " ) * g) * ( proj (1,1)));

      coherence

      proof

        reconsider f = (( proj (1,1)) qua Function " ) as PartFunc of REAL , ( REAL 1) by PARTFUN1: 9;

        ((f * g) * ( proj (1,1))) is PartFunc of ( REAL 1), ( REAL 1);

        hence thesis;

      end;

    end

    definition

      let n be Nat;

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

      :: PDIFF_1:def3

      func <>* g -> PartFunc of ( REAL n), ( REAL 1) equals ((( proj (1,1)) qua Function " ) * g);

      correctness

      proof

        reconsider f = (( proj (1,1)) qua Function " ) as PartFunc of REAL , ( REAL 1) by PARTFUN1: 9;

        (f * g) is PartFunc of ( REAL n), ( REAL 1);

        hence thesis;

      end;

    end

    definition

      let i,n be Nat;

      :: PDIFF_1:def4

      func Proj (i,n) -> Function of ( REAL-NS n), ( REAL-NS 1) means

      : Def4: for x be Point of ( REAL-NS n) holds (it . x) = <*(( proj (i,n)) . x)*>;

      existence

      proof

        deffunc F( Point of ( REAL-NS n)) = <*(( proj (i,n)) . $1)*>;

        

         A1: for x be Point of ( REAL-NS n) holds F(x) is Element of ( REAL-NS 1)

        proof

          let x be Point of ( REAL-NS n);

          (( proj (i,n)) . x) in REAL by XREAL_0:def 1;

          then

           A2: F(x) is FinSequence of REAL by FINSEQ_1: 74;

          ( len F(x)) = 1 by FINSEQ_1: 39;

          then F(x) is Element of (1 -tuples_on REAL ) by A2, FINSEQ_2: 92;

          then F(x) in ( REAL 1);

          hence thesis by REAL_NS1:def 4;

        end;

        thus ex f be Function of ( REAL-NS n), ( REAL-NS 1) st for x be Point of ( REAL-NS n) holds (f . x) = F(x) from FUNCT_2:sch 9( A1);

      end;

      uniqueness

      proof

        let f,g be Function of ( REAL-NS n), ( REAL-NS 1);

        assume that

         A3: for x be Point of ( REAL-NS n) holds (f . x) = <*(( proj (i,n)) . x)*> and

         A4: for x be Point of ( REAL-NS n) holds (g . x) = <*(( proj (i,n)) . x)*>;

        now

          let x be Point of ( REAL-NS n);

          (f . x) = <*(( proj (i,n)) . x)*> by A3;

          hence (f . x) = (g . x) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let i be Nat;

      let x be FinSequence of REAL ;

      :: PDIFF_1:def5

      func reproj (i,x) -> Function means

      : Def5: ( dom it ) = REAL & for r be Element of REAL holds (it . r) = ( Replace (x,i,r));

      existence

      proof

        deffunc F( Element of REAL ) = ( Replace (x,i,$1));

        consider f be Function such that

         A1: ( dom f) = REAL & for r be Element of REAL st r in REAL holds (f . r) = F(r) from CLASSES1:sch 2;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be Function;

        assume that

         A2: ( dom f) = REAL and

         A3: for r be Element of REAL holds (f . r) = ( Replace (x,i,r)) and

         A4: ( dom g) = REAL and

         A5: for r be Element of REAL holds (g . r) = ( Replace (x,i,r));

        now

          let p be object;

          assume p in ( dom f);

          then

          reconsider r = p as Element of REAL by A2;

          (f . r) = ( Replace (x,i,r)) by A3;

          hence (f . p) = (g . p) by A5;

        end;

        hence thesis by A2, A4, FUNCT_1: 2;

      end;

    end

    definition

      let n,i be Nat;

      let x be Element of ( REAL n);

      :: original: reproj

      redefine

      func reproj (i,x) -> Function of REAL , ( REAL n) ;

      correctness

      proof

         A1:

        now

          let p be object;

          assume p in REAL ;

          then

          reconsider r = p as Element of REAL ;

          

           A2: (( reproj (i,x)) . r) = ( Replace (x,i,r)) by Def5;

          then

          reconsider IT = (( reproj (i,x)) . r) as FinSequence of REAL ;

          ( len IT) = ( len x) by A2, FINSEQ_7: 5

          .= n by CARD_1:def 7;

          then

          reconsider IT as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

          IT is Element of ( REAL n);

          hence (( reproj (i,x)) . p) in ( REAL n);

        end;

        ( dom ( reproj (i,x))) = REAL by Def5;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let n,i be Nat;

      let x be Point of ( REAL-NS n);

      :: PDIFF_1:def6

      func reproj (i,x) -> Function of ( REAL-NS 1), ( REAL-NS n) means

      : Def6: for r be Element of ( REAL-NS 1) holds ex q be Element of REAL , y be Element of ( REAL n) st r = <*q*> & y = x & (it . r) = (( reproj (i,y)) . q);

      existence

      proof

        defpred P[ Element of ( REAL-NS 1), Point of ( REAL-NS n)] means ex q be Element of REAL , z be Element of ( REAL n) st $1 = <*q*> & z = x & $2 = (( reproj (i,z)) . q);

        

         A1: for r be Element of ( REAL-NS 1) holds ex y be Element of ( REAL-NS n) st P[r, y]

        proof

          reconsider z = x as Element of ( REAL n) by REAL_NS1:def 4;

          let r be Element of ( REAL-NS 1);

          r is Element of ( REAL 1) by REAL_NS1:def 4;

          then

          consider q be Element of REAL such that

           A2: r = <*q*> by FINSEQ_2: 97;

          (( reproj (i,z)) . q) is Element of ( REAL-NS n) by REAL_NS1:def 4;

          hence thesis by A2;

        end;

        thus ex f be Function of ( REAL-NS 1), ( REAL-NS n) st for r be Element of ( REAL-NS 1) holds P[r, (f . r)] from FUNCT_2:sch 3( A1);

      end;

      uniqueness

      proof

        let f,g be Function of ( REAL-NS 1), ( REAL-NS n);

        assume that

         A3: for r be Element of ( REAL-NS 1) holds ex q be Element of REAL , y be Element of ( REAL n) st r = <*q*> & y = x & (f . r) = (( reproj (i,y)) . q) and

         A4: for r be Element of ( REAL-NS 1) holds ex q be Element of REAL , y be Element of ( REAL n) st r = <*q*> & y = x & (g . r) = (( reproj (i,y)) . q);

        now

          let r be Point of ( REAL-NS 1);

          consider p be Element of REAL , y be Element of ( REAL n) such that

           A5: r = <*p*> and

           A6: y = x and

           A7: (f . r) = (( reproj (i,y)) . p) by A3;

          

           A8: ex q be Element of REAL , z be Element of ( REAL n) st r = <*q*> & z = x & (g . r) = (( reproj (i,z)) . q) by A4;

          p = ( <*p*> . 1) by FINSEQ_1:def 8;

          hence (f . r) = (g . r) by A5, A6, A7, A8, FINSEQ_1:def 8;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let m,n be non zero Nat;

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

      let x be Element of ( REAL m);

      :: PDIFF_1:def7

      pred f is_differentiable_in x means ex g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st f = g & x = y & g is_differentiable_in y;

    end

    definition

      let m,n be non zero Nat;

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

      let x be Element of ( REAL m);

      assume

       A1: f is_differentiable_in x;

      :: PDIFF_1:def8

      func diff (f,x) -> Function of ( REAL m), ( REAL n) means

      : Def8: ex g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st f = g & x = y & it = ( diff (g,y));

      correctness

      proof

        

         A2: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

        consider g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) such that

         A3: f = g and

         A4: x = y and g is_differentiable_in y by A1;

        the carrier of ( REAL-NS m) = ( REAL m) by REAL_NS1:def 4;

        then ( diff (g,y)) is Function of ( REAL m), ( REAL n) by A2, LOPBAN_1:def 9;

        hence thesis by A3, A4;

      end;

    end

    theorem :: PDIFF_1:3

    

     Th3: for I be Function of REAL , ( REAL 1) st I = (( proj (1,1)) qua Function " ) holds (for x be VECTOR of ( REAL-NS 1), y be Real st x = (I . y) holds ||.x.|| = |.y.|) & (for x,y be VECTOR of ( REAL-NS 1), a,b be Real st x = (I . a) & y = (I . b) holds (x + y) = (I . (a + b))) & (for x be VECTOR of ( REAL-NS 1), y,a be Real st x = (I . y) holds (a * x) = (I . (a * y))) & (for x be VECTOR of ( REAL-NS 1), a be Real st x = (I . a) holds ( - x) = (I . ( - a))) & for x,y be VECTOR of ( REAL-NS 1), a,b be Real st x = (I . a) & y = (I . b) holds (x - y) = (I . (a - b))

    proof

      let I be Function of REAL , ( REAL 1);

      assume

       A1: I = (( proj (1,1)) qua Function " );

      hereby

        let x be VECTOR of ( REAL-NS 1), y be Real;

        reconsider xx = x as Element of ( REAL 1) by REAL_NS1:def 4;

        reconsider yy = y as Real;

        reconsider yy2 = (yy ^2 ) as Real;

        assume x = (I . y);

        then xx = <*y*> by A1, Lm1;

        then ( sqrt ( Sum ( sqr xx))) = ( sqrt ( Sum <*yy2*>)) by RVSUM_1: 55;

        then

         A2: ( sqrt ( Sum ( sqr xx))) = ( sqrt (y ^2 )) by RVSUM_1: 73;

         ||.x.|| = |.xx.| by REAL_NS1: 1;

        hence ||.x.|| = |.y.| by A2, COMPLEX1: 72;

      end;

       A3:

      now

        let x,y be VECTOR of ( REAL-NS 1), a,b be Real;

        reconsider xx = x, yy = y as Element of ( REAL 1) by REAL_NS1:def 4;

        reconsider aa = a, bb = b as Real;

        assume that

         A4: x = (I . a) and

         A5: y = (I . b);

        

         A6: <*b*> = yy by A1, A5, Lm1;

         <*a*> = xx by A1, A4, Lm1;

        then (x - y) = ( <*aa*> - <*bb*>) by A6, REAL_NS1: 5;

        then (x - y) = <*(a - b)*> by RVSUM_1: 29;

        hence (x - y) = (I . (a - b)) by A1, Lm1;

      end;

      hereby

        let x,y be VECTOR of ( REAL-NS 1), a,b be Real;

        reconsider xx = x, yy = y as Element of ( REAL 1) by REAL_NS1:def 4;

        reconsider aa = a, bb = b as Real;

        assume that

         A7: x = (I . a) and

         A8: y = (I . b);

        

         A9: <*b*> = yy by A1, A8, Lm1;

         <*a*> = xx by A1, A7, Lm1;

        then (x + y) = ( <*aa*> + <*bb*>) by A9, REAL_NS1: 2;

        then (x + y) = <*(a + b)*> by RVSUM_1: 13;

        hence (x + y) = (I . (a + b)) by A1, Lm1;

      end;

       A10:

      now

        let x be VECTOR of ( REAL-NS 1), y,a be Real;

        reconsider xx = x as Element of ( REAL 1) by REAL_NS1:def 4;

        assume x = (I . y);

        then

         A11: xx = <*y*> by A1, Lm1;

        (a * x) = (a * xx) by REAL_NS1: 3;

        then (a * x) = <*(a * y)*> by A11, RVSUM_1: 47;

        hence (a * x) = (I . (a * y)) by A1, Lm1;

      end;

      now

        let x be VECTOR of ( REAL-NS 1), a be Real;

        assume x = (I . a);

        then (( - 1) * x) = (I . (( - 1) * a)) by A10;

        hence ( - x) = (I . ( - a)) by RLVECT_1: 16;

      end;

      hence thesis by A10, A3;

    end;

    reconsider I = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL 1) by Th2;

    theorem :: PDIFF_1:4

    

     Th4: for J be Function of ( REAL 1), REAL st J = ( proj (1,1)) holds (for x be VECTOR of ( REAL-NS 1), y be Real st (J . x) = y holds ||.x.|| = |.y.|) & (for x,y be VECTOR of ( REAL-NS 1), a,b be Real st (J . x) = a & (J . y) = b holds (J . (x + y)) = (a + b)) & (for x be VECTOR of ( REAL-NS 1), y,a be Real st (J . x) = y holds (J . (a * x)) = (a * y)) & (for x be VECTOR of ( REAL-NS 1), a be Real st (J . x) = a holds (J . ( - x)) = ( - a)) & for x,y be VECTOR of ( REAL-NS 1), a,b be Real st (J . x) = a & (J . y) = b holds (J . (x - y)) = (a - b)

    proof

      let J be Function of ( REAL 1), REAL ;

      assume

       A1: J = ( proj (1,1));

      hereby

        let x be VECTOR of ( REAL-NS 1), y be Real;

        reconsider xx = x as Element of ( REAL 1) by REAL_NS1:def 4;

        assume (J . x) = y;

        then (I . (J . xx)) = (I . y);

        then x = (I . y) by A1, Lm1, FUNCT_1: 34;

        hence ||.x.|| = |.y.| by Th3;

      end;

      hereby

        let x,y be VECTOR of ( REAL-NS 1), a,b be Real;

        reconsider xx = x, yy = y as Element of ( REAL 1) by REAL_NS1:def 4;

        reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

        assume that

         A2: (J . x) = a and

         A3: (J . y) = b;

        (I . (J . yy)) = (I . b) by A3;

        then

         A4: y = (I . b) by A1, Lm1, FUNCT_1: 34;

        (I . (J . xx)) = (I . a) by A2;

        then x = (I . a) by A1, Lm1, FUNCT_1: 34;

        then (J . (x + y)) = (J . (I . (a + b))) by A4, Th3;

        then (J . (x + y)) = (J . (I . (aa + bb)));

        hence (J . (x + y)) = (a + b) by A1, Lm1, FUNCT_1: 35;

      end;

      hereby

        let x be VECTOR of ( REAL-NS 1), y,a be Real;

        reconsider xx = x as Element of ( REAL 1) by REAL_NS1:def 4;

        reconsider yy = y, aa = a as Element of REAL by XREAL_0:def 1;

        assume (J . x) = y;

        then (I . (J . xx)) = (I . y);

        then x = (I . y) by A1, Lm1, FUNCT_1: 34;

        then (J . (a * x)) = (J . (I . (a * y))) by Th3;

        then (J . (a * x)) = (aa * yy) by A1, Lm1, FUNCT_1: 35;

        hence (J . (a * x)) = (a * y);

      end;

      hereby

        let x be VECTOR of ( REAL-NS 1), y be Real;

        reconsider xx = x as Element of ( REAL 1) by REAL_NS1:def 4;

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

        assume (J . x) = y;

        then (I . y) = (I . (J . xx));

        then x = (I . y) by A1, Lm1, FUNCT_1: 34;

        then (J . ( - x)) = (J . (I . ( - y))) by Th3;

        then (J . ( - x)) = ( - yy) by A1, Lm1, FUNCT_1: 35;

        hence (J . ( - x)) = ( - y);

      end;

      let x,y be VECTOR of ( REAL-NS 1), a,b be Real;

      reconsider xx = x, yy = y as Element of ( REAL 1) by REAL_NS1:def 4;

      reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

      assume that

       A5: (J . x) = a and

       A6: (J . y) = b;

      (I . (J . yy)) = (I . b) by A6;

      then

       A7: y = (I . b) by A1, Lm1, FUNCT_1: 34;

      (I . (J . xx)) = (I . a) by A5;

      then x = (I . a) by A1, Lm1, FUNCT_1: 34;

      then (J . (x - y)) = (J . (I . (a - b))) by A7, Th3;

      then (J . (x - y)) = (aa - bb) by A1, Lm1, FUNCT_1: 35;

      hence thesis;

    end;

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    theorem :: PDIFF_1:5

    

     Th5: for I be Function of REAL , ( REAL 1), J be Function of ( REAL 1), REAL st I = (( proj (1,1)) qua Function " ) & J = ( proj (1,1)) holds (for R be RestFunc of ( REAL-NS 1), ( REAL-NS 1) holds ((J * R) * I) is RestFunc) & for L be LinearOperator of ( REAL-NS 1), ( REAL-NS 1) holds ((J * L) * I) is LinearFunc

    proof

      let I be Function of REAL , ( REAL 1), J be Function of ( REAL 1), REAL ;

      assume that

       A1: I = (( proj (1,1)) qua Function " ) and

       A2: J = ( proj (1,1));

      thus for R be RestFunc of ( REAL-NS 1), ( REAL-NS 1) holds ((J * R) * I) is RestFunc

      proof

        let R be RestFunc of ( REAL-NS 1), ( REAL-NS 1);

        

         A3: R is total by NDIFF_1:def 5;

        the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

        then

        reconsider R0 = R as Function of ( REAL 1), ( REAL 1) by A3;

        reconsider R1 = ((J * R) * I) as PartFunc of REAL , REAL ;

        

         A4: ((J * R0) * I) is Function of REAL , REAL ;

        then

         A5: ( dom R1) = REAL by FUNCT_2:def 1;

        

         A6: for r be Real st r > 0 holds ex d be Real st d > 0 & for z1 be Real st z1 <> 0 & |.z1.| < d holds (( |.z1.| " ) * |.(R1 . z1).|) < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider d be Real such that

           A7: d > 0 and

           A8: for z be Point of ( REAL-NS 1) st z <> ( 0. ( REAL-NS 1)) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r by A3, NDIFF_1: 23;

          take d;

          for z1 be Real st z1 <> 0 & |.z1.| < d holds (( |.z1.| " ) * |.(R1 . z1).|) < r

          proof

            let z1 be Real such that

             A9: z1 <> 0 and

             A10: |.z1.| < d;

            reconsider z1 as Element of REAL by XREAL_0:def 1;

            reconsider z = (I . z1) as Point of ( REAL-NS 1) by REAL_NS1:def 4;

             |.z1.| > 0 by A9, COMPLEX1: 47;

            then ||.z.|| <> 0 by A1, Th3;

            then

             A11: z <> ( 0. ( REAL-NS 1));

            (I * J) = ( id ( dom ( proj (1,1)))) by A1, A2, FUNCT_1: 39;

            then

             A12: (I * J) = ( id ( REAL 1)) by FUNCT_2:def 1;

            

             A13: ( dom (J * R0)) = ( REAL 1) by FUNCT_2:def 1;

            R is total by NDIFF_1:def 5;

            then

             A14: ( dom R) = the carrier of ( REAL-NS 1) by PARTFUN1:def 2;

            then (R /. z) = (R . z) by PARTFUN1:def 6;

            then (R /. z) = ((( id the carrier of ( REAL-NS 1)) * R) . (I . z1)) by FUNCT_2: 17;

            then (R /. z) = (((I * J) * R) . (I . z1)) by A12, REAL_NS1:def 4;

            then

             A15: (R /. z) = ((I * J) . (R . (I . z1))) by A14, FUNCT_1: 13;

            ( dom J) = ( REAL 1) by FUNCT_2:def 1;

            then (R /. z) = (I . (J . (R0 . z))) by A15, FUNCT_1: 13, FUNCT_2: 5;

            then (R /. z) = (I . ((J * R0) . (I . z1))) by A13, FUNCT_1: 12;

            then (R /. z) = (I . (R1 . z1)) by A5, FUNCT_1: 12;

            then

             A16: ||.(R /. z).|| = |.(R1 . z1).| by A1, Th3;

            

             A17: ( ||.z.|| " ) = ( |.z1.| " ) by A1, Th3;

             ||.z.|| < d by A1, A10, Th3;

            hence thesis by A8, A11, A17, A16;

          end;

          hence thesis by A7;

        end;

        for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0

        proof

          let h be 0 -convergent non-zero Real_Sequence;

           A18:

          now

            let r0 be Real;

            reconsider r = r0 as Real;

            

             A19: ( lim h) = 0 ;

            assume r0 > 0 ;

            then

            consider d be Real such that

             A20: d > 0 and

             A21: for z1 be Real st z1 <> 0 & |.z1.| < d holds (( |.z1.| " ) * |.(R1 . z1).|) < r by A6;

            reconsider d1 = d as Real;

            consider m be Nat such that

             A22: for n be Nat st m <= n holds |.((h . n) - 0 ).| < d1 by A20, A19, SEQ_2:def 7;

            take m;

            hereby

              let n be Nat;

              

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

              

               A24: n in NAT by ORDINAL1:def 12;

              ( rng h) c= ( dom R1) by A5;

              

              then

               A25: (( |.(h . n).| " ) * |.(R1 . (h . n)).|) = (( |.(h . n).| " ) * |.((R1 /* h) . n).|) by FUNCT_2: 108, A24

              .= (((( abs h) . n) " ) * |.((R1 /* h) . n).|) by SEQ_1: 12

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

              .= ((( abs (h " )) . n) * |.((R1 /* h) . n).|) by SEQ_1: 54

              .= ( |.((h " ) . n).| * |.((R1 /* h) . n).|) by SEQ_1: 12

              .= |.(((h " ) . n) * ((R1 /* h) . n)).| by COMPLEX1: 65

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

              assume m <= n;

              then |.((h . n) - 0 ).| < d by A22;

              hence |.((((h " ) (#) (R1 /* h)) . n) - 0 ).| < r0 by A21, A23, A25;

            end;

          end;

          hence ((h " ) (#) (R1 /* h)) is convergent by SEQ_2:def 6;

          hence thesis by A18, SEQ_2:def 7;

        end;

        hence thesis by A4, FDIFF_1:def 2;

      end;

      thus for L be LinearOperator of ( REAL-NS 1), ( REAL-NS 1) holds ((J * L) * I) is LinearFunc

      proof

        let L be LinearOperator of ( REAL-NS 1), ( REAL-NS 1);

        

         A26: the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

        then

        reconsider L0 = L as Function of ( REAL 1), ( REAL 1);

        reconsider L1 = ((J * L0) * I) as PartFunc of REAL , REAL ;

        

         A27: ( dom (J * L0)) = ( REAL 1) by FUNCT_2:def 1;

        consider r be Real such that

         A28: r = (L1 . 1);

        

         A29: ( dom ((J * L0) * I)) = REAL by FUNCT_2:def 1;

        

         A30: ( dom L0) = ( REAL 1) by FUNCT_2:def 1;

        for p be Real holds (L1 . p) = (r * p)

        proof

          reconsider 1p = (I . jj) as VECTOR of ( REAL-NS 1) by REAL_NS1:def 4;

          let p be Real;

          reconsider pp = p, jj = 1 as Element of REAL by XREAL_0:def 1;

          ( dom I) = REAL by FUNCT_2:def 1;

          then (L1 . p) = ((J * L) . (I . (pp * jj))) by FUNCT_1: 13;

          then (L1 . p) = ((J * L) . (p * 1p)) by A1, Th3;

          then (L1 . p) = (J . (L . (p * 1p))) by A26, A30, FUNCT_1: 13;

          then (L1 . p) = (J . (p * (L . 1p))) by LOPBAN_1:def 5;

          then (L1 . p) = (p * (J . (L . 1p))) by A2, Th4;

          then (L1 . p) = (p * ((J * L0) . (I . jj))) by A27, FUNCT_1: 12;

          hence thesis by A29, A28, FUNCT_1: 12;

        end;

        hence thesis by FDIFF_1:def 3;

      end;

    end;

    theorem :: PDIFF_1:6

    

     Th6: for I be Function of REAL , ( REAL 1), J be Function of ( REAL 1), REAL st I = (( proj (1,1)) qua Function " ) & J = ( proj (1,1)) holds (for R be RestFunc holds ((I * R) * J) is RestFunc of ( REAL-NS 1), ( REAL-NS 1)) & for L be LinearFunc holds ((I * L) * J) is Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1)

    proof

      let I be Function of REAL , ( REAL 1), J be Function of ( REAL 1), REAL ;

      assume that

       A1: I = (( proj (1,1)) qua Function " ) and

       A2: J = ( proj (1,1));

      thus for R be RestFunc holds ((I * R) * J) is RestFunc of ( REAL-NS 1), ( REAL-NS 1)

      proof

        let R be RestFunc;

        R is total by FDIFF_1:def 2;

        then

        reconsider R0 = R as Function of REAL , REAL ;

        

         A3: the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

        then

        reconsider R1 = ((I * R0) * J) as PartFunc of ( REAL-NS 1), ( REAL-NS 1);

        for h be ( 0. ( REAL-NS 1)) -convergent non-zero sequence of ( REAL-NS 1) holds (( ||.h.|| " ) (#) (R1 /* h)) is convergent & ( lim (( ||.h.|| " ) (#) (R1 /* h))) = ( 0. ( REAL-NS 1))

        proof

          let h be ( 0. ( REAL-NS 1)) -convergent non-zero sequence of ( REAL-NS 1);

          

           A4: ( lim h) = ( 0. ( REAL-NS 1)) by NDIFF_1:def 4;

          deffunc F( Nat) = (J . (h . $1));

          consider s be Real_Sequence such that

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

          

           A6: h is convergent by NDIFF_1:def 4;

           A7:

          now

            let p be Real;

            assume 0 < p;

            then

            consider m be Nat such that

             A8: for n be Nat st m <= n holds ||.((h . n) - ( 0. ( REAL-NS 1))).|| < p by A6, A4, NORMSP_1:def 7;

            reconsider m as Nat;

            take m;

            now

              let n be Nat;

              assume

               A9: m <= n;

              reconsider nn = n as Nat;

               ||.((h . nn) - ( 0. ( REAL-NS 1))).|| < p by A8, A9;

              then

               A10: ||.(h . nn).|| < p by RLVECT_1: 13;

              (s . n) = (J . (h . n)) by A5;

              hence |.((s . n) - 0 ).| < p by A2, A10, Th4;

            end;

            hence for n be Nat st m <= n holds |.((s . n) - 0 ).| < p;

          end;

          then

           A11: s is convergent by SEQ_2:def 6;

          then

           A12: ( lim s) = 0 by A7, SEQ_2:def 7;

          now

            let x be object;

            assume x in NAT ;

            then

            reconsider n = x as Element of NAT ;

            

             A13: 0 <= |.(s . n).| by COMPLEX1: 46;

            (h . n) <> ( 0. ( REAL-NS 1)) by NDIFF_1: 6;

            then

             A14: ||.(h . n).|| <> 0 by NORMSP_0:def 5;

            (s . n) = (J . (h . n)) by A5;

            then |.(s . x).| <> 0 by A2, A14, Th4;

            hence (s . x) <> 0 by A13, COMPLEX1: 47;

          end;

          then s is non-zero by SEQ_1: 4;

          then

          reconsider s as 0 -convergent non-zero Real_Sequence by A11, A12, FDIFF_1:def 1;

          

           A15: (J * I) = ( id REAL ) by A1, A2, Lm1, FUNCT_1: 39;

          now

            reconsider f1 = R1 as Function;

            let n be Element of NAT ;

            

             A16: ( rng h) c= the carrier of ( REAL-NS 1);

            (h . n) in the carrier of ( REAL-NS 1);

            then

             A17: (h . n) in ( REAL 1) by REAL_NS1:def 4;

            

             A18: ((R0 * J) . (h . n)) in REAL by XREAL_0:def 1;

            R1 is total by A3;

            then ((R /* s) . n) = (R . (s . n)) by FUNCT_2: 115;

            then ((R /* s) . n) = (R . (J . (h . n))) by A5;

            then ((R /* s) . n) = ((J * I) . (R0 . (J . (h . n)))) by A15;

            then ((R /* s) . n) = ((J * I) . ((R0 * J) . (h . n))) by A17, FUNCT_2: 15;

            then ((R /* s) . n) = (J . (I . ((R0 * J) . (h . n)))) by FUNCT_2: 15, A18;

            then

             A19: ((R /* s) . n) = (J . ((I * (R0 * J)) . (h . n))) by A17, FUNCT_2: 15;

             NAT = ( dom h) by FUNCT_2:def 1;

            then

             A20: (R1 . (h . n)) = ((f1 * h) . n) by FUNCT_1: 13;

            ( dom R1) = ( REAL 1) by FUNCT_2:def 1;

            then ( rng h) c= ( dom R1) by A16, REAL_NS1:def 4;

            then (R1 . (h . n)) = ((R1 /* h) . n) by A20, FUNCT_2:def 11;

            then

             A21: ((R /* s) . n) = (J . ((R1 /* h) . n)) by A19, RELAT_1: 36;

            

             A22: (s . n) = (J . (h . n)) by A5;

            ( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . n) = ||.((( ||.h.|| " ) (#) (R1 /* h)) . n).|| by NORMSP_0:def 4

            .= ||.((( ||.h.|| " ) . n) * ((R1 /* h) . n)).|| by NDIFF_1:def 2

            .= ( |.(( ||.h.|| " ) . n).| * ||.((R1 /* h) . n).||) by NORMSP_1:def 1

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

            .= ( |.( ||.(h . n).|| " ).| * ||.((R1 /* h) . n).||) by NORMSP_0:def 4

            .= (( ||.(h . n).|| " ) * ||.((R1 /* h) . n).||) by ABSVALUE:def 1

            .= (( |.(s . n).| " ) * ||.((R1 /* h) . n).||) by A2, A22, Th4

            .= (( |.(s . n).| " ) * |.((R /* s) . n).|) by A2, A21, Th4

            .= (( |.(s . n).| " ) * ( |.(R /* s).| . n)) by SEQ_1: 12

            .= (((( abs s) . n) " ) * ( |.(R /* s).| . n)) by SEQ_1: 12

            .= (((( abs s) " ) . n) * ( |.(R /* s).| . n)) by VALUED_1: 10

            .= (((( abs s) " ) (#) |.(R /* s).|) . n) by SEQ_1: 8

            .= (( |.(s " ).| (#) ( abs (R /* s))) . n) by SEQ_1: 54;

            hence ( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . n) = ( |.((s " ) (#) (R /* s)).| . n) by SEQ_1: 52;

          end;

          then

           A23: ||.(( ||.h.|| " ) (#) (R1 /* h)).|| = |.((s " ) (#) (R /* s)).| by FUNCT_2: 63;

          

           A24: ( lim ((s " ) (#) (R /* s))) = 0 by FDIFF_1:def 2;

          

           A25: ((s " ) (#) (R /* s)) is convergent by FDIFF_1:def 2;

          then ( lim |.((s " ) (#) (R /* s)).|) = |.( lim ((s " ) (#) (R /* s))).| by SEQ_4: 14;

          then

           A26: ( lim |.((s " ) (#) (R /* s)).|) = 0 by A24, ABSVALUE: 2;

          

           A27: ( abs ((s " ) (#) (R /* s))) is convergent by A25, SEQ_4: 13;

           A28:

          now

            let p be Real;

            assume 0 < p;

            then

            consider m be Nat such that

             A29: for n be Nat st m <= n holds |.(( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . n) - 0 ).| < p by A23, A27, A26, SEQ_2:def 7;

            reconsider m as Nat;

            take m;

            let n be Nat;

            assume m <= n;

            then |.(( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . n) - 0 ).| < p by A29;

            then

             A30: |. ||.((( ||.h.|| " ) (#) (R1 /* h)) . n).||.| < p by NORMSP_0:def 4;

             ||.((( ||.h.|| " ) (#) (R1 /* h)) . n).|| < p by A30, ABSVALUE:def 1;

            hence ||.(((( ||.h.|| " ) (#) (R1 /* h)) . n) - ( 0. ( REAL-NS 1))).|| < p by RLVECT_1: 13;

          end;

          then (( ||.h.|| " ) (#) (R1 /* h)) is convergent by NORMSP_1:def 6;

          hence thesis by A28, NORMSP_1:def 7;

        end;

        hence thesis by A3, NDIFF_1:def 10;

      end;

      thus for L be LinearFunc holds ((I * L) * J) is Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1)

      proof

        let L be LinearFunc;

        consider r be Real such that

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

        L is total by FDIFF_1:def 3;

        then

        reconsider L0 = L as Function of REAL , REAL ;

        reconsider r as Real;

        set K = |.r.|;

        

         A32: the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

        ((I * L0) * J) is Function of ( REAL 1), ( REAL 1);

        then

        reconsider L1 = ((I * L) * J) as Function of ( REAL-NS 1), ( REAL-NS 1) by A32;

        

         A33: ( dom L1) = ( REAL 1) by A32, FUNCT_2:def 1;

        

         A34: ( dom L0) = REAL by FUNCT_2:def 1;

         A35:

        now

          let x,y be VECTOR of ( REAL-NS 1);

          

           A36: ((J . x) + (J . y)) in REAL by XREAL_0:def 1;

          

           A37: (J . x) in REAL by XREAL_0:def 1;

          (J . y) in REAL by XREAL_0:def 1;

          then (I . (L . (J . y))) = ((I * L) . (J . y)) by A34, FUNCT_1: 13;

          then

           A38: (I . (L . (J . y))) = (L1 . y) by A32, A33, FUNCT_1: 12;

          (L1 . (x + y)) = ((I * L) . (J . (x + y))) by A32, A33, FUNCT_1: 12;

          then (L1 . (x + y)) = ((I * L) . ((J . x) + (J . y))) by A2, Th4;

          then (L1 . (x + y)) = (I . (L . ((J . x) + (J . y)))) by A36, A34, FUNCT_1: 13;

          then (L1 . (x + y)) = (I . (r * ((J . x) + (J . y)))) by A31;

          then (L1 . (x + y)) = (I . ((r * (J . x)) + (r * (J . y))));

          then (L1 . (x + y)) = (I . ((L . (J . x)) + (r * (J . y)))) by A31;

          then

           A39: (L1 . (x + y)) = (I . ((L . (J . x)) + (L . (J . y)))) by A31;

          (I . (L . (J . x))) = ((I * L) . (J . x)) by A37, A34, FUNCT_1: 13;

          then (I . (L . (J . x))) = (L1 . x) by A32, A33, FUNCT_1: 12;

          hence (L1 . (x + y)) = ((L1 . x) + (L1 . y)) by A1, A38, A39, Th3;

        end;

        now

          let x be VECTOR of ( REAL-NS 1), a be Real;

          reconsider aa = a as Real;

          

           A40: (J . x) in REAL by XREAL_0:def 1;

          

           A41: (aa * (J . x)) in REAL by XREAL_0:def 1;

          (L1 . (a * x)) = ((I * L) . (J . (a * x))) by A32, A33, FUNCT_1: 12;

          then (L1 . (a * x)) = ((I * L) . (a * (J . x))) by A2, Th4;

          then (L1 . (aa * x)) = (I . (L . (aa * (J . x)))) by A41, A34, FUNCT_1: 13;

          then (L1 . (a * x)) = (I . (r * (a * (J . x)))) by A31;

          then (L1 . (a * x)) = (I . (a * (r * (J . x))));

          then

           A42: (L1 . (a * x)) = (I . (a * (L . (J . x)))) by A31;

          (I . (L . (J . x))) = ((I * L) . (J . x)) by A40, A34, FUNCT_1: 13;

          then (I . (L . (J . x))) = (L1 . x) by A32, A33, FUNCT_1: 12;

          hence (L1 . (a * x)) = (a * (L1 . x)) by A1, A42, Th3;

        end;

        then

        reconsider L1 as LinearOperator of ( REAL-NS 1), ( REAL-NS 1) by A35, VECTSP_1:def 20, LOPBAN_1:def 5;

         A43:

        now

          let x be VECTOR of ( REAL-NS 1);

          (J . x) in REAL by XREAL_0:def 1;

          then (I . (L . (J . x))) = ((I * L) . (J . x)) by A34, FUNCT_1: 13;

          then (I . (L . (J . x))) = (L1 . x) by A32, A33, FUNCT_1: 12;

          then ||.(L1 . x).|| = |.(L . (J . x)).| by A1, Th3;

          then ||.(L1 . x).|| = |.(r * (J . x)).| by A31;

          then ||.(L1 . x).|| = ( |.r.| * |.(J . x).|) by COMPLEX1: 65;

          hence ||.(L1 . x).|| <= (K * ||.x.||) by A2, Th4;

        end;

         0 <= K by COMPLEX1: 46;

        hence thesis by A43, LOPBAN_1:def 8;

      end;

    end;

    reserve f for PartFunc of ( REAL-NS 1), ( REAL-NS 1);

    reserve g for PartFunc of REAL , REAL ;

    reserve x for Point of ( REAL-NS 1);

    reserve y for Real;

    theorem :: PDIFF_1:7

    

     Th7: f = ( <>* g) & x = <*y*> & f is_differentiable_in x implies g is_differentiable_in y & ( diff (g,y)) = (((( proj (1,1)) * ( diff (f,x))) * (( proj (1,1)) qua Function " )) . 1)

    proof

      set J = ( proj (1,1)) qua Function;

      reconsider L = ( diff (f,x)) as Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1) by LOPBAN_1:def 9;

      

       A1: ( rng g) c= ( dom I) by Th2;

      reconsider L0 = ((J * L) * I) as LinearFunc by Th5;

      assume that

       A2: f = ( <>* g) and

       A3: x = <*y*> and

       A4: f is_differentiable_in x;

      consider NN be Neighbourhood of x such that

       A5: NN c= ( dom f) and

       A6: ex R be RestFunc of ( REAL-NS 1), ( REAL-NS 1) st for y be Point of ( REAL-NS 1) st y in NN holds ((f /. y) - (f /. x)) = ((( diff (f,x)) . (y - x)) + (R /. (y - x))) by A4, NDIFF_1:def 7;

      consider e be Real such that

       A7: 0 < e and

       A8: { z where z be Point of ( REAL-NS 1) : ||.(z - x).|| < e } c= NN by NFCONT_1:def 1;

      consider R be RestFunc of ( REAL-NS 1), ( REAL-NS 1) such that

       A9: for x9 be Point of ( REAL-NS 1) st x9 in NN holds ((f /. x9) - (f /. x)) = ((( diff (f,x)) . (x9 - x)) + (R /. (x9 - x))) by A6;

      set N = { z where z be Point of ( REAL-NS 1) : ||.(z - x).|| < e };

      

       A10: N c= the carrier of ( REAL-NS 1)

      proof

        let y be object;

        assume y in N;

        then ex z be Point of ( REAL-NS 1) st y = z & ||.(z - x).|| < e;

        hence thesis;

      end;

      then

      reconsider N as Neighbourhood of x by A7, NFCONT_1:def 1;

      set N0 = { z where z be Element of REAL : |.(z - y).| < e };

      

       A11: N c= ( dom f) by A5, A8;

      now

        let z be object;

        hereby

          assume z in N0;

          then

          consider y9 be Element of REAL such that

           A12: z = y9 and

           A13: |.(y9 - y).| < e;

          reconsider w = (I . y9) as Point of ( REAL-NS 1) by REAL_NS1:def 4;

          x = (I . y) by A3, Lm1;

          then (w - x) = (I . (y9 - y)) by Th3;

          then ||.(w - x).|| = |.(y9 - y).| by Th3;

          then w in { z0 where z0 be Point of ( REAL-NS 1) : ||.(z0 - x).|| < e } by A13;

          then (J . w) in (J .: N) by FUNCT_2: 35;

          hence z in (J .: N) by A12, Lm1, FUNCT_1: 35;

        end;

        assume z in (J .: N);

        then

        consider ww be object such that ww in ( REAL 1) and

         A14: ww in N and

         A15: z = (J . ww) by FUNCT_2: 64;

        consider w be Point of ( REAL-NS 1) such that

         A16: ww = w and

         A17: ||.(w - x).|| < e by A14;

        reconsider y9 = (J . w) as Element of REAL by XREAL_0:def 1;

        (J . x) = y by A3, Lm1;

        then (J . (w - x)) = (y9 - y) by Th4;

        then |.(y9 - y).| < e by A17, Th4;

        hence z in N0 by A15, A16;

      end;

      then

       A18: N0 = (J .: N) by TARSKI: 2;

      ( dom f) = (J " ( dom (I * g))) by A2, RELAT_1: 147;

      then (J .: ( dom f)) = (J .: (J " ( dom g))) by A1, RELAT_1: 27;

      then

       A19: (J .: ( dom f)) = ( dom g) by Lm1, FUNCT_1: 77;

      

       A20: (I * J) = ( id ( REAL 1)) by Lm1, FUNCT_1: 39;

      reconsider R0 = ((J * R) * I) as RestFunc by Th5;

      

       A21: (J * I) = ( id REAL ) by Lm1, FUNCT_1: 39;

      N c= ( dom f) by A5, A8;

      then

       A22: N0 c= ( dom g) by A19, A18, RELAT_1: 123;

      

       A23: ].(y - e), (y + e).[ c= N0

      proof

        let d be object such that

         A24: d in ].(y - e), (y + e).[;

        reconsider y0 = d as Element of REAL by A24;

         |.(y0 - y).| < e by A24, RCOMP_1: 1;

        hence thesis;

      end;

      N0 c= ].(y - e), (y + e).[

      proof

        let d be object;

        assume d in N0;

        then ex r be Element of REAL st d = r & |.(r - y).| < e;

        hence thesis by RCOMP_1: 1;

      end;

      then N0 = ].(y - e), (y + e).[ by A23, XBOOLE_0:def 10;

      then

       A25: N0 is Neighbourhood of y by A7, RCOMP_1:def 6;

      N c= ( REAL 1) by A10, REAL_NS1:def 4;

      then ((I * J) .: N) = N by A20, FRECHET: 13;

      then

       A26: (I .: N0) = N by A18, RELAT_1: 126;

      

       A27: for y0 be Real st y0 in N0 holds ((g . y0) - (g . y)) = ((L0 . (y0 - y)) + (R0 . (y0 - y)))

      proof

        let y0 be Real;

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

        reconsider y9 = (I . yy0) as Point of ( REAL-NS 1) by REAL_NS1:def 4;

        R is total by NDIFF_1:def 5;

        then

         A28: ( dom R) = the carrier of ( REAL-NS 1) by PARTFUN1:def 2;

        R0 is total by FDIFF_1:def 2;

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

        then (yy0 - yy) in ( dom ((J * R) * I));

        then

         A29: (y0 - y) in ( dom (J * (R * I))) by RELAT_1: 36;

        (I . (yy0 - yy)) in ( REAL 1);

        then (I . (yy0 - yy)) in ( dom R) by A28, REAL_NS1:def 4;

        then (J . (R /. (I . (yy0 - yy)))) = (J . (R . (I . (yy0 - yy)))) by PARTFUN1:def 6;

        then (J . (R /. (I . (yy0 - yy)))) = (J . ((R * I) . (yy0 - yy))) by Th2, FUNCT_1: 13;

        then (J . (R /. (I . (yy0 - yy)))) = ((J * (R * I)) . (yy0 - yy)) by A29, FUNCT_1: 12;

        then

         A30: (J . (R /. (I . (yy0 - yy)))) = (R0 . (yy0 - yy)) by RELAT_1: 36;

        L0 is total by FDIFF_1:def 3;

        then ( dom ((J * L) * I)) = REAL by PARTFUN1:def 2;

        then (yy0 - yy) in ( dom ((J * L) * I));

        then

         A31: (y0 - y) in ( dom (J * (L * I))) by RELAT_1: 36;

        assume

         A32: y0 in N0;

        then

         A33: (I . yy0) in N by A26, FUNCT_2: 35;

        then (J . (f /. (I . yy0))) = (J . (f . (I . yy0))) by A11, PARTFUN1:def 6;

        then

         A34: (J . (f /. (I . yy0))) = (J . ((f * I) . yy0)) by Th2, FUNCT_1: 13;

        (J * f) = (J * (I * (g * J))) by A2, RELAT_1: 36;

        then

         A35: (J * f) = (( id REAL ) * (g * J)) by A21, RELAT_1: 36;

        ( rng (g * J)) c= REAL ;

        then ((J * f) * I) = ((g * J) * I) by A35, RELAT_1: 53;

        then

         A36: ((J * f) * I) = (g * ( id REAL )) by A21, RELAT_1: 36;

        ( dom g) c= REAL ;

        then

         A37: g = ((J * f) * I) by A36, RELAT_1: 51;

        y0 in ( dom g) by A22, A32;

        then y0 in ( dom (J * (f * I))) by A37, RELAT_1: 36;

        then (J . (f /. (I . y0))) = ((J * (f * I)) . y0) by A34, FUNCT_1: 12;

        then

         A38: (J . (f /. (I . y0))) = (g . y0) by A37, RELAT_1: 36;

        

         A39: x = (I . y) by A3, Lm1;

        set Iy = (I . yy);

        x in N by NFCONT_1: 4;

        then (J . (f /. (I . y))) = (J . (f . Iy)) by A11, A39, PARTFUN1:def 6;

        then

         A40: (J . (f /. Iy)) = (J . ((f * I) . yy)) by Th2, FUNCT_1: 13;

        y in N0 by A25, RCOMP_1: 16;

        then y in ( dom g) by A22;

        then y in ( dom (J * (f * I))) by A37, RELAT_1: 36;

        then (J . (f /. (I . y))) = ((J * (f * I)) . y) by A40, FUNCT_1: 12;

        then

         A41: (J . (f /. (I . y))) = (g . y) by A37, RELAT_1: 36;

        (J . ((f /. y9) - (f /. x))) = (J . ((L . (y9 - x)) + (R /. (y9 - x)))) by A9, A8, A33;

        then ((J . (f /. y9)) - (J . (f /. x))) = (J . ((L . (y9 - x)) + (R /. (y9 - x)))) by Th4;

        then ((J . (f /. (I . y0))) - (J . (f /. (I . y)))) = ((J . (L . (y9 - x))) + (J . (R /. (y9 - x)))) by A39, Th4;

        then

         A42: ((J . (f /. (I . y0))) - (J . (f /. (I . y)))) = ((J . (L . (I . (y0 - y)))) + (J . (R /. (y9 - x)))) by A39, Th3;

        (J . (L . (I . (yy0 - yy)))) = (J . ((L * I) . (yy0 - yy))) by Th2, FUNCT_1: 13;

        then (J . (L . (I . (y0 - y)))) = ((J * (L * I)) . (y0 - y)) by A31, FUNCT_1: 12;

        then (J . (L . (I . (y0 - y)))) = (L0 . (y0 - y)) by RELAT_1: 36;

        hence thesis by A39, A42, A38, A41, A30, Th3;

      end;

      hence g is_differentiable_in y by A25, A22, FDIFF_1:def 4;

      hence thesis by A25, A22, A27, FDIFF_1:def 5;

    end;

    theorem :: PDIFF_1:8

    

     Th8: f = ( <>* g) & x = <*y*> & g is_differentiable_in y implies f is_differentiable_in x & (( diff (f,x)) . <*1*>) = <*( diff (g,y))*>

    proof

      set J = ( proj (1,1));

      assume that

       A1: f = ( <>* g) and

       A2: x = <*y*> and

       A3: g is_differentiable_in y;

      reconsider x0 = y as Real;

      consider N0 be Neighbourhood of x0 such that

       A4: N0 c= ( dom g) and

       A5: ex L0 be LinearFunc, R0 be RestFunc st ( diff (g,x0)) = (L0 . 1) & for y0 be Real st y0 in N0 holds ((g . y0) - (g . x0)) = ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by A3, FDIFF_1:def 5;

      consider e0 be Real such that

       A6: 0 < e0 and

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

      reconsider e = e0 as Real;

      set N = { z where z be Point of ( REAL-NS 1) : ||.(z - x).|| < e };

      

       A8: ( rng (g * J)) c= REAL ;

      consider L0 be LinearFunc, R0 be RestFunc such that

       A9: ( diff (g,x0)) = (L0 . 1) and

       A10: for y0 be Real st y0 in N0 holds ((g . y0) - (g . x0)) = ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by A5;

      reconsider R = ((I * R0) * J) as RestFunc of ( REAL-NS 1), ( REAL-NS 1) by Th6;

      reconsider L = ((I * L0) * J) as Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1) by Th6;

      

       A11: ( dom g) c= REAL ;

      ( dom f) c= the carrier of ( REAL-NS 1);

      then

       A12: ( dom f) c= ( rng I) by Th2, REAL_NS1:def 4;

      

       A13: (J * I) = ( id REAL ) by Lm1, FUNCT_1: 39;

      now

        let z be object;

        hereby

          assume z in N;

          then

          consider w be Point of ( REAL-NS 1) such that

           A14: z = w and

           A15: ||.(w - x).|| < e;

          reconsider y = (J . w) as Element of REAL by XREAL_0:def 1;

          (J . x) = x0 by A2, Lm1;

          then (J . (w - x)) = (y - x0) by Th4;

          then |.(y - x0).| < e by A15, Th4;

          then

           A16: y in N0 by A7, RCOMP_1: 1;

          w in the carrier of ( REAL-NS 1);

          then w in ( dom J) by Lm1, REAL_NS1:def 4;

          then w = (I . y) by FUNCT_1: 34;

          hence z in (I .: N0) by A14, A16, FUNCT_2: 35;

        end;

        assume z in (I .: N0);

        then

        consider yy be object such that

         A17: yy in REAL and

         A18: yy in N0 and

         A19: z = (I . yy) by FUNCT_2: 64;

        reconsider y = yy as Element of REAL by A17;

        reconsider w = (I . y) as Point of ( REAL-NS 1) by REAL_NS1:def 4;

        (I . x0) = x by A2, Lm1;

        then

         A20: (w - x) = (I . (y - x0)) by Th3;

         |.(y - x0).| < e by A7, A18, RCOMP_1: 1;

        then ||.(w - x).|| < e by A20, Th3;

        hence z in N by A19;

      end;

      then

       A21: N = (I .: N0) by TARSKI: 2;

      (J * f) = (J * (I * (g * J))) by A1, RELAT_1: 36;

      then (J * f) = (( id REAL ) * (g * J)) by A13, RELAT_1: 36;

      then ((J * f) * I) = ((g * J) * I) by A8, RELAT_1: 53;

      then ((J * f) * I) = (g * ( id REAL )) by A13, RELAT_1: 36;

      then g = ((J * f) * I) by A11, RELAT_1: 51;

      then

       A22: ( dom g) = (I " ( dom (J * f))) by RELAT_1: 147;

      ( rng f) c= the carrier of ( REAL-NS 1);

      then ( rng f) c= ( dom J) by Lm1, REAL_NS1:def 4;

      then (I .: ( dom g)) = (I .: (I " ( dom f))) by A22, RELAT_1: 27;

      then (I .: ( dom g)) = ( dom f) by A12, FUNCT_1: 77;

      then

       A23: N c= ( dom f) by A4, A21, RELAT_1: 123;

      N c= the carrier of ( REAL-NS 1)

      proof

        let y be object;

        assume y in N;

        then ex z be Point of ( REAL-NS 1) st y = z & ||.(z - x).|| < e;

        hence thesis;

      end;

      then

       A24: N is Neighbourhood of x by A6, NFCONT_1:def 1;

      (J * I) = ( id REAL ) by Lm1, FUNCT_1: 39;

      then ((J * I) .: N0) = N0 by FRECHET: 13;

      then

       A25: (J .: N) = N0 by A21, RELAT_1: 126;

      

       A26: for y be Point of ( REAL-NS 1) st y in N holds ((f /. y) - (f /. x)) = ((L . (y - x)) + (R /. (y - x)))

      proof

        x in the carrier of ( REAL-NS 1);

        then x in ( dom J) by Lm1, REAL_NS1:def 4;

        then

         A27: (I . (g . (J . x))) = (I . ((g * J) . x)) by FUNCT_1: 13;

        

         A28: x in N by A24, NFCONT_1: 4;

        then x in ( dom f) by A23;

        then x in ( dom (I * (g * J))) by A1, RELAT_1: 36;

        then (I . (g . (J . x))) = ((I * (g * J)) . x) by A27, FUNCT_1: 12;

        then (I . (g . (J . x))) = (f . x) by A1, RELAT_1: 36;

        then

         A29: (I . (g . (J . x))) = (f /. x) by A23, A28, PARTFUN1:def 6;

        let y be Point of ( REAL-NS 1);

        assume

         A30: y in N;

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

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

        reconsider gy0 = (g . y0), gx0 = (g . x0), g0 = (g . 0 ) as Element of REAL by XREAL_0:def 1;

        reconsider L0y0x0 = (L0 . y0x0) as Element of REAL by XREAL_0:def 1;

        reconsider R0y0x0 = (R0 . y0x0), Jyx = (J . (y - x)) as Element of REAL by XREAL_0:def 1;

        reconsider gJy = (g . (J . y)), gJx = (g . (J . x)) as Element of REAL by XREAL_0:def 1;

        reconsider R0Jyx = (R0 . Jyx), L0Jyx = (L0 . Jyx) as Element of REAL by XREAL_0:def 1;

        reconsider p1 = (I . gy0), p2 = (I . gx0), q1 = (I . L0y0x0), q2 = (I . R0y0x0) as VECTOR of ( REAL-NS 1) by REAL_NS1:def 4;

        

         A31: (J . x) = x0 by A2, Lm1;

        y in the carrier of ( REAL-NS 1);

        then y in ( REAL 1) by REAL_NS1:def 4;

        then (I . ((g . y0) - (g . x0))) = (I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0)))) by A10, A25, A30, FUNCT_2: 35;

        then (p1 - p2) = (I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0)))) by Th3;

        then (p1 - p2) = (q1 + q2) by Th3;

        then ((I . gy0) - (I . gx0)) = (q1 + q2) by REAL_NS1: 5;

        then ((I . gJy) - (I . gJx)) = ((I . L0y0x0) + (I . R0y0x0)) by A31, REAL_NS1: 2;

        then ((I . gJy) - (I . gJx)) = ((I . L0Jyx) + (I . R0y0x0)) by A31, Th4;

        then

         A32: ((I . gJy) - (I . gJx)) = ((I . L0Jyx) + (I . R0Jyx)) by A31, Th4;

        ( dom L) = the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

        then (y - x) in ( dom ((I * L0) * J));

        then

         A33: (y - x) in ( dom (I * (L0 * J))) by RELAT_1: 36;

        (y - x) in the carrier of ( REAL-NS 1);

        then

         A34: (y - x) in ( dom J) by Lm1, REAL_NS1:def 4;

        then

         A35: (I . (R0 . (J . (y - x)))) = (I . ((R0 * J) . (y - x))) by FUNCT_1: 13;

        R is total by NDIFF_1:def 5;

        then

         A36: ( dom ((I * R0) * J)) = the carrier of ( REAL-NS 1) by PARTFUN1:def 2;

        then (y - x) in ( dom ((I * R0) * J));

        then (y - x) in ( dom (I * (R0 * J))) by RELAT_1: 36;

        then (I . (R0 . (J . (y - x)))) = ((I * (R0 * J)) . (y - x)) by A35, FUNCT_1: 12;

        then (I . (R0 . (J . (y - x)))) = (((I * R0) * J) . (y - x)) by RELAT_1: 36;

        then

         A37: (I . (R0 . (J . (y - x)))) = (R /. (y - x)) by A36, PARTFUN1:def 6;

        y in the carrier of ( REAL-NS 1);

        then y in ( dom J) by Lm1, REAL_NS1:def 4;

        then

         A38: (I . (g . (J . y))) = (I . ((g * J) . y)) by FUNCT_1: 13;

        (I . (L0 . (J . (y - x)))) = (I . ((L0 * J) . (y - x))) by A34, FUNCT_1: 13;

        then (I . (L0 . (J . (y - x)))) = ((I * (L0 * J)) . (y - x)) by A33, FUNCT_1: 12;

        then

         A39: (I . (L0 . (J . (y - x)))) = (L . (y - x)) by RELAT_1: 36;

        y in ( dom f) by A23, A30;

        then y in ( dom (I * (g * J))) by A1, RELAT_1: 36;

        then (I . (g . (J . y))) = ((I * (g * J)) . y) by A38, FUNCT_1: 12;

        then (I . (g . (J . y))) = (f . y) by A1, RELAT_1: 36;

        then (I . (g . (J . y))) = (f /. y) by A23, A30, PARTFUN1:def 6;

        then ((I . gJy) - (I . gJx)) = ((f /. y) - (f /. x)) by A29, REAL_NS1: 5;

        hence thesis by A32, A37, A39, REAL_NS1: 2;

      end;

      L0 is total by FDIFF_1:def 3;

      then

       A40: ( dom L0) = REAL by PARTFUN1:def 2;

      

       A41: L is Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),( REAL-NS 1))) by LOPBAN_1:def 9;

      then f is_differentiable_in x by A24, A23, A26, NDIFF_1:def 6;

      then ( diff (f,x)) = ((I * L0) * J) by A24, A23, A41, A26, NDIFF_1:def 7;

      then (( diff (f,x)) . <*1*>) = (((I * L0) * J) . (I . 1)) by Lm1;

      then (( diff (f,x)) . <*jj*>) = ((I * L0) . (J . (I . jj))) by Lm1, FUNCT_1: 13;

      then (( diff (f,x)) . <*jj*>) = (I . (L0 . (J . (I . jj)))) by A40, FUNCT_1: 13;

      then (( diff (f,x)) . <*1*>) = (I . (L0 . 1)) by Lm1, FUNCT_1: 35;

      hence thesis by A24, A23, A9, A41, A26, Lm1, NDIFF_1:def 6;

    end;

    theorem :: PDIFF_1:9

    f = ( <>* g) & x = <*y*> implies (f is_differentiable_in x iff g is_differentiable_in y) by Th7, Th8;

    theorem :: PDIFF_1:10

    

     Th10: f = ( <>* g) & x = <*y*> & f is_differentiable_in x implies (( diff (f,x)) . <*1*>) = <*( diff (g,y))*>

    proof

      assume that

       A1: f = ( <>* g) and

       A2: x = <*y*> and

       A3: f is_differentiable_in x;

      g is_differentiable_in y by A1, A2, A3, Th7;

      hence thesis by A1, A2, Th8;

    end;

    begin

    reserve m,n for non zero Nat;

    reserve i,j for Nat;

    reserve f for PartFunc of ( REAL-NS n), ( REAL-NS 1);

    reserve g for PartFunc of ( REAL n), REAL ;

    reserve x for Point of ( REAL-NS n);

    reserve y for Element of ( REAL n);

    definition

      let n,m be non zero Nat;

      let i be Nat;

      let f be PartFunc of ( REAL-NS m), ( REAL-NS n);

      let x be Point of ( REAL-NS m);

      :: PDIFF_1:def9

      pred f is_partial_differentiable_in x,i means (f * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x);

    end

    definition

      let m,n be non zero Nat;

      let i be Nat;

      let f be PartFunc of ( REAL-NS m), ( REAL-NS n);

      let x be Point of ( REAL-NS m);

      :: PDIFF_1:def10

      func partdiff (f,x,i) -> Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),( REAL-NS n))) equals ( diff ((f * ( reproj (i,x))),(( Proj (i,m)) . x)));

      coherence ;

    end

    definition

      let n be non zero Nat;

      let i be Nat;

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

      let x be Element of ( REAL n);

      :: PDIFF_1:def11

      pred f is_partial_differentiable_in x,i means (f * ( reproj (i,x))) is_differentiable_in (( proj (i,n)) . x);

    end

    definition

      let n be non zero Nat;

      let i be Nat;

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

      let x be Element of ( REAL n);

      :: PDIFF_1:def12

      func partdiff (f,x,i) -> Real equals ( diff ((f * ( reproj (i,x))),(( proj (i,n)) . x)));

      coherence ;

    end

    theorem :: PDIFF_1:11

    

     Th11: ( Proj (i,n)) = ((( proj (1,1)) qua Function " ) * ( proj (i,n)))

    proof

      reconsider h = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL 1) by Th2;

      

       A1: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

       A2:

      now

        let x be Element of ( REAL n);

        reconsider z = x as Point of ( REAL-NS n) by REAL_NS1:def 4;

        

         A3: ((h * ( proj (i,n))) . x) = (h . (( proj (i,n)) . x)) by FUNCT_2: 15;

        hence ((h * ( proj (i,n))) . x) = <*(( proj (i,n)) . x)*> by Lm1;

        (( Proj (i,n)) . x) = (( Proj (i,n)) . z);

        then (( Proj (i,n)) . x) = <*(( proj (i,n)) . x)*> by Def4;

        hence (( Proj (i,n)) . x) = ((h * ( proj (i,n))) . x) by A3, Lm1;

      end;

      the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      hence thesis by A1, A2, FUNCT_2: 63;

    end;

    theorem :: PDIFF_1:12

    

     Th12: x = y implies (( reproj (i,y)) * ( proj (1,1))) = ( reproj (i,x))

    proof

      reconsider k = ( proj (1,1)) as Function of ( REAL 1), REAL ;

      

       A1: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

      assume

       A2: x = y;

       A3:

      now

        let s be Element of ( REAL 1);

        reconsider r = s as Point of ( REAL-NS 1) by REAL_NS1:def 4;

        

         A4: ((( reproj (i,y)) * k) . s) = (( reproj (i,y)) . (k . s)) by FUNCT_2: 15;

        ex q be Element of REAL , z be Element of ( REAL n) st r = <*q*> & z = x & (( reproj (i,x)) . r) = (( reproj (i,z)) . q) by Def6;

        hence (( reproj (i,x)) . s) = ((( reproj (i,y)) * k) . s) by A2, A4, Lm1;

      end;

      the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      hence thesis by A1, A3, FUNCT_2: 63;

    end;

    theorem :: PDIFF_1:13

    

     Th13: f = ( <>* g) & x = y implies ( <>* (g * ( reproj (i,y)))) = (f * ( reproj (i,x)))

    proof

      reconsider h = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL 1) by Th2;

      assume that

       A1: f = ( <>* g) and

       A2: x = y;

      (( reproj (i,y)) * ( proj (1,1))) = ( reproj (i,x)) by A2, Th12;

      then (((h * g) * ( reproj (i,y))) * ( proj (1,1))) = (f * ( reproj (i,x))) by A1, RELAT_1: 36;

      hence thesis by RELAT_1: 36;

    end;

    theorem :: PDIFF_1:14

    

     Th14: f = ( <>* g) & x = y implies (f is_partial_differentiable_in (x,i) iff g is_partial_differentiable_in (y,i))

    proof

      assume that

       A1: f = ( <>* g) and

       A2: x = y;

      

       A3: <*(( proj (i,n)) . y)*> = (( Proj (i,n)) . x) by A2, Def4;

      (f * ( reproj (i,x))) = ( <>* (g * ( reproj (i,y)))) by A1, A2, Th13;

      hence thesis by A3, Th7, Th8;

    end;

    theorem :: PDIFF_1:15

    

     Th15: f = ( <>* g) & x = y & f is_partial_differentiable_in (x,i) implies (( partdiff (f,x,i)) . <*1*>) = <*( partdiff (g,y,i))*>

    proof

      assume that

       A1: f = ( <>* g) and

       A2: x = y and

       A3: f is_partial_differentiable_in (x,i);

      

       A4: (f * ( reproj (i,x))) is_differentiable_in (( Proj (i,n)) . x) by A3;

      

       A5: <*(( proj (i,n)) . y)*> = (( Proj (i,n)) . x) by A2, Def4;

      (f * ( reproj (i,x))) = ( <>* (g * ( reproj (i,y)))) by A1, A2, Th13;

      hence thesis by A4, A5, Th10;

    end;

    definition

      let m,n be non zero Nat;

      let i be Nat;

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

      let x be Element of ( REAL m);

      :: PDIFF_1:def13

      pred f is_partial_differentiable_in x,i means ex g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st f = g & x = y & g is_partial_differentiable_in (y,i);

    end

    definition

      let m,n be non zero Nat;

      let i be Nat;

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

      let x be Element of ( REAL m);

      assume

       A1: f is_partial_differentiable_in (x,i);

      :: PDIFF_1:def14

      func partdiff (f,x,i) -> Element of ( REAL n) means

      : Def14: ex g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st f = g & x = y & it = (( partdiff (g,y,i)) . <*1*>);

      correctness

      proof

        

         A2: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

        consider g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) such that

         A3: f = g and

         A4: x = y and g is_partial_differentiable_in (y,i) by A1;

        the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

        then ( partdiff (g,y,i)) is Function of ( REAL 1), ( REAL n) by A2, LOPBAN_1:def 9;

        then (( partdiff (g,y,i)) . <*jj*>) is Element of ( REAL n) by FINSEQ_2: 98, FUNCT_2: 5;

        hence thesis by A3, A4;

      end;

    end

    theorem :: PDIFF_1:16

    for m,n be non zero Nat, F be PartFunc of ( REAL-NS m), ( REAL-NS n), G be PartFunc of ( REAL m), ( REAL n), x be Point of ( REAL-NS m), y be Element of ( REAL m) st F = G & x = y holds F is_partial_differentiable_in (x,i) iff G is_partial_differentiable_in (y,i);

    theorem :: PDIFF_1:17

    

     Th17: for m,n be non zero Nat, F be PartFunc of ( REAL-NS m), ( REAL-NS n), G be PartFunc of ( REAL m), ( REAL n), x be Point of ( REAL-NS m), y be Element of ( REAL m) st F = G & x = y & F is_partial_differentiable_in (x,i) holds (( partdiff (F,x,i)) . <*1*>) = ( partdiff (G,y,i))

    proof

      let m,n be non zero Nat, F be PartFunc of ( REAL-NS m), ( REAL-NS n), G be PartFunc of ( REAL m), ( REAL n), x be Point of ( REAL-NS m), y be Element of ( REAL m);

      assume that

       A1: F = G and

       A2: x = y and

       A3: F is_partial_differentiable_in (x,i);

      

       A4: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

      the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then ( partdiff (F,x,i)) is Function of ( REAL 1), ( REAL n) by A4, LOPBAN_1:def 9;

      then

       A5: (( partdiff (F,x,i)) . <*jj*>) is Element of ( REAL n) by FINSEQ_2: 98, FUNCT_2: 5;

      G is_partial_differentiable_in (y,i) by A1, A2, A3;

      hence thesis by A1, A2, A5, Def14;

    end;

    theorem :: PDIFF_1:18

    for g1 be PartFunc of ( REAL n), ( REAL 1) holds g1 = ( <>* g) implies (g1 is_partial_differentiable_in (y,i) iff g is_partial_differentiable_in (y,i))

    proof

      let g1 be PartFunc of ( REAL n), ( REAL 1);

      assume

       A1: g1 = ( <>* g);

      reconsider y9 = y as Point of ( REAL-NS n) by REAL_NS1:def 4;

      the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider h = g1 as PartFunc of ( REAL-NS n), ( REAL-NS 1) by REAL_NS1:def 4;

      h is_partial_differentiable_in (y9,i) iff g1 is_partial_differentiable_in (y,i);

      hence thesis by A1, Th14;

    end;

    theorem :: PDIFF_1:19

    for g1 be PartFunc of ( REAL n), ( REAL 1) st g1 = ( <>* g) & g1 is_partial_differentiable_in (y,i) holds ( partdiff (g1,y,i)) = <*( partdiff (g,y,i))*>

    proof

      let g1 be PartFunc of ( REAL n), ( REAL 1);

      assume that

       A1: g1 = ( <>* g) and

       A2: g1 is_partial_differentiable_in (y,i);

      reconsider y9 = y as Point of ( REAL-NS n) by REAL_NS1:def 4;

      the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider h = g1 as PartFunc of ( REAL-NS n), ( REAL-NS 1) by REAL_NS1:def 4;

      

       A3: h is_partial_differentiable_in (y9,i) by A2;

      then (( partdiff (h,y9,i)) . <*1*>) = ( partdiff (g1,y,i)) by Th17;

      hence thesis by A1, A3, Th15;

    end;

    begin

    reserve X for set;

    reserve r for Real;

    reserve f,f1,f2 for PartFunc of ( REAL-NS m), ( REAL-NS n);

    reserve g,g1,g2 for PartFunc of ( REAL n), REAL ;

    reserve h for PartFunc of ( REAL m), ( REAL n);

    reserve x for Point of ( REAL-NS m);

    reserve y for Element of ( REAL n);

    reserve z for Element of ( REAL m);

    definition

      let m,n be non zero Nat;

      let i,j be Nat;

      let f be PartFunc of ( REAL-NS m), ( REAL-NS n);

      let x be Point of ( REAL-NS m);

      :: PDIFF_1:def15

      pred f is_partial_differentiable_in x,i,j means ((( Proj (j,n)) * f) * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x);

    end

    definition

      let m,n be non zero Nat;

      let i,j be Nat;

      let f be PartFunc of ( REAL-NS m), ( REAL-NS n);

      let x be Point of ( REAL-NS m);

      :: PDIFF_1:def16

      func partdiff (f,x,i,j) -> Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),( REAL-NS 1))) equals ( diff (((( Proj (j,n)) * f) * ( reproj (i,x))),(( Proj (i,m)) . x)));

      correctness ;

    end

    definition

      let m,n be non zero Nat;

      let i,j be Nat;

      let h be PartFunc of ( REAL m), ( REAL n);

      let z be Element of ( REAL m);

      :: PDIFF_1:def17

      pred h is_partial_differentiable_in z,i,j means ((( proj (j,n)) * h) * ( reproj (i,z))) is_differentiable_in (( proj (i,m)) . z);

    end

    definition

      let m,n be non zero Nat;

      let i,j be Nat;

      let h be PartFunc of ( REAL m), ( REAL n);

      let z be Element of ( REAL m);

      :: PDIFF_1:def18

      func partdiff (h,z,i,j) -> Real equals ( diff (((( proj (j,n)) * h) * ( reproj (i,z))),(( proj (i,m)) . z)));

      correctness ;

    end

    theorem :: PDIFF_1:20

    for m,n be non zero Nat, F be PartFunc of ( REAL-NS m), ( REAL-NS n), G be PartFunc of ( REAL m), ( REAL n), x be Point of ( REAL-NS m), y be Element of ( REAL m) st F = G & x = y holds F is_differentiable_in x iff G is_differentiable_in y;

    theorem :: PDIFF_1:21

    for m,n be non zero Nat, F be PartFunc of ( REAL-NS m), ( REAL-NS n), G be PartFunc of ( REAL m), ( REAL n), x be Point of ( REAL-NS m), y be Element of ( REAL m) st F = G & x = y & F is_differentiable_in x holds ( diff (F,x)) = ( diff (G,y))

    proof

      let m,n be non zero Nat, F be PartFunc of ( REAL-NS m), ( REAL-NS n), G be PartFunc of ( REAL m), ( REAL n), x be Point of ( REAL-NS m), y be Element of ( REAL m);

      assume that

       A1: F = G and

       A2: x = y and

       A3: F is_differentiable_in x;

      

       A4: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

      the carrier of ( REAL-NS m) = ( REAL m) by REAL_NS1:def 4;

      then

       A5: ( diff (F,x)) is Function of ( REAL m), ( REAL n) by A4, LOPBAN_1:def 9;

      G is_differentiable_in y by A1, A2, A3;

      hence thesis by A1, A2, A5, Def8;

    end;

    theorem :: PDIFF_1:22

    

     Th22: f = h & x = z implies ((( Proj (j,n)) * f) * ( reproj (i,x))) = ( <>* ((( proj (j,n)) * h) * ( reproj (i,z))))

    proof

      reconsider h1 = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL 1) by Th2;

      assume that

       A1: f = h and

       A2: x = z;

      ( <>* ((( proj (j,n)) * h) * ( reproj (i,z)))) = ((h1 * (( proj (j,n)) * (h * ( reproj (i,z))))) * ( proj (1,1))) by RELAT_1: 36

      .= (((h1 * ( proj (j,n))) * (h * ( reproj (i,z)))) * ( proj (1,1))) by RELAT_1: 36

      .= ((h1 * ( proj (j,n))) * ((h * ( reproj (i,z))) * ( proj (1,1)))) by RELAT_1: 36

      .= ((h1 * ( proj (j,n))) * (h * (( reproj (i,z)) * ( proj (1,1))))) by RELAT_1: 36

      .= (( Proj (j,n)) * (h * (( reproj (i,z)) * ( proj (1,1))))) by Th11

      .= (( Proj (j,n)) * (h * ( reproj (i,x)))) by A2, Th12;

      hence thesis by A1, RELAT_1: 36;

    end;

    theorem :: PDIFF_1:23

    f = h & x = z implies (f is_partial_differentiable_in (x,i,j) iff h is_partial_differentiable_in (z,i,j))

    proof

      assume that

       A1: f = h and

       A2: x = z;

      

       A3: (( Proj (i,m)) . x) = <*(( proj (i,m)) . z)*> by A2, Def4;

      ((( Proj (j,n)) * f) * ( reproj (i,x))) = ( <>* ((( proj (j,n)) * h) * ( reproj (i,z)))) by A1, A2, Th22;

      hence thesis by A3, Th7, Th8;

    end;

    theorem :: PDIFF_1:24

    f = h & x = z & f is_partial_differentiable_in (x,i,j) implies (( partdiff (f,x,i,j)) . <*1*>) = <*( partdiff (h,z,i,j))*>

    proof

      assume that

       A1: f = h and

       A2: x = z and

       A3: f is_partial_differentiable_in (x,i,j);

      

       A4: (( Proj (i,m)) . x) = <*(( proj (i,m)) . z)*> by A2, Def4;

      

       A5: ((( Proj (j,n)) * f) * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A3;

      ((( Proj (j,n)) * f) * ( reproj (i,x))) = ( <>* ((( proj (j,n)) * h) * ( reproj (i,z)))) by A1, A2, Th22;

      hence thesis by A4, A5, Th10;

    end;

    definition

      let m,n be non zero Nat;

      let i be Nat;

      let f be PartFunc of ( REAL-NS m), ( REAL-NS n);

      let X be set;

      :: PDIFF_1:def19

      pred f is_partial_differentiable_on X,i means X c= ( dom f) & for x be Point of ( REAL-NS m) st x in X holds (f | X) is_partial_differentiable_in (x,i);

    end

    theorem :: PDIFF_1:25

    

     Th25: f is_partial_differentiable_on (X,i) implies X is Subset of ( REAL-NS m) by XBOOLE_1: 1;

    definition

      let m,n be non zero Nat;

      let i be Nat;

      let f be PartFunc of ( REAL-NS m), ( REAL-NS n);

      let X;

      assume

       A1: f is_partial_differentiable_on (X,i);

      :: PDIFF_1:def20

      func f `partial| (X,i) -> PartFunc of ( REAL-NS m), ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),( REAL-NS n))) means ( dom it ) = X & for x be Point of ( REAL-NS m) st x in X holds (it /. x) = ( partdiff (f,x,i));

      existence

      proof

        deffunc F( Element of ( REAL-NS m)) = ( partdiff (f,$1,i));

        defpred P[ Element of ( REAL-NS m)] means $1 in X;

        consider F be PartFunc of ( REAL-NS m), ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),( REAL-NS n))) such that

         A2: (for x be Point of ( REAL-NS m) holds x in ( dom F) iff P[x]) & for x be Point of ( REAL-NS m) st x in ( dom F) holds (F . x) = F(x) from SEQ_1:sch 3;

        take F;

        now

          

           A3: X is Subset of ( REAL-NS m) by A1, Th25;

          let y be object;

          assume y in X;

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

        end;

        then

         A4: X c= ( dom F);

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

        then ( dom F) c= X;

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

        hereby

          let x be Point of ( REAL-NS m);

          assume x in X;

          then

           A5: x in ( dom F) by A2;

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

          hence (F /. x) = ( partdiff (f,x,i)) by A5, PARTFUN1:def 6;

        end;

      end;

      uniqueness

      proof

        let F,G be PartFunc of ( REAL-NS m), ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),( REAL-NS n)));

        assume that

         A6: ( dom F) = X and

         A7: for x be Point of ( REAL-NS m) st x in X holds (F /. x) = ( partdiff (f,x,i)) and

         A8: ( dom G) = X and

         A9: for x be Point of ( REAL-NS m) st x in X holds (G /. x) = ( partdiff (f,x,i));

        now

          let x be Point of ( REAL-NS m);

          assume

           A10: x in ( dom F);

          then (F /. x) = ( partdiff (f,x,i)) by A6, A7;

          hence (F /. x) = (G /. x) by A6, A9, A10;

        end;

        hence thesis by A6, A8, PARTFUN2: 1;

      end;

    end

    theorem :: PDIFF_1:26

    

     Th26: ((f1 + f2) * ( reproj (i,x))) = ((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x)))) & ((f1 - f2) * ( reproj (i,x))) = ((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x))))

    proof

      

       A1: ( dom ( reproj (i,x))) = the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

      

       A2: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 1;

      for s be Element of ( REAL-NS 1) holds s in ( dom ((f1 + f2) * ( reproj (i,x)))) iff s in ( dom ((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x)))))

      proof

        let s be Element of ( REAL-NS 1);

        s in ( dom ((f1 + f2) * ( reproj (i,x)))) iff (( reproj (i,x)) . s) in (( dom f1) /\ ( dom f2)) by A2, A1, FUNCT_1: 11;

        then s in ( dom ((f1 + f2) * ( reproj (i,x)))) iff (( reproj (i,x)) . s) in ( dom f1) & (( reproj (i,x)) . s) in ( dom f2) by XBOOLE_0:def 4;

        then s in ( dom ((f1 + f2) * ( reproj (i,x)))) iff s in ( dom (f1 * ( reproj (i,x)))) & s in ( dom (f2 * ( reproj (i,x)))) by A1, FUNCT_1: 11;

        then s in ( dom ((f1 + f2) * ( reproj (i,x)))) iff s in (( dom (f1 * ( reproj (i,x)))) /\ ( dom (f2 * ( reproj (i,x))))) by XBOOLE_0:def 4;

        hence thesis by VFUNCT_1:def 1;

      end;

      then for s be object holds s in ( dom ((f1 + f2) * ( reproj (i,x)))) iff s in ( dom ((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x)))));

      then

       A3: ( dom ((f1 + f2) * ( reproj (i,x)))) = ( dom ((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x))))) by TARSKI: 2;

      

       A4: for z be Element of ( REAL-NS 1) st z in ( dom ((f1 + f2) * ( reproj (i,x)))) holds (((f1 + f2) * ( reproj (i,x))) . z) = (((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x)))) . z)

      proof

        let z be Element of ( REAL-NS 1);

        assume

         A5: z in ( dom ((f1 + f2) * ( reproj (i,x))));

        then

         A6: (( reproj (i,x)) . z) in ( dom (f1 + f2)) by FUNCT_1: 11;

        

         A7: (( reproj (i,x)) . z) in (( dom f1) /\ ( dom f2)) by A2, A5, FUNCT_1: 11;

        then

         A8: (( reproj (i,x)) . z) in ( dom f1) by XBOOLE_0:def 4;

        then

         A9: z in ( dom (f1 * ( reproj (i,x)))) by A1, FUNCT_1: 11;

        

         A10: (( reproj (i,x)) . z) in ( dom f2) by A7, XBOOLE_0:def 4;

        then

         A11: z in ( dom (f2 * ( reproj (i,x)))) by A1, FUNCT_1: 11;

        

         A12: (f2 /. (( reproj (i,x)) . z)) = (f2 . (( reproj (i,x)) . z)) by A10, PARTFUN1:def 6

        .= ((f2 * ( reproj (i,x))) . z) by A11, FUNCT_1: 12

        .= ((f2 * ( reproj (i,x))) /. z) by A11, PARTFUN1:def 6;

        

         A13: (f1 /. (( reproj (i,x)) . z)) = (f1 . (( reproj (i,x)) . z)) by A8, PARTFUN1:def 6

        .= ((f1 * ( reproj (i,x))) . z) by A9, FUNCT_1: 12

        .= ((f1 * ( reproj (i,x))) /. z) by A9, PARTFUN1:def 6;

        (((f1 + f2) * ( reproj (i,x))) . z) = ((f1 + f2) . (( reproj (i,x)) . z)) by A5, FUNCT_1: 12

        .= ((f1 + f2) /. (( reproj (i,x)) . z)) by A6, PARTFUN1:def 6

        .= ((f1 /. (( reproj (i,x)) . z)) + (f2 /. (( reproj (i,x)) . z))) by A6, VFUNCT_1:def 1

        .= (((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x)))) /. z) by A3, A5, A13, A12, VFUNCT_1:def 1;

        hence thesis by A3, A5, PARTFUN1:def 6;

      end;

      

       A14: ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 2;

      for s be Element of ( REAL-NS 1) holds s in ( dom ((f1 - f2) * ( reproj (i,x)))) iff s in ( dom ((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x)))))

      proof

        let s be Element of ( REAL-NS 1);

        s in ( dom ((f1 - f2) * ( reproj (i,x)))) iff (( reproj (i,x)) . s) in (( dom f1) /\ ( dom f2)) by A14, A1, FUNCT_1: 11;

        then s in ( dom ((f1 - f2) * ( reproj (i,x)))) iff (( reproj (i,x)) . s) in ( dom f1) & (( reproj (i,x)) . s) in ( dom f2) by XBOOLE_0:def 4;

        then s in ( dom ((f1 - f2) * ( reproj (i,x)))) iff s in ( dom (f1 * ( reproj (i,x)))) & s in ( dom (f2 * ( reproj (i,x)))) by A1, FUNCT_1: 11;

        then s in ( dom ((f1 - f2) * ( reproj (i,x)))) iff s in (( dom (f1 * ( reproj (i,x)))) /\ ( dom (f2 * ( reproj (i,x))))) by XBOOLE_0:def 4;

        hence thesis by VFUNCT_1:def 2;

      end;

      then for s be object holds s in ( dom ((f1 - f2) * ( reproj (i,x)))) iff s in ( dom ((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x)))));

      then

       A15: ( dom ((f1 - f2) * ( reproj (i,x)))) = ( dom ((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x))))) by TARSKI: 2;

      for z be Element of ( REAL-NS 1) st z in ( dom ((f1 - f2) * ( reproj (i,x)))) holds (((f1 - f2) * ( reproj (i,x))) . z) = (((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x)))) . z)

      proof

        let z be Element of ( REAL-NS 1);

        assume

         A16: z in ( dom ((f1 - f2) * ( reproj (i,x))));

        then

         A17: (( reproj (i,x)) . z) in ( dom (f1 - f2)) by FUNCT_1: 11;

        

         A18: (( reproj (i,x)) . z) in (( dom f1) /\ ( dom f2)) by A14, A16, FUNCT_1: 11;

        then

         A19: (( reproj (i,x)) . z) in ( dom f1) by XBOOLE_0:def 4;

        then

         A20: z in ( dom (f1 * ( reproj (i,x)))) by A1, FUNCT_1: 11;

        

         A21: (( reproj (i,x)) . z) in ( dom f2) by A18, XBOOLE_0:def 4;

        then

         A22: z in ( dom (f2 * ( reproj (i,x)))) by A1, FUNCT_1: 11;

        

         A23: (f2 /. (( reproj (i,x)) . z)) = (f2 . (( reproj (i,x)) . z)) by A21, PARTFUN1:def 6

        .= ((f2 * ( reproj (i,x))) . z) by A22, FUNCT_1: 12

        .= ((f2 * ( reproj (i,x))) /. z) by A22, PARTFUN1:def 6;

        

         A24: (f1 /. (( reproj (i,x)) . z)) = (f1 . (( reproj (i,x)) . z)) by A19, PARTFUN1:def 6

        .= ((f1 * ( reproj (i,x))) . z) by A20, FUNCT_1: 12

        .= ((f1 * ( reproj (i,x))) /. z) by A20, PARTFUN1:def 6;

        

        thus (((f1 - f2) * ( reproj (i,x))) . z) = ((f1 - f2) . (( reproj (i,x)) . z)) by A16, FUNCT_1: 12

        .= ((f1 - f2) /. (( reproj (i,x)) . z)) by A17, PARTFUN1:def 6

        .= ((f1 /. (( reproj (i,x)) . z)) - (f2 /. (( reproj (i,x)) . z))) by A17, VFUNCT_1:def 2

        .= (((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x)))) /. z) by A15, A16, A24, A23, VFUNCT_1:def 2

        .= (((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x)))) . z) by A15, A16, PARTFUN1:def 6;

      end;

      hence thesis by A3, A15, A4, PARTFUN1: 5;

    end;

    theorem :: PDIFF_1:27

    

     Th27: (r (#) (f * ( reproj (i,x)))) = ((r (#) f) * ( reproj (i,x)))

    proof

      

       A1: ( dom (r (#) f)) = ( dom f) by VFUNCT_1:def 4;

      

       A2: ( dom (r (#) (f * ( reproj (i,x))))) = ( dom (f * ( reproj (i,x)))) by VFUNCT_1:def 4;

      

       A3: ( dom ( reproj (i,x))) = the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

      for s be Element of ( REAL-NS 1) holds s in ( dom ((r (#) f) * ( reproj (i,x)))) iff s in ( dom (f * ( reproj (i,x))))

      proof

        let s be Element of ( REAL-NS 1);

        s in ( dom ((r (#) f) * ( reproj (i,x)))) iff (( reproj (i,x)) . s) in ( dom (r (#) f)) by A3, FUNCT_1: 11;

        hence thesis by A1, A3, FUNCT_1: 11;

      end;

      then for s be object holds s in ( dom (r (#) (f * ( reproj (i,x))))) iff s in ( dom ((r (#) f) * ( reproj (i,x)))) by A2;

      then

       A4: ( dom (r (#) (f * ( reproj (i,x))))) = ( dom ((r (#) f) * ( reproj (i,x)))) by TARSKI: 2;

      

       A5: for s be Element of ( REAL-NS 1) holds s in ( dom ((r (#) f) * ( reproj (i,x)))) iff (( reproj (i,x)) . s) in ( dom (r (#) f))

      proof

        let s be Element of ( REAL-NS 1);

        ( dom ( reproj (i,x))) = the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

        hence thesis by FUNCT_1: 11;

      end;

      for z be Element of ( REAL-NS 1) st z in ( dom (r (#) (f * ( reproj (i,x))))) holds ((r (#) (f * ( reproj (i,x)))) . z) = (((r (#) f) * ( reproj (i,x))) . z)

      proof

        let z be Element of ( REAL-NS 1);

        assume

         A6: z in ( dom (r (#) (f * ( reproj (i,x)))));

        then

         A7: z in ( dom (f * ( reproj (i,x)))) by VFUNCT_1:def 4;

        

         A8: (( reproj (i,x)) . z) in ( dom f) by A1, A5, A4, A6;

        

        then

         A9: (f /. (( reproj (i,x)) . z)) = (f . (( reproj (i,x)) . z)) by PARTFUN1:def 6

        .= ((f * ( reproj (i,x))) . z) by A7, FUNCT_1: 12

        .= ((f * ( reproj (i,x))) /. z) by A7, PARTFUN1:def 6;

        

         A10: ((r (#) (f * ( reproj (i,x)))) . z) = ((r (#) (f * ( reproj (i,x)))) /. z) by A6, PARTFUN1:def 6

        .= (r * (f /. (( reproj (i,x)) . z))) by A6, A9, VFUNCT_1:def 4;

        (((r (#) f) * ( reproj (i,x))) . z) = ((r (#) f) . (( reproj (i,x)) . z)) by A4, A6, FUNCT_1: 12

        .= ((r (#) f) /. (( reproj (i,x)) . z)) by A1, A8, PARTFUN1:def 6

        .= (r * (f /. (( reproj (i,x)) . z))) by A1, A8, VFUNCT_1:def 4;

        hence thesis by A10;

      end;

      hence thesis by A4, PARTFUN1: 5;

    end;

    theorem :: PDIFF_1:28

    

     Th28: f1 is_partial_differentiable_in (x,i) & f2 is_partial_differentiable_in (x,i) implies (f1 + f2) is_partial_differentiable_in (x,i) & ( partdiff ((f1 + f2),x,i)) = (( partdiff (f1,x,i)) + ( partdiff (f2,x,i)))

    proof

      assume that

       A1: f1 is_partial_differentiable_in (x,i) and

       A2: f2 is_partial_differentiable_in (x,i);

      

       A3: (f1 * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A1;

      

       A4: (f2 * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A2;

      ((f1 + f2) * ( reproj (i,x))) = ((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x)))) by Th26;

      then ((f1 + f2) * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A3, A4, NDIFF_1: 35;

      hence (f1 + f2) is_partial_differentiable_in (x,i);

      ( diff (((f1 * ( reproj (i,x))) + (f2 * ( reproj (i,x)))),(( Proj (i,m)) . x))) = ( partdiff ((f1 + f2),x,i)) by Th26;

      hence thesis by A3, A4, NDIFF_1: 35;

    end;

    theorem :: PDIFF_1:29

    g1 is_partial_differentiable_in (y,i) & g2 is_partial_differentiable_in (y,i) implies (g1 + g2) is_partial_differentiable_in (y,i) & ( partdiff ((g1 + g2),y,i)) = (( partdiff (g1,y,i)) + ( partdiff (g2,y,i)))

    proof

      assume that

       A1: g1 is_partial_differentiable_in (y,i) and

       A2: g2 is_partial_differentiable_in (y,i);

      reconsider x = y as Point of ( REAL-NS n) by REAL_NS1:def 4;

      

       A3: the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider f1 = ( <>* g1), f2 = ( <>* g2) as PartFunc of ( REAL-NS n), ( REAL-NS 1) by REAL_NS1:def 4;

      reconsider One = <*jj*> as VECTOR of ( REAL-NS 1) by A3, FINSEQ_2: 98;

      

       A4: f1 is_partial_differentiable_in (x,i) by A1, Th14;

      then

       A5: (( partdiff (f1,x,i)) . One) = <*( partdiff (g1,y,i))*> by Th15;

      reconsider d2 = ( partdiff (g2,y,i)) as Element of REAL by XREAL_0:def 1;

      reconsider Pd2 = <*d2*> as Element of ( REAL 1) by FINSEQ_2: 98;

      reconsider d1 = ( partdiff (g1,y,i)) as Element of REAL by XREAL_0:def 1;

      reconsider Pd1 = <*d1*> as Element of ( REAL 1) by FINSEQ_2: 98;

      

       A6: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

      ( rng g2) c= ( dom W) by Th2;

      then

       A7: ( dom (W * g2)) = ( dom g2) by RELAT_1: 27;

      ( rng g1) c= ( dom W) by Th2;

      then

       A8: ( dom (W * g1)) = ( dom g1) by RELAT_1: 27;

      then ( dom (f1 + f2)) = (( dom g1) /\ ( dom g2)) by A7, VFUNCT_1:def 1;

      then

       A9: ( dom (f1 + f2)) = ( dom (g1 + g2)) by VALUED_1:def 1;

      

       A10: ( rng (g1 + g2)) c= ( dom W) by Th2;

      then

       A11: ( dom (W * (g1 + g2))) = ( dom (g1 + g2)) by RELAT_1: 27;

       A12:

      now

        let x be Element of ( REAL-NS n);

        assume

         A13: x in ( dom (f1 + f2));

        then ((f1 + f2) . x) = ((f1 + f2) /. x) by PARTFUN1:def 6;

        then

         A14: ((f1 + f2) . x) = ((f1 /. x) + (f2 /. x)) by A13, VFUNCT_1:def 1;

        

         A15: x in (( dom f1) /\ ( dom f2)) by A13, VFUNCT_1:def 1;

        then x in ( dom f1) by XBOOLE_0:def 4;

        then

         A16: (f1 /. x) = ((W * g1) . x) by PARTFUN1:def 6;

        x in ( dom f2) by A15, XBOOLE_0:def 4;

        then

         A17: (f2 /. x) = ((W * g2) . x) by PARTFUN1:def 6;

        x in ( dom g2) by A7, A15, XBOOLE_0:def 4;

        then

         A18: (f2 /. x) = (W . (g2 . x)) by A17, FUNCT_1: 13;

        x in ( dom g1) by A8, A15, XBOOLE_0:def 4;

        then

         A19: (f1 /. x) = (W . (g1 . x)) by A16, FUNCT_1: 13;

        (( <>* (g1 + g2)) . x) = (W . ((g1 + g2) . x)) by A9, A11, A13, FUNCT_1: 12;

        then (( <>* (g1 + g2)) . x) = (W . ((g1 . x) + (g2 . x))) by A9, A13, VALUED_1:def 1;

        hence ((f1 + f2) . x) = (( <>* (g1 + g2)) . x) by A14, A19, A18, Th2, Th3;

      end;

      

       A20: f2 is_partial_differentiable_in (x,i) by A2, Th14;

      then

       A21: (( partdiff (f2,x,i)) . One) = <*( partdiff (g2,y,i))*> by Th15;

      

       A22: (f1 + f2) is_partial_differentiable_in (x,i) by A4, A20, Th28;

      ( dom (f1 + f2)) = ( dom ( <>* (g1 + g2))) by A9, A10, RELAT_1: 27;

      then

       A23: (f1 + f2) = ( <>* (g1 + g2)) by A6, A3, A12, PARTFUN1: 5;

      

      then <*( partdiff ((g1 + g2),y,i))*> = (( partdiff ((f1 + f2),x,i)) . <*1*>) by A4, A20, Th15, Th28

      .= ((( partdiff (f1,x,i)) + ( partdiff (f2,x,i))) . <*1*>) by A4, A20, Th28

      .= ((( partdiff (f1,x,i)) . One) + (( partdiff (f2,x,i)) . One)) by LOPBAN_1: 35

      .= (Pd1 + Pd2) by A5, A21, REAL_NS1: 2

      .= <*(( partdiff (g1,y,i)) + ( partdiff (g2,y,i)))*> by RVSUM_1: 13;

      then ( partdiff ((g1 + g2),y,i)) = ( <*(( partdiff (g1,y,i)) + ( partdiff (g2,y,i)))*> . 1) by FINSEQ_1: 40;

      hence thesis by A23, A22, Th14, FINSEQ_1: 40;

    end;

    theorem :: PDIFF_1:30

    

     Th30: f1 is_partial_differentiable_in (x,i) & f2 is_partial_differentiable_in (x,i) implies (f1 - f2) is_partial_differentiable_in (x,i) & ( partdiff ((f1 - f2),x,i)) = (( partdiff (f1,x,i)) - ( partdiff (f2,x,i)))

    proof

      assume that

       A1: f1 is_partial_differentiable_in (x,i) and

       A2: f2 is_partial_differentiable_in (x,i);

      

       A3: (f1 * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A1;

      

       A4: (f2 * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A2;

      ((f1 - f2) * ( reproj (i,x))) = ((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x)))) by Th26;

      then ((f1 - f2) * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A3, A4, NDIFF_1: 36;

      hence (f1 - f2) is_partial_differentiable_in (x,i);

      ( diff (((f1 * ( reproj (i,x))) - (f2 * ( reproj (i,x)))),(( Proj (i,m)) . x))) = ( partdiff ((f1 - f2),x,i)) by Th26;

      hence thesis by A3, A4, NDIFF_1: 36;

    end;

    theorem :: PDIFF_1:31

    g1 is_partial_differentiable_in (y,i) & g2 is_partial_differentiable_in (y,i) implies (g1 - g2) is_partial_differentiable_in (y,i) & ( partdiff ((g1 - g2),y,i)) = (( partdiff (g1,y,i)) - ( partdiff (g2,y,i)))

    proof

      assume that

       A1: g1 is_partial_differentiable_in (y,i) and

       A2: g2 is_partial_differentiable_in (y,i);

      reconsider x = y as Point of ( REAL-NS n) by REAL_NS1:def 4;

      

       A3: the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider f1 = ( <>* g1), f2 = ( <>* g2) as PartFunc of ( REAL-NS n), ( REAL-NS 1) by REAL_NS1:def 4;

      reconsider One = <*jj*> as VECTOR of ( REAL-NS 1) by A3, FINSEQ_2: 98;

      

       A4: f1 is_partial_differentiable_in (x,i) by A1, Th14;

      then

       A5: (( partdiff (f1,x,i)) . One) = <*( partdiff (g1,y,i))*> by Th15;

      reconsider d2 = ( partdiff (g2,y,i)) as Element of REAL by XREAL_0:def 1;

      reconsider Pd2 = <*d2*> as Element of ( REAL 1) by FINSEQ_2: 98;

      reconsider d1 = ( partdiff (g1,y,i)) as Element of REAL by XREAL_0:def 1;

      reconsider Pd1 = <*d1*> as Element of ( REAL 1) by FINSEQ_2: 98;

      

       A6: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

      ( rng g2) c= ( dom W) by Th2;

      then

       A7: ( dom (W * g2)) = ( dom g2) by RELAT_1: 27;

      ( rng g1) c= ( dom W) by Th2;

      then

       A8: ( dom (W * g1)) = ( dom g1) by RELAT_1: 27;

      then ( dom (f1 - f2)) = (( dom g1) /\ ( dom g2)) by A7, VFUNCT_1:def 2;

      then

       A9: ( dom (f1 - f2)) = ( dom (g1 - g2)) by VALUED_1: 12;

      

       A10: ( rng (g1 - g2)) c= ( dom W) by Th2;

      then

       A11: ( dom (W * (g1 - g2))) = ( dom (g1 - g2)) by RELAT_1: 27;

       A12:

      now

        let x be Element of ( REAL-NS n);

        assume

         A13: x in ( dom (f1 - f2));

        then ((f1 - f2) . x) = ((f1 - f2) /. x) by PARTFUN1:def 6;

        then

         A14: ((f1 - f2) . x) = ((f1 /. x) - (f2 /. x)) by A13, VFUNCT_1:def 2;

        

         A15: x in (( dom f1) /\ ( dom f2)) by A13, VFUNCT_1:def 2;

        then x in ( dom f1) by XBOOLE_0:def 4;

        then

         A16: (f1 /. x) = ((W * g1) . x) by PARTFUN1:def 6;

        x in ( dom f2) by A15, XBOOLE_0:def 4;

        then

         A17: (f2 /. x) = ((W * g2) . x) by PARTFUN1:def 6;

        x in ( dom g2) by A7, A15, XBOOLE_0:def 4;

        then

         A18: (f2 /. x) = (W . (g2 . x)) by A17, FUNCT_1: 13;

        x in ( dom g1) by A8, A15, XBOOLE_0:def 4;

        then

         A19: (f1 /. x) = (W . (g1 . x)) by A16, FUNCT_1: 13;

        (( <>* (g1 - g2)) . x) = (W . ((g1 - g2) . x)) by A9, A11, A13, FUNCT_1: 12;

        then (( <>* (g1 - g2)) . x) = (W . ((g1 . x) - (g2 . x))) by A9, A13, VALUED_1: 13;

        hence ((f1 - f2) . x) = (( <>* (g1 - g2)) . x) by A14, A19, A18, Th2, Th3;

      end;

      

       A20: f2 is_partial_differentiable_in (x,i) by A2, Th14;

      then

       A21: (( partdiff (f2,x,i)) . One) = <*( partdiff (g2,y,i))*> by Th15;

      

       A22: (f1 - f2) is_partial_differentiable_in (x,i) by A4, A20, Th30;

      ( dom (f1 - f2)) = ( dom ( <>* (g1 - g2))) by A9, A10, RELAT_1: 27;

      then

       A23: (f1 - f2) = ( <>* (g1 - g2)) by A6, A3, A12, PARTFUN1: 5;

      

      then <*( partdiff ((g1 - g2),y,i))*> = (( partdiff ((f1 - f2),x,i)) . <*1*>) by A4, A20, Th15, Th30

      .= ((( partdiff (f1,x,i)) - ( partdiff (f2,x,i))) . <*1*>) by A4, A20, Th30

      .= ((( partdiff (f1,x,i)) . One) - (( partdiff (f2,x,i)) . One)) by LOPBAN_1: 40

      .= (Pd1 - Pd2) by A5, A21, REAL_NS1: 5

      .= <*(( partdiff (g1,y,i)) - ( partdiff (g2,y,i)))*> by RVSUM_1: 29;

      then ( partdiff ((g1 - g2),y,i)) = ( <*(( partdiff (g1,y,i)) - ( partdiff (g2,y,i)))*> . 1) by FINSEQ_1: 40;

      hence thesis by A23, A22, Th14, FINSEQ_1: 40;

    end;

    theorem :: PDIFF_1:32

    

     Th32: f is_partial_differentiable_in (x,i) implies (r (#) f) is_partial_differentiable_in (x,i) & ( partdiff ((r (#) f),x,i)) = (r * ( partdiff (f,x,i)))

    proof

      assume f is_partial_differentiable_in (x,i);

      then

       A1: (f * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x);

      (r (#) (f * ( reproj (i,x)))) = ((r (#) f) * ( reproj (i,x))) by Th27;

      then ((r (#) f) * ( reproj (i,x))) is_differentiable_in (( Proj (i,m)) . x) by A1, NDIFF_1: 37;

      hence (r (#) f) is_partial_differentiable_in (x,i);

      ( diff ((r (#) (f * ( reproj (i,x)))),(( Proj (i,m)) . x))) = ( partdiff ((r (#) f),x,i)) by Th27;

      hence thesis by A1, NDIFF_1: 37;

    end;

    theorem :: PDIFF_1:33

    g is_partial_differentiable_in (y,i) implies (r (#) g) is_partial_differentiable_in (y,i) & ( partdiff ((r (#) g),y,i)) = (r * ( partdiff (g,y,i)))

    proof

      

       A1: the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

      

       A2: ( rng g) c= ( dom W) by Th2;

      then

       A3: ( dom (W * g)) = ( dom g) by RELAT_1: 27;

      reconsider d = ( partdiff (g,y,i)) as Element of REAL by XREAL_0:def 1;

      reconsider Pd = <*d*> as Element of ( REAL 1) by FINSEQ_2: 98;

      reconsider x = y as Point of ( REAL-NS n) by REAL_NS1:def 4;

      

       A4: the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider f = ( <>* g) as PartFunc of ( REAL-NS n), ( REAL-NS 1) by REAL_NS1:def 4;

      reconsider One = <*jj*> as VECTOR of ( REAL-NS 1) by A4, FINSEQ_2: 98;

      assume g is_partial_differentiable_in (y,i);

      then

       A5: f is_partial_differentiable_in (x,i) by Th14;

      then

       A6: (r (#) f) is_partial_differentiable_in (x,i) by Th32;

      ( dom (r (#) f)) = ( dom (W * g)) by VFUNCT_1:def 4;

      then ( dom (r (#) f)) = ( dom g) by A2, RELAT_1: 27;

      then

       A7: ( dom (r (#) f)) = ( dom (r (#) g)) by VALUED_1:def 5;

      

       A8: ( rng (r (#) g)) c= ( dom W) by Th2;

      then

       A9: ( dom (W * (r (#) g))) = ( dom (r (#) g)) by RELAT_1: 27;

       A10:

      now

        let x be Element of ( REAL-NS n);

        consider I be Function of REAL , ( REAL 1) such that I is bijective and

         A11: W = I by Th2;

        assume

         A12: x in ( dom (r (#) f));

        then

         A13: (( <>* (r (#) g)) . x) = (W . ((r (#) g) . x)) by A7, A9, FUNCT_1: 12;

        ((r (#) f) . x) = ((r (#) f) /. x) by A12, PARTFUN1:def 6;

        then

         A14: ((r (#) f) . x) = (r * (f /. x)) by A12, VFUNCT_1:def 4;

        

         A15: x in ( dom g) by A3, A12, VFUNCT_1:def 4;

        then

         A16: x in ( dom (r (#) g)) by VALUED_1:def 5;

        x in ( dom f) by A12, VFUNCT_1:def 4;

        then (f /. x) = ((W * g) . x) by PARTFUN1:def 6;

        then (f /. x) = (W . (g . x)) by A15, FUNCT_1: 13;

        then (r * (f /. x)) = (I . (r * (g . x))) by A11, Th3;

        hence ((r (#) f) . x) = (( <>* (r (#) g)) . x) by A16, A14, A13, A11, VALUED_1:def 5;

      end;

      

       A17: (( partdiff (f,x,i)) . One) = <*( partdiff (g,y,i))*> by A5, Th15;

      ( dom (r (#) f)) = ( dom ( <>* (r (#) g))) by A7, A8, RELAT_1: 27;

      then

       A18: (r (#) f) = ( <>* (r (#) g)) by A1, A4, A10, PARTFUN1: 5;

      

      then <*( partdiff ((r (#) g),y,i))*> = (( partdiff ((r (#) f),x,i)) . <*1*>) by A5, Th15, Th32

      .= ((r * ( partdiff (f,x,i))) . <*1*>) by A5, Th32

      .= (r * (( partdiff (f,x,i)) . One)) by LOPBAN_1: 36

      .= (r * Pd) by A17, REAL_NS1: 3

      .= <*(r * ( partdiff (g,y,i)))*> by RVSUM_1: 47;

      then ( partdiff ((r (#) g),y,i)) = ( <*(r * ( partdiff (g,y,i)))*> . 1) by FINSEQ_1: 40;

      hence thesis by A18, A6, Th14, FINSEQ_1: 40;

    end;