pdiff_6.miz



    begin

    reserve i,n,m for Nat;

    theorem :: PDIFF_6:1

    

     Th1: for f be set holds f is PartFunc of ( REAL m), ( REAL n) iff f is PartFunc of ( REAL-NS m), ( REAL-NS n)

    proof

      let f be set;

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

      hence thesis;

    end;

    theorem :: PDIFF_6:2

    

     Th2: for n,m be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n), x be Element of ( REAL m), y be Point of ( REAL-NS m) st f = g & x = y holds f is_differentiable_in x iff g is_differentiable_in y

    proof

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

      assume

       A1: f = g & x = y;

      hereby

        assume f is_differentiable_in x;

        then 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 by PDIFF_1:def 7;

        hence g is_differentiable_in y by A1;

      end;

      assume g is_differentiable_in y;

      hence f is_differentiable_in x by A1, PDIFF_1:def 7;

    end;

    theorem :: PDIFF_6:3

    

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

    proof

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

      assume

       A1: f = g & x = y & f is_differentiable_in x;

      then ex g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st f = g & x = y & ( diff (f,x)) = ( diff (g,y)) by PDIFF_1:def 8;

      hence thesis by A1;

    end;

    theorem :: PDIFF_6:4

    

     Th4: for f1,f2 be PartFunc of ( REAL m), ( REAL n), g1,g2 be PartFunc of ( REAL-NS m), ( REAL-NS n) st f1 = g1 & f2 = g2 holds (f1 + f2) = (g1 + g2)

    proof

      let f1,f2 be PartFunc of ( REAL m), ( REAL n), g1,g2 be PartFunc of ( REAL-NS m), ( REAL-NS n);

      assume

       A1: f1 = g1 & f2 = g2;

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

      then

      reconsider g12 = (g1 + g2) as PartFunc of ( REAL m), ( REAL n);

      

       A2: (( dom f1) /\ ( dom f2)) = ( dom g12) by A1, VFUNCT_1:def 1;

      

       A3: (f1 <++> f2) = (f1 + f2) by INTEGR15:def 9;

      for c be object st c in ( dom g12) holds ((g1 + g2) . c) = ((f1 . c) + (f2 . c))

      proof

        let c be object;

        assume

         A4: c in ( dom g12);

        then

         A5: c in ( dom (g1 + g2));

        c in ( dom f1) & c in ( dom f2) by A2, A4, XBOOLE_0:def 4;

        then

         A6: (f1 /. c) = (f1 . c) & (f2 /. c) = (f2 . c) by PARTFUN1:def 6;

        

         A7: (f1 /. c) = (g1 /. c) & (f2 /. c) = (g2 /. c) by A1, REAL_NS1:def 4;

        (g12 . c) = ((g1 + g2) /. c) by A4, PARTFUN1:def 6

        .= ((g1 /. c) + (g2 /. c)) by A5, VFUNCT_1:def 1;

        hence thesis by A6, A7, REAL_NS1: 2;

      end;

      hence thesis by A2, A3, VALUED_2:def 45;

    end;

    theorem :: PDIFF_6:5

    

     Th5: for f1,f2 be PartFunc of ( REAL m), ( REAL n), g1,g2 be PartFunc of ( REAL-NS m), ( REAL-NS n) st f1 = g1 & f2 = g2 holds (f1 - f2) = (g1 - g2)

    proof

      let f1,f2 be PartFunc of ( REAL m), ( REAL n), g1,g2 be PartFunc of ( REAL-NS m), ( REAL-NS n);

      assume

       A1: f1 = g1 & f2 = g2;

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

      then

      reconsider g12 = (g1 - g2) as PartFunc of ( REAL m), ( REAL n);

      

       A2: (( dom f1) /\ ( dom f2)) = ( dom g12) by A1, VFUNCT_1:def 2;

      

       A3: (f1 <--> f2) = (f1 - f2) by INTEGR15:def 10;

      for c be object st c in ( dom g12) holds ((g1 - g2) . c) = ((f1 . c) - (f2 . c))

      proof

        let c be object;

        assume

         A4: c in ( dom g12);

        then

         A5: c in ( dom (g1 - g2));

        c in ( dom f1) & c in ( dom f2) by A2, A4, XBOOLE_0:def 4;

        then

         A6: (f1 /. c) = (f1 . c) & (f2 /. c) = (f2 . c) by PARTFUN1:def 6;

        

         A7: (f1 /. c) = (g1 /. c) & (f2 /. c) = (g2 /. c) by A1, REAL_NS1:def 4;

        (g12 . c) = ((g1 - g2) /. c) by A4, PARTFUN1:def 6

        .= ((g1 /. c) - (g2 /. c)) by A5, VFUNCT_1:def 2;

        hence thesis by A6, A7, REAL_NS1: 5;

      end;

      hence thesis by A2, A3, VALUED_2:def 46;

    end;

    theorem :: PDIFF_6:6

    

     Th6: for f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n), a be Real st f = g holds (a (#) f) = (a (#) g)

    proof

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

      assume

       A1: f = g;

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

      then

      reconsider aG = (a (#) g) as PartFunc of ( REAL m), ( REAL n);

      

       A2: ( dom f) = ( dom aG) by A1, VFUNCT_1:def 4;

      

       A3: (a (#) f) = (f [#] a) by INTEGR15:def 11;

      for c be object st c in ( dom aG) holds (aG . c) = (a (#) (f . c))

      proof

        let c be object;

        assume

         A4: c in ( dom aG);

        then

         A5: c in ( dom (a (#) g));

        

         A6: (f /. c) = (g /. c) by A1, REAL_NS1:def 4;

        

         A7: (f /. c) = (f . c) by A2, A4, PARTFUN1:def 6;

        (aG . c) = ((a (#) g) /. c) by A4, PARTFUN1:def 6

        .= (a * (g /. c)) by A5, VFUNCT_1:def 4;

        hence (aG . c) = (a (#) (f . c)) by A6, A7, REAL_NS1: 3;

      end;

      hence thesis by A2, A3, VALUED_2:def 39;

    end;

    theorem :: PDIFF_6:7

    

     Th7: for f1,f2 be Function of ( REAL m), ( REAL n), g1,g2 be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))) st f1 = g1 & f2 = g2 holds (f1 + f2) = (g1 + g2)

    proof

      let f1,f2 be Function of ( REAL m), ( REAL n), g1,g2 be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n)));

      assume

       A1: f1 = g1 & f2 = g2;

      

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

      then

      reconsider g12 = (g1 + g2) as Function of ( REAL m), ( REAL n) by LOPBAN_1:def 9;

      g1 is LinearOperator of ( REAL-NS m), ( REAL-NS n) & g2 is LinearOperator of ( REAL-NS m), ( REAL-NS n) by LOPBAN_1:def 9;

      then ( dom g1) = ( REAL m) & ( dom g2) = ( REAL m) by A2, FUNCT_2:def 1;

      then

       A3: (( dom f1) /\ ( dom f2)) = ( dom g12) by A1, FUNCT_2:def 1;

      

       A4: (f1 <++> f2) = (f1 + f2) by INTEGR15:def 9;

      for c be object st c in ( dom g12) holds (g12 . c) = ((f1 . c) + (f2 . c))

      proof

        let c be object;

        assume

         A5: c in ( dom g12);

        then

        reconsider x = c as VECTOR of ( REAL-NS m) by REAL_NS1:def 4;

        reconsider c1 = c as Element of ( REAL m) by A5;

        (g12 . x) = ((g1 . x) + (g2 . x)) by LOPBAN_1: 35;

        

        hence (g12 . c) = ((f1 /. c1) + (f2 /. c1)) by A1, REAL_NS1: 2

        .= ((f1 . c) + (f2 . c));

      end;

      hence thesis by A3, A4, VALUED_2:def 45;

    end;

    theorem :: PDIFF_6:8

    

     Th8: for f1,f2 be Function of ( REAL m), ( REAL n), g1,g2 be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))) st f1 = g1 & f2 = g2 holds (f1 - f2) = (g1 - g2)

    proof

      let f1,f2 be Function of ( REAL m), ( REAL n), g1,g2 be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n)));

      assume

       A1: f1 = g1 & f2 = g2;

      

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

      then

      reconsider g12 = (g1 - g2) as Function of ( REAL m), ( REAL n) by LOPBAN_1:def 9;

      g1 is LinearOperator of ( REAL-NS m), ( REAL-NS n) & g2 is LinearOperator of ( REAL-NS m), ( REAL-NS n) by LOPBAN_1:def 9;

      then ( dom g1) = ( REAL m) & ( dom g2) = ( REAL m) by A2, FUNCT_2:def 1;

      then

       A3: (( dom f1) /\ ( dom f2)) = ( dom g12) by A1, FUNCT_2:def 1;

      

       A4: (f1 <--> f2) = (f1 - f2) by INTEGR15:def 10;

      for c be object st c in ( dom g12) holds (g12 . c) = ((f1 . c) - (f2 . c))

      proof

        let c be object;

        assume

         A5: c in ( dom g12);

        then

        reconsider x = c as VECTOR of ( REAL-NS m) by REAL_NS1:def 4;

        reconsider c1 = c as Element of ( REAL m) by A5;

        (g12 . x) = ((g1 . x) - (g2 . x)) by LOPBAN_1: 40;

        

        hence (g12 . c) = ((f1 /. c1) - (f2 /. c1)) by A1, REAL_NS1: 5

        .= ((f1 . c) - (f2 . c));

      end;

      hence thesis by A3, A4, VALUED_2:def 46;

    end;

    theorem :: PDIFF_6:9

    

     Th9: for f be Function of ( REAL m), ( REAL n), g be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))), r be Real st f = g holds (r (#) f) = (r * g)

    proof

      let f be Function of ( REAL m), ( REAL n), g be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))), r be Real;

      assume

       A1: f = g;

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

      then

      reconsider rG = (r * g) as Function of ( REAL m), ( REAL n) by LOPBAN_1:def 9;

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

      then

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

      

       A3: (r (#) f) = (f [#] r) by INTEGR15:def 11;

      for c be object st c in ( dom rG) holds (rG . c) = (r (#) (f . c))

      proof

        let c be object;

        assume

         A4: c in ( dom rG);

        then

        reconsider x = c as VECTOR of ( REAL-NS m) by REAL_NS1:def 4;

        reconsider c1 = c as Element of ( REAL m) by A4;

        (rG . x) = (r * (g . x)) by LOPBAN_1: 36;

        

        hence (rG . c) = (r * (f /. c1)) by A1, REAL_NS1: 3

        .= (r (#) (f . c));

      end;

      hence thesis by A2, A3, VALUED_2:def 39;

    end;

    theorem :: PDIFF_6:10

    

     Th10: for m,n be non zero Nat holds for f be PartFunc of ( REAL m), ( REAL n), x be Element of ( REAL m) st f is_differentiable_in x holds ( diff (f,x)) is Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n)))

    proof

      let m,n be non zero Nat;

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

      assume f is_differentiable_in x;

      then ex g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st f = g & x = y & ( diff (f,x)) = ( diff (g,y)) by PDIFF_1:def 8;

      hence thesis;

    end;

    definition

      let n,m be Nat;

      let IT be Function of ( REAL m), ( REAL n);

      :: PDIFF_6:def1

      attr IT is additive means

      : Def1: for x,y be Element of ( REAL m) holds (IT . (x + y)) = ((IT . x) + (IT . y));

      :: PDIFF_6:def2

      attr IT is homogeneous means

      : Def2: for x be Element of ( REAL m), r be Real holds (IT . (r * x)) = (r * (IT . x));

    end

    theorem :: PDIFF_6:11

    

     Th11: for IT be Function of ( REAL m), ( REAL n) st IT is additive holds (IT . ( 0* m)) = ( 0* n)

    proof

      let IT be Function of ( REAL m), ( REAL n);

      assume

       A1: IT is additive;

      (IT . ( 0* m)) = (IT . (( 0* m) + ( 0* m))) by RVSUM_1: 16;

      then (IT . ( 0* m)) = ((IT . ( 0* m)) + (IT . ( 0* m))) by A1;

      then ( 0* n) = (((IT . ( 0* m)) + (IT . ( 0* m))) - (IT . ( 0* m))) by RVSUM_1: 37;

      hence ( 0* n) = (IT . ( 0* m)) by RVSUM_1: 42;

    end;

    theorem :: PDIFF_6:12

    

     Th12: for f be Function of ( REAL m), ( REAL n), g be Function of ( REAL-NS m), ( REAL-NS n) st f = g holds f is additive iff g is additive

    proof

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

      assume

       A1: f = g;

      hereby

        assume

         A2: f is additive;

        now

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

          reconsider x1 = x, y1 = y as Element of ( REAL m) by REAL_NS1:def 4;

          (g . (x + y)) = (f . (x1 + y1)) by A1, REAL_NS1: 2

          .= ((f . x1) + (f . y1)) by A2;

          hence (g . (x + y)) = ((g . x) + (g . y)) by A1, REAL_NS1: 2;

        end;

        hence g is additive by VECTSP_1:def 20;

      end;

      assume

       A3: g is additive;

      now

        let x,y be Element of ( REAL m);

        reconsider x1 = x, y1 = y as Point of ( REAL-NS m) by REAL_NS1:def 4;

        (f . (x + y)) = (g . (x1 + y1)) by A1, REAL_NS1: 2

        .= ((g . x1) + (g . y1)) by A3, VECTSP_1:def 20;

        hence (f . (x + y)) = ((f . x) + (f . y)) by A1, REAL_NS1: 2;

      end;

      hence f is additive;

    end;

    theorem :: PDIFF_6:13

    

     Th13: for f be Function of ( REAL m), ( REAL n), g be Function of ( REAL-NS m), ( REAL-NS n) st f = g holds f is homogeneous iff g is homogeneous

    proof

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

      assume

       A1: f = g;

      hereby

        assume

         A2: f is homogeneous;

        now

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

          reconsider x1 = x as Element of ( REAL m) by REAL_NS1:def 4;

          (g . (r * x)) = (f . (r * x1)) by A1, REAL_NS1: 3

          .= (r * (f . x1)) by A2;

          hence (g . (r * x)) = (r * (g . x)) by A1, REAL_NS1: 3;

        end;

        hence g is homogeneous;

      end;

      assume

       A3: g is homogeneous;

      now

        let x be Element of ( REAL m), r be Real;

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

        (f . (r * x)) = (g . (r * x1)) by A1, REAL_NS1: 3

        .= (r * (g . x1)) by A3;

        hence (f . (r * x)) = (r * (f . x)) by A1, REAL_NS1: 3;

      end;

      hence f is homogeneous;

    end;

    registration

      let n,m be Nat;

      cluster (( REAL m) --> ( 0* n)) -> additive homogeneous;

      coherence

      proof

        let f be Function of ( REAL m), ( REAL n) such that

         A1: f = (( REAL m) --> ( 0* n));

        reconsider n1 = n as Nat;

        hereby

          let x,y be Element of ( REAL m);

          

           A2: ( 0. ( REAL-NS n1)) = ( 0* n) by REAL_NS1:def 4;

          (f . (x + y)) = ( 0* n) by A1, FUNCOP_1: 7

          .= ( 0. ( REAL-NS n1)) by REAL_NS1:def 4

          .= (( 0. ( REAL-NS n1)) + ( 0. ( REAL-NS n1))) by RLVECT_1: 4

          .= (( 0* n) + ( 0* n)) by A2, REAL_NS1: 2

          .= ((f . x) + ( 0* n)) by A1, FUNCOP_1: 7;

          hence (f . (x + y)) = ((f . x) + (f . y)) by A1, FUNCOP_1: 7;

        end;

        hereby

          let x be Element of ( REAL m), r be Real;

          

           A3: ( 0. ( REAL-NS n1)) = ( 0* n) by REAL_NS1:def 4;

          (f . (r * x)) = ( 0* n) by A1, FUNCOP_1: 7

          .= ( 0. ( REAL-NS n1)) by REAL_NS1:def 4

          .= (r * ( 0. ( REAL-NS n1))) by RLVECT_1: 10

          .= (r * ( 0* n)) by A3, REAL_NS1: 3;

          hence (f . (r * x)) = (r * (f . x)) by A1, FUNCOP_1: 7;

        end;

      end;

    end

    registration

      let n,m be Nat;

      cluster additive homogeneous for Function of ( REAL m), ( REAL n);

      existence

      proof

        take (( REAL m) --> ( 0* n));

        thus thesis;

      end;

    end

    definition

      let m,n be Nat;

      mode LinearOperator of m,n is additive homogeneous Function of ( REAL m), ( REAL n);

    end

    theorem :: PDIFF_6:14

    

     Th14: for f be set holds f is LinearOperator of m, n iff f is LinearOperator of ( REAL-NS m), ( REAL-NS n)

    proof

      let f be set;

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

      hence f is additive homogeneous Function of ( REAL m), ( REAL n) iff f is additive homogeneous Function of ( REAL-NS m), ( REAL-NS n) by Th12, Th13;

    end;

    definition

      let m,n be Nat, IT be Function of ( REAL m), ( REAL n);

      :: PDIFF_6:def3

      attr IT is Lipschitzian means

      : Def3: ex K be Real st 0 <= K & for x be Element of ( REAL m) holds |.(IT . x).| <= (K * |.x.|);

    end

    theorem :: PDIFF_6:15

    

     Th15: for xseq,yseq be FinSequence of ( REAL m) st ( len xseq) = (( len yseq) + 1) & (xseq | ( len yseq)) = yseq holds ex v be Element of ( REAL m) st v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum yseq) + v)

    proof

      let xseq,yseq be FinSequence of ( REAL m);

      assume

       A1: ( len xseq) = (( len yseq) + 1) & (xseq | ( len yseq)) = yseq;

      

       A2: ( len xseq) = ( len ( accum xseq)) & (xseq . 1) = (( accum xseq) . 1) & (for k be Nat st 1 <= k & k < ( len xseq) holds (( accum xseq) . (k + 1)) = ((( accum xseq) /. k) + (xseq /. (k + 1)))) by EUCLID_7:def 10;

      

       A3: ( Sum xseq) = (( accum xseq) . ( len xseq)) by A1, EUCLID_7:def 11;

      set g = ( accum xseq);

      set i = ( len yseq);

      per cases ;

        suppose

         A4: i = 0 ;

        then

        reconsider v = (xseq . ( len xseq)) as Element of ( REAL m) by A1, A3, EUCLID_7:def 10;

        take v;

        ( Sum yseq) = ( 0* m) by A4, EUCLID_7:def 11;

        hence v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum yseq) + v) by A1, A2, A3, A4, RVSUM_1: 16;

      end;

        suppose

         A5: i <> 0 ;

        

         A6: ( len yseq) = ( len ( accum yseq)) & (yseq . 1) = (( accum yseq) . 1) & (for k be Nat st 1 <= k & k < ( len yseq) holds (( accum yseq) . (k + 1)) = ((( accum yseq) /. k) + (yseq /. (k + 1)))) by EUCLID_7:def 10;

        

         A7: ( Sum yseq) = (( accum yseq) . i) by A5, EUCLID_7:def 11;

        set g0 = ( accum yseq);

        

         A8: i <= ( len g) by A1, A2, NAT_1: 11;

        then

         A9: ( len (g | i)) = i by FINSEQ_1: 59;

        

         A10: for k be Nat st 1 <= k & k <= ( len (g | i)) holds ((g | i) . k) = (g0 . k)

        proof

          defpred PP[ Nat] means 1 <= $1 & $1 <= ( len (g | i)) implies ((g | i) . $1) = (g0 . $1);

          

           A11: PP[ 0 ];

           A12:

          now

            let k be Nat;

            assume

             A13: PP[k];

            now

              assume

               A14: 1 <= (k + 1) & (k + 1) <= ( len (g | i));

              then

               A15: (k + 1) <= ( len yseq) by A8, FINSEQ_1: 59;

              then (k + 1) in ( Seg i) by A14;

              then

               A16: ((g | i) . (k + 1)) = (g . (k + 1)) & (xseq . (k + 1)) = ((xseq | ( Seg i)) . (k + 1)) by FUNCT_1: 49;

              

               A17: k < ( len yseq) by A15, NAT_1: 13;

              now

                assume

                 A18: k <> 0 ;

                then

                 A19: 1 <= k by NAT_1: 14;

                then

                 A20: k in ( Seg i) by A17;

                ( len yseq) <= ( len xseq) by A1, NAT_1: 12;

                then

                 A21: k < ( len xseq) by A17, XXREAL_0: 2;

                then (g /. k) = (g . k) by A2, A19, FINSEQ_4: 15;

                then (g /. k) = ((g | i) . k) by A20, FUNCT_1: 49;

                then

                 A22: (g /. k) = (g0 /. k) by A6, A17, A19, A13, A14, FINSEQ_4: 15, NAT_1: 13;

                (k + 1) <= ( len xseq) by A15, A1, NAT_1: 12;

                then (xseq /. (k + 1)) = (xseq . (k + 1)) by A14, FINSEQ_4: 15;

                then (xseq /. (k + 1)) = (yseq /. (k + 1)) by A1, A14, A9, A16, FINSEQ_4: 15;

                then ((g /. k) + (xseq /. (k + 1))) = (g0 . (k + 1)) by A6, A17, A18, A22, NAT_1: 14;

                hence ((g | i) . (k + 1)) = (g0 . (k + 1)) by A2, A16, A18, A21, NAT_1: 14;

              end;

              hence ((g | i) . (k + 1)) = (g0 . (k + 1)) by A1, A6, A16, EUCLID_7:def 10;

            end;

            hence PP[(k + 1)];

          end;

          thus for k be Nat holds PP[k] from NAT_1:sch 2( A11, A12);

        end;

        1 <= i by A5, NAT_1: 14;

        then i in ( Seg i);

        then

         A23: i in ( dom (g | i)) by A9, FINSEQ_1:def 3;

        then i in ( dom g) by RELAT_1: 57;

        then (g . i) = (g /. i) by PARTFUN1:def 6;

        then ((g | i) . i) = (g /. i) by A23, FUNCT_1: 47;

        then

         A24: (g0 . i) = (g /. i) by A6, A9, A10, FINSEQ_1: 14;

        ( dom xseq) = ( Seg (i + 1)) by A1, FINSEQ_1:def 3;

        then (xseq . ( len xseq)) in ( rng xseq) by A1, FINSEQ_1: 4, FUNCT_1: 3;

        then

        reconsider v = (xseq . ( len xseq)) as Element of ( REAL m);

        take v;

        thus v = (xseq . ( len xseq));

        

         A25: i < ( len xseq) by A1, NAT_1: 13;

        1 <= (i + 1) by NAT_1: 11;

        then ((g /. i) + (xseq /. (i + 1))) = (( Sum yseq) + v) by A7, A24, A1, FINSEQ_4: 15;

        hence ( Sum xseq) = (( Sum yseq) + v) by A1, A25, A2, A3, A5, NAT_1: 14;

      end;

    end;

    theorem :: PDIFF_6:16

    

     Th16: for f be LinearOperator of m, n, xseq be FinSequence of ( REAL m), yseq be FinSequence of ( REAL n) st ( len xseq) = ( len yseq) & (for i be Nat st i in ( dom xseq) holds (yseq . i) = (f . (xseq . i))) holds ( Sum yseq) = (f . ( Sum xseq))

    proof

      let f be LinearOperator of m, n;

      defpred P[ Nat] means for xseq be FinSequence of ( REAL m), yseq be FinSequence of ( REAL n) st $1 = ( len xseq) & ( len xseq) = ( len yseq) & for i be Nat st i in ( dom xseq) holds (yseq . i) = (f . (xseq . i)) holds ( Sum yseq) = (f . ( Sum xseq));

      

       A1: P[ 0 ]

      proof

        let xseq be FinSequence of ( REAL m), yseq be FinSequence of ( REAL n);

        assume 0 = ( len xseq) & ( len xseq) = ( len yseq) & for i be Nat st i in ( dom xseq) holds (yseq . i) = (f . (xseq . i));

        then ( Sum xseq) = ( 0* m) & ( Sum yseq) = ( 0* n) by EUCLID_7:def 11;

        hence thesis by Th11;

      end;

       A2:

      now

        let i be Nat;

        assume

         A3: P[i];

        now

          let xseq be FinSequence of ( REAL m), yseq be FinSequence of ( REAL n);

          assume

           A4: (i + 1) = ( len xseq) & ( len xseq) = ( len yseq) & for k be Nat st k in ( dom xseq) holds (yseq . k) = (f . (xseq . k));

          set xseq0 = (xseq | i), yseq0 = (yseq | i);

          

           A5: i = ( len xseq0) by A4, FINSEQ_1: 59, NAT_1: 11;

          then

           A6: ( len xseq0) = ( len yseq0) by A4, FINSEQ_1: 59, NAT_1: 11;

          for k be Nat st k in ( dom xseq0) holds (yseq0 . k) = (f . (xseq0 . k))

          proof

            let k be Nat;

            assume

             A7: k in ( dom xseq0);

            then

             A8: k in ( Seg i) by RELAT_1: 57;

            k in ( dom xseq) by A7, RELAT_1: 57;

            then

             A9: (yseq . k) = (f . (xseq . k)) by A4;

            (xseq . k) = (xseq0 . k) by A8, FUNCT_1: 49;

            hence (yseq0 . k) = (f . (xseq0 . k)) by A8, A9, FUNCT_1: 49;

          end;

          then

           A10: ( Sum yseq0) = (f . ( Sum xseq0)) by A5, A6, A3;

          consider v be Element of ( REAL m) such that

           A11: v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum xseq0) + v) by A4, A5, Th15;

          consider w be Element of ( REAL n) such that

           A12: w = (yseq . ( len yseq)) & ( Sum yseq) = (( Sum yseq0) + w) by A4, A5, A6, Th15;

          ( dom xseq) = ( Seg (i + 1)) by A4, FINSEQ_1:def 3;

          then w = (f . v) by A4, A12, A11, FINSEQ_1: 4;

          hence ( Sum yseq) = (f . ( Sum xseq)) by A10, A11, A12, Def1;

        end;

        hence P[(i + 1)];

      end;

      

       A13: for k be Nat holds P[k] from NAT_1:sch 2( A1, A2);

      let xseq be FinSequence of ( REAL m), yseq be FinSequence of ( REAL n);

      assume ( len xseq) = ( len yseq) & for i be Nat st i in ( dom xseq) holds (yseq . i) = (f . (xseq . i));

      hence ( Sum yseq) = (f . ( Sum xseq)) by A13;

    end;

    theorem :: PDIFF_6:17

    

     Th17: for xseq be FinSequence of ( REAL m), yseq be FinSequence of REAL st ( len xseq) = ( len yseq) & (for i be Nat st i in ( dom xseq) holds ex v be Element of ( REAL m) st v = (xseq . i) & (yseq . i) = |.v.|) holds |.( Sum xseq).| <= ( Sum yseq)

    proof

      defpred P[ Nat] means for xseq be FinSequence of ( REAL m), yseq be FinSequence of REAL st $1 = ( len xseq) & ( len xseq) = ( len yseq) & (for i be Nat st i in ( dom xseq) holds ex v be Element of ( REAL m) st v = (xseq . i) & (yseq . i) = |.v.|) holds |.( Sum xseq).| <= ( Sum yseq);

      

       A1: P[ 0 ]

      proof

        let xseq be FinSequence of ( REAL m), yseq be FinSequence of REAL ;

        assume 0 = ( len xseq) & ( len xseq) = ( len yseq) & (for i be Nat st i in ( dom xseq) holds ex v be Element of ( REAL m) st v = (xseq . i) & (yseq . i) = |.v.|);

        then ( Sum xseq) = ( 0* m) & ( <*> REAL ) = yseq by EUCLID_7:def 11;

        hence thesis by EUCLID: 7, RVSUM_1: 72;

      end;

       A2:

      now

        let i be Nat;

        assume

         A3: P[i];

        now

          let xseq be FinSequence of ( REAL m), yseq be FinSequence of REAL ;

          set xseq0 = (xseq | i), yseq0 = (yseq | i);

          assume

           A4: (i + 1) = ( len xseq) & ( len xseq) = ( len yseq) & (for i be Nat st i in ( dom xseq) holds ex v be Element of ( REAL m) st v = (xseq . i) & (yseq . i) = |.v.|);

          

           A5: for k be Nat st k in ( dom xseq0) holds ex v be Element of ( REAL m) st v = (xseq0 . k) & (yseq0 . k) = |.v.|

          proof

            let k be Nat;

            assume k in ( dom xseq0);

            then

             A6: k in ( Seg i) & k in ( dom xseq) by RELAT_1: 57;

            then

            consider v be Element of ( REAL m) such that

             A7: v = (xseq . k) & (yseq . k) = |.v.| by A4;

            take v;

            thus thesis by A6, A7, FUNCT_1: 49;

          end;

          ( dom xseq) = ( Seg (i + 1)) by A4, FINSEQ_1:def 3;

          then

          consider w be Element of ( REAL m) such that

           A8: w = (xseq . (i + 1)) & (yseq . (i + 1)) = |.w.| by A4, FINSEQ_1: 4;

          

           A9: 1 <= (i + 1) & (i + 1) <= ( len yseq) by A4, NAT_1: 11;

          yseq = ((yseq | i) ^ <*(yseq /. (i + 1))*>) by A4, FINSEQ_5: 21;

          then yseq = (yseq0 ^ <*(yseq . (i + 1))*>) by A9, FINSEQ_4: 15;

          then

           A10: ( Sum yseq) = (( Sum yseq0) + (yseq . (i + 1))) by RVSUM_1: 74;

          

           A11: i = ( len xseq0) by A4, FINSEQ_1: 59, NAT_1: 11;

          then

           A12: ex v be Element of ( REAL m) st v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum xseq0) + v) by A4, Th15;

          

           A13: |.(( Sum xseq0) + w).| <= ( |.( Sum xseq0).| + |.w.|) by EUCLID: 12;

          ( len xseq0) = ( len yseq0) by A4, A11, FINSEQ_1: 59, NAT_1: 11;

          then |.( Sum xseq0).| <= ( Sum yseq0) by A3, A5, A11;

          then ( |.( Sum xseq0).| + |.w.|) <= (( Sum yseq0) + (yseq . (i + 1))) by A8, XREAL_1: 6;

          hence |.( Sum xseq).| <= ( Sum yseq) by A4, A8, A10, A12, A13, XXREAL_0: 2;

        end;

        hence P[(i + 1)];

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    registration

      let m,n be Nat;

      cluster -> Lipschitzian for LinearOperator of m, n;

      coherence

      proof

        let f be LinearOperator of m, n;

        

         A1: m in NAT & n in NAT by ORDINAL1:def 12;

        defpred KSX[ Nat, object] means $2 = |.(f . ( Base_FinSeq (m,$1))).|;

        

         A2: for k0 be Nat st k0 in ( Seg m) holds ex v be Element of REAL st KSX[k0, v]

        proof

          let k0 be Nat;

          assume k0 in ( Seg m);

          consider v be Real such that

           A3: KSX[k0, v];

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

           KSX[k0, v] by A3;

          hence thesis;

        end;

        consider KS be FinSequence of REAL such that

         A4: ( dom KS) = ( Seg m) & for i be Nat st i in ( Seg m) holds KSX[i, (KS . i)] from FINSEQ_1:sch 5( A2);

        set K = (( Sum KS) + 1);

        now

          let j be Nat;

          assume j in ( dom KS);

          then (KS . j) = |.(f . ( Base_FinSeq (m,j))).| by A4;

          hence 0 <= (KS . j);

        end;

        then

         A5: 0 <= ( Sum KS) by RVSUM_1: 84;

        reconsider m0 = m as Nat;

        now

          let x be Element of ( REAL m);

          

           A6: ( len ( ProjFinSeq x)) = m by EUCLID_7:def 12;

          defpred PFX[ set, set] means $2 = (f . (( ProjFinSeq x) . $1));

           A7:

          now

            let k be Nat;

            assume k in ( Seg m);

            then k in ( dom ( ProjFinSeq x)) by A6, FINSEQ_1:def 3;

            then

            reconsider v = (( ProjFinSeq x) . k) as Element of ( REAL m) by PARTFUN1: 4;

            (f . v) is Element of ( REAL n);

            hence ex x be Element of ( REAL n) st PFX[k, x];

          end;

          consider fx be FinSequence of ( REAL n) such that

           A8: ( dom fx) = ( Seg m) & for i be Nat st i in ( Seg m) holds PFX[i, (fx . i)] from FINSEQ_1:sch 5( A7);

          

           A9: x = ( Sum ( ProjFinSeq x)) & ( len fx) = m by A1, A8, EUCLID_7: 31, FINSEQ_1:def 3;

          now

            let i be Nat;

            assume i in ( dom ( ProjFinSeq x));

            then i in ( Seg m) by A6, FINSEQ_1:def 3;

            hence (fx . i) = (f . (( ProjFinSeq x) . i)) by A8;

          end;

          then

           A10: ( Sum fx) = (f . x) by A6, A9, Th16;

          reconsider x0 = x as Element of ( REAL m);

          

           A11: for i be Nat st 1 <= i & i <= m holds ex v be Element of ( REAL n) st v = (fx . i) & |.v.| <= ( |.x.| * |.(f . ( Base_FinSeq (m,i))).|)

          proof

            let i be Nat;

            assume

             A12: 1 <= i & i <= m;

            then

             A13: (( ProjFinSeq x) . i) = ( |(x, ( Base_FinSeq (m,i)))| * ( Base_FinSeq (m,i))) by EUCLID_7:def 12;

            

             A14: i in ( Seg m) by A12;

            then

            reconsider v = (fx . i) as Element of ( REAL n) by A8, PARTFUN1: 4;

            take v;

            v = (f . (( ProjFinSeq x) . i)) by A8, A14;

            then v = ( |(x, ( Base_FinSeq (m,i)))| * (f . ( Base_FinSeq (m,i)))) by A13, Def2;

            then v = ((x0 . i) * (f . ( Base_FinSeq (m,i)))) by A12, EUCLID_7: 30;

            then |.v.| = ( |.(x0 . i).| * |.(f . ( Base_FinSeq (m,i))).|) by EUCLID: 11;

            hence thesis by A14, REAL_NS1: 8, XREAL_1: 64;

          end;

          defpred ZFX[ set, set] means ex v be Element of ( REAL n) st v = (fx . $1) & $2 = |.v.|;

           A15:

          now

            let k be Nat;

            assume k in ( Seg m);

            then

            reconsider v = (fx . k) as Element of ( REAL n) by A8, PARTFUN1: 4;

             |.v.| in REAL by XREAL_0:def 1;

            hence ex x be Element of REAL st ZFX[k, x];

          end;

          consider zfx be FinSequence of REAL such that

           A16: ( dom zfx) = ( Seg m) & for i be Nat st i in ( Seg m) holds ZFX[i, (zfx . i)] from FINSEQ_1:sch 5( A15);

          

           A17: ( len zfx) = m by A1, A16, FINSEQ_1:def 3;

          then

           A18: ( len fx) = ( len zfx) by A8, FINSEQ_1:def 3;

          for i be Nat st i in ( dom fx) holds ex v be Element of ( REAL n) st v = (fx . i) & (zfx . i) = |.v.| by A8, A16;

          then

           A19: |.(f . x).| <= ( Sum zfx) by A10, A18, Th17;

           A20:

          now

            let j be Nat;

            assume

             A21: j in ( Seg m);

            then

             A22: ex v be Element of ( REAL n) st v = (fx . j) & (zfx . j) = |.v.| by A16;

            1 <= j & j <= m by A21, FINSEQ_1: 1;

            then ex v be Element of ( REAL n) st v = (fx . j) & |.v.| <= ( |.x.| * |.(f . ( Base_FinSeq (m,j))).|) by A11;

            then (zfx . j) <= ( |.x.| * (KS . j)) by A4, A21, A22;

            hence (zfx . j) <= (( |.x.| * KS) . j) by VALUED_1: 6;

          end;

          

           A23: zfx is Element of (m -tuples_on REAL ) by A17, FINSEQ_2: 92;

          ( len KS) = m by A1, A4, FINSEQ_1:def 3;

          then

          reconsider KS0 = KS as Element of ( REAL m0) by FINSEQ_2: 92;

          ( |.x.| * KS0) is Element of (m0 -tuples_on REAL );

          then ( Sum zfx) <= ( Sum ( |.x.| * KS)) by A20, A23, RVSUM_1: 82;

          then ( Sum zfx) <= ( |.x.| * ( Sum KS)) by RVSUM_1: 87;

          then

           A24: |.(f . x).| <= ( |.x.| * ( Sum KS)) by A19, XXREAL_0: 2;

          ( 0 + ( Sum KS)) <= (1 + ( Sum KS)) by XREAL_1: 6;

          then ( |.x.| * ( Sum KS)) <= ( |.x.| * (1 + ( Sum KS))) by XREAL_1: 64;

          hence |.(f . x).| <= (K * |.x.|) by A24, XXREAL_0: 2;

        end;

        hence thesis by A5;

      end;

    end

    registration

      let m, n;

      cluster -> Lipschitzian for LinearOperator of ( REAL-NS m), ( REAL-NS n);

      coherence

      proof

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

        reconsider g = f as LinearOperator of m, n by Th14;

        consider K be Real such that

         A1: 0 <= K & for x be Element of ( REAL m) holds |.(g . x).| <= (K * |.x.|) by Def3;

        take K;

        thus 0 <= K by A1;

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

        reconsider x1 = x as Element of ( REAL m) by REAL_NS1:def 4;

        reconsider y = (g . x1) as Element of ( REAL n);

         ||.(f . x).|| = |.y.| by REAL_NS1: 1;

        then ||.(f . x).|| <= (K * |.x1.|) by A1;

        hence ||.(f . x).|| <= (K * ||.x.||) by REAL_NS1: 1;

      end;

    end

    theorem :: PDIFF_6:18

    

     Th18: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), x be Element of ( REAL m) st f is_differentiable_in x holds ( diff (f,x)) is LinearOperator of ( REAL-NS m), ( REAL-NS n)

    proof

      let m,n be non zero Nat;

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

      assume f is_differentiable_in x;

      then ( diff (f,x)) is Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))) by Th10;

      hence thesis by LOPBAN_1:def 9;

    end;

    theorem :: PDIFF_6:19

    for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), x be Element of ( REAL m) st f is_differentiable_in x holds ( diff (f,x)) is LinearOperator of m, n

    proof

      let m,n be non zero Nat;

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

      assume f is_differentiable_in x;

      then ( diff (f,x)) is LinearOperator of ( REAL-NS m), ( REAL-NS n) by Th18;

      hence thesis by Th14;

    end;

    theorem :: PDIFF_6:20

    for n,m be non zero Nat, g1,g2 be PartFunc of ( REAL m), ( REAL n), y0 be Element of ( REAL m) st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds (g1 + g2) is_differentiable_in y0 & ( diff ((g1 + g2),y0)) = (( diff (g1,y0)) + ( diff (g2,y0)))

    proof

      let n,m be non zero Nat, g1,g2 be PartFunc of ( REAL m), ( REAL n), y0 be Element of ( REAL m);

      assume

       A1: g1 is_differentiable_in y0 & g2 is_differentiable_in y0;

      reconsider f1 = g1 as PartFunc of ( REAL-NS m), ( REAL-NS n) by Th1;

      reconsider f2 = g2 as PartFunc of ( REAL-NS m), ( REAL-NS n) by Th1;

      reconsider x0 = y0 as Point of ( REAL-NS m) by REAL_NS1:def 4;

      f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1, Th2;

      then

       A2: (f1 + f2) is_differentiable_in x0 & ( diff ((f1 + f2),x0)) = (( diff (f1,x0)) + ( diff (f2,x0))) by NDIFF_1: 35;

      (f1 + f2) = (g1 + g2) by Th4;

      hence (g1 + g2) is_differentiable_in y0 by A2, Th2;

      then

       A3: ( diff ((g1 + g2),y0)) = ( diff ((f1 + f2),x0)) by Th4, Th3;

      ( diff (f1,x0)) = ( diff (g1,y0)) & ( diff (f2,x0)) = ( diff (g2,y0)) by Th3, A1;

      hence ( diff ((g1 + g2),y0)) = (( diff (g1,y0)) + ( diff (g2,y0))) by A2, A3, Th7;

    end;

    theorem :: PDIFF_6:21

    for n,m be non zero Nat, g1,g2 be PartFunc of ( REAL m), ( REAL n), y0 be Element of ( REAL m) st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds (g1 - g2) is_differentiable_in y0 & ( diff ((g1 - g2),y0)) = (( diff (g1,y0)) - ( diff (g2,y0)))

    proof

      let n,m be non zero Nat, g1,g2 be PartFunc of ( REAL m), ( REAL n), y0 be Element of ( REAL m);

      assume

       A1: g1 is_differentiable_in y0 & g2 is_differentiable_in y0;

      reconsider f1 = g1 as PartFunc of ( REAL-NS m), ( REAL-NS n) by Th1;

      reconsider f2 = g2 as PartFunc of ( REAL-NS m), ( REAL-NS n) by Th1;

      reconsider x0 = y0 as Point of ( REAL-NS m) by REAL_NS1:def 4;

      f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1, Th2;

      then

       A2: (f1 - f2) is_differentiable_in x0 & ( diff ((f1 - f2),x0)) = (( diff (f1,x0)) - ( diff (f2,x0))) by NDIFF_1: 36;

      (f1 - f2) = (g1 - g2) by Th5;

      hence (g1 - g2) is_differentiable_in y0 by A2, Th2;

      then

       A3: ( diff ((g1 - g2),y0)) = ( diff ((f1 - f2),x0)) by Th3, Th5;

      ( diff (f1,x0)) = ( diff (g1,y0)) & ( diff (f2,x0)) = ( diff (g2,y0)) by Th3, A1;

      hence ( diff ((g1 - g2),y0)) = (( diff (g1,y0)) - ( diff (g2,y0))) by A2, A3, Th8;

    end;

    theorem :: PDIFF_6:22

    for n,m be non zero Nat, g be PartFunc of ( REAL m), ( REAL n), y0 be Element of ( REAL m), r be Real st g is_differentiable_in y0 holds (r (#) g) is_differentiable_in y0 & ( diff ((r (#) g),y0)) = (r (#) ( diff (g,y0)))

    proof

      let n,m be non zero Nat, g be PartFunc of ( REAL m), ( REAL n), y0 be Element of ( REAL m), r be Real;

      assume

       A1: g is_differentiable_in y0;

      reconsider f = g as PartFunc of ( REAL-NS m), ( REAL-NS n) by Th1;

      reconsider x0 = y0 as Point of ( REAL-NS m) by REAL_NS1:def 4;

      f is_differentiable_in x0 by A1, Th2;

      then

       A2: (r (#) f) is_differentiable_in x0 & ( diff ((r (#) f),x0)) = (r * ( diff (f,x0))) by NDIFF_1: 37;

      (r (#) f) = (r (#) g) by Th6;

      hence (r (#) g) is_differentiable_in y0 by A2, Th2;

      then ( diff ((r (#) g),y0)) = ( diff ((r (#) f),x0)) by Th3, Th6;

      hence ( diff ((r (#) g),y0)) = (r (#) ( diff (g,y0))) by A2, Th9, Th3, A1;

    end;

    theorem :: PDIFF_6:23

    

     Th23: for x0 be Element of ( REAL m), y0 be Point of ( REAL-NS m), r be Real st x0 = y0 holds { y where y be Element of ( REAL m) : |.(y - x0).| < r } = { z where z be Point of ( REAL-NS m) : ||.(z - y0).|| < r }

    proof

      let x0 be Element of ( REAL m), y0 be Point of ( REAL-NS m), r be Real;

      assume

       A1: x0 = y0;

      now

        let w be object;

        assume w in { y where y be Element of ( REAL m) : |.(y - x0).| < r };

        then

        consider y be Element of ( REAL m) such that

         A2: y = w & |.(y - x0).| < r;

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

         ||.(z - y0).|| < r by A1, A2, REAL_NS1: 1, REAL_NS1: 5;

        hence w in { z1 where z1 be Point of ( REAL-NS m) : ||.(z1 - y0).|| < r } by A2;

      end;

      then

       A3: { y where y be Element of ( REAL m) : |.(y - x0).| < r } c= { z where z be Point of ( REAL-NS m) : ||.(z - y0).|| < r } by TARSKI:def 3;

      now

        let w be object;

        assume w in { z where z be Point of ( REAL-NS m) : ||.(z - y0).|| < r };

        then

        consider y be Point of ( REAL-NS m) such that

         A4: y = w & ||.(y - y0).|| < r;

        reconsider z = y as Element of ( REAL m) by REAL_NS1:def 4;

         |.(z - x0).| < r by A1, A4, REAL_NS1: 1, REAL_NS1: 5;

        hence w in { z1 where z1 be Element of ( REAL m) : |.(z1 - x0).| < r } by A4;

      end;

      then { z where z be Point of ( REAL-NS m) : ||.(z - y0).|| < r } c= { y where y be Element of ( REAL m) : |.(y - x0).| < r } by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: PDIFF_6:24

    

     Th24: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), x0 be Element of ( REAL m), L,R be Function of ( REAL m), ( REAL n) st L is LinearOperator of m, n & ex r0 be Real st 0 < r0 & { y where y be Element of ( REAL m) : |.(y - x0).| < r0 } c= ( dom f) & (for r be Real st r > 0 holds ex d be Real st d > 0 & (for z be Element of ( REAL m), w be Element of ( REAL n) st z <> ( 0* m) & |.z.| < d & w = (R . z) holds (( |.z.| " ) * |.w.|) < r)) & for x be Element of ( REAL m) st |.(x - x0).| < r0 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R . (x - x0))) holds f is_differentiable_in x0 & ( diff (f,x0)) = L

    proof

      let m,n be non zero Nat;

      let f be PartFunc of ( REAL m), ( REAL n), x0 be Element of ( REAL m), L,R be Function of ( REAL m), ( REAL n);

      reconsider g = f as PartFunc of ( REAL-NS m), ( REAL-NS n) by Th1;

      reconsider y0 = x0 as Point of ( REAL-NS m) by REAL_NS1:def 4;

      assume

       A1: L is LinearOperator of m, n;

      given r0 be Real such that

       A2: 0 < r0 & { y where y be Element of ( REAL m) : |.(y - x0).| < r0 } c= ( dom f) & (for r be Real st r > 0 holds ex d be Real st d > 0 & (for z be Element of ( REAL m), w be Element of ( REAL n) st z <> ( 0* m) & |.z.| < d & w = (R . z) holds (( |.z.| " ) * |.w.|) < r)) & for x be Element of ( REAL m) st |.(x - x0).| < r0 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R . (x - x0)));

      L is LinearOperator of ( REAL-NS m), ( REAL-NS n) by A1, Th14;

      then

      reconsider GL = L as Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))) by LOPBAN_1:def 9;

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

      then

      reconsider GR = R as Function of ( REAL-NS m), ( REAL-NS n);

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

      then

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

      now

        let r be Real;

        assume r > 0 ;

        then

        consider d be Real such that

         A4: d > 0 & (for z be Element of ( REAL m), w be Element of ( REAL n) st z <> ( 0* m) & |.z.| < d & w = (R . z) holds (( |.z.| " ) * |.w.|) < r) by A2;

        take d;

        thus d > 0 by A4;

        thus for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(GR /. z).||) < r

        proof

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

          assume

           A5: z <> ( 0. ( REAL-NS m)) & ||.z.|| < d;

          reconsider s = z as Element of ( REAL m) by REAL_NS1:def 4;

          reconsider w = (R . s) as Element of ( REAL n);

          

           A6: s <> ( 0* m) by A5, REAL_NS1:def 4;

           |.s.| < d by A5, REAL_NS1: 1;

          then (( |.s.| " ) * |.w.|) < r by A4, A6;

          then (( ||.z.|| " ) * |.w.|) < r by REAL_NS1: 1;

          hence (( ||.z.|| " ) * ||.(GR /. z).||) < r by REAL_NS1: 1;

        end;

      end;

      then

      reconsider GR as RestFunc of ( REAL-NS m), ( REAL-NS n) by NDIFF_1: 23;

      set N = { y where y be Point of ( REAL-NS m) : ||.(y - y0).|| < r0 };

      reconsider N as Neighbourhood of y0 by A2, NFCONT_1: 3;

      

       A7: N c= ( dom g) by A2, Th23;

      

       A8: for y be Point of ( REAL-NS m) st y in N holds ((g /. y) - (g /. y0)) = ((GL . (y - y0)) + (GR /. (y - y0)))

      proof

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

        assume

         A9: y in N;

        reconsider x = y as Element of ( REAL m) by REAL_NS1:def 4;

        x in { s where s be Element of ( REAL m) : |.(s - x0).| < r0 } by A9, Th23;

        then ex s be Element of ( REAL m) st s = x & |.(s - x0).| < r0;

        then

         A10: ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R . (x - x0))) by A2;

        

         A11: y0 in N by NFCONT_1: 4;

        then (f /. x) = (f . x) & (f /. x0) = (f . x0) by A9, A7, PARTFUN1:def 6;

        then

         A12: (f /. x) = (g /. y) & (f /. x0) = (g /. y0) by A9, A11, A7, PARTFUN1:def 6;

        (x - x0) = (y - y0) by REAL_NS1: 5;

        then (L . (x - x0)) = (GL . (y - y0)) & (R . (x - x0)) = (GR /. (y - y0)) by A3, PARTFUN1:def 6;

        then ((L . (x - x0)) + (R . (x - x0))) = ((GL . (y - y0)) + (GR /. (y - y0))) by REAL_NS1: 2;

        hence ((g /. y) - (g /. y0)) = ((GL . (y - y0)) + (GR /. (y - y0))) by A10, A12, REAL_NS1: 5;

      end;

      then

       A13: g is_differentiable_in y0 by A7, NDIFF_1:def 6;

      hence

       A14: f is_differentiable_in x0 by Th2;

      ( diff (g,y0)) = GL by A13, A8, A7, NDIFF_1:def 7;

      hence thesis by Th3, A14;

    end;

    theorem :: PDIFF_6:25

    for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), x0 be Element of ( REAL m) holds f is_differentiable_in x0 iff ex r0 be Real st 0 < r0 & { y where y be Element of ( REAL m) : |.(y - x0).| < r0 } c= ( dom f) & ex L,R be Function of ( REAL m), ( REAL n) st L is LinearOperator of m, n & (for r be Real st r > 0 holds ex d be Real st d > 0 & (for z be Element of ( REAL m), w be Element of ( REAL n) st z <> ( 0* m) & |.z.| < d & w = (R . z) holds (( |.z.| " ) * |.w.|) < r)) & for x be Element of ( REAL m) st |.(x - x0).| < r0 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R . (x - x0)))

    proof

      let m,n be non zero Nat;

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

      reconsider g = f as PartFunc of ( REAL-NS m), ( REAL-NS n) by Th1;

      reconsider y0 = x0 as Point of ( REAL-NS m) by REAL_NS1:def 4;

      hereby

        assume f is_differentiable_in x0;

        then g is_differentiable_in y0 by Th2;

        then

        consider N be Neighbourhood of y0 such that

         A1: N c= ( dom g) & ex GL be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))), GR be RestFunc of ( REAL-NS m), ( REAL-NS n) st for y be Point of ( REAL-NS m) st y in N holds ((g /. y) - (g /. y0)) = ((GL . (y - y0)) + (GR /. (y - y0))) by NDIFF_1:def 6;

        consider GL be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n))), GR be RestFunc of ( REAL-NS m), ( REAL-NS n) such that

         A2: for y be Point of ( REAL-NS m) st y in N holds ((g /. y) - (g /. y0)) = ((GL . (y - y0)) + (GR /. (y - y0))) by A1;

        consider r0 be Real such that

         A3: 0 < r0 & { y where y be Point of ( REAL-NS m) : ||.(y - y0).|| < r0 } c= N by NFCONT_1:def 1;

        take r0;

        thus 0 < r0 by A3;

        { y where y be Point of ( REAL-NS m) : ||.(y - y0).|| < r0 } c= ( dom g) by A3, A1, XBOOLE_1: 1;

        hence { y where y be Element of ( REAL m) : |.(y - x0).| < r0 } c= ( dom f) by Th23;

        

         A4: GR is total by NDIFF_1:def 5;

        then

         A5: ( dom GR) = the carrier of ( REAL-NS m) by PARTFUN1:def 2;

        

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

        then

        reconsider L = GL as Function of ( REAL m), ( REAL n) by LOPBAN_1:def 9;

        reconsider R = GR as Function of ( REAL m), ( REAL n) by A6, A4;

        take L, R;

        GL is LinearOperator of ( REAL-NS m), ( REAL-NS n) by LOPBAN_1:def 9;

        hence L is LinearOperator of m, n by Th14;

        thus for r be Real st r > 0 holds ex d be Real st d > 0 & (for z be Element of ( REAL m), w be Element of ( REAL n) st z <> ( 0* m) & |.z.| < d & w = (R . z) holds (( |.z.| " ) * |.w.|) < r)

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider d be Real such that

           A7: d > 0 & (for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(GR /. z).||) < r) by A4, NDIFF_1: 23;

          take d;

          thus d > 0 by A7;

          let z be Element of ( REAL m), w be Element of ( REAL n);

          assume

           A8: z <> ( 0* m) & |.z.| < d & w = (R . z);

          reconsider s = z as Element of ( REAL-NS m) by REAL_NS1:def 4;

          

           A9: s <> ( 0. ( REAL-NS m)) by A8, REAL_NS1:def 4;

           ||.s.|| < d by A8, REAL_NS1: 1;

          then (( ||.s.|| " ) * ||.(GR /. s).||) < r by A7, A9;

          then (( |.z.| " ) * ||.(GR /. s).||) < r by REAL_NS1: 1;

          hence (( |.z.| " ) * |.w.|) < r by A5, A8, PARTFUN1:def 6, REAL_NS1: 1;

        end;

        thus for x be Element of ( REAL m) st |.(x - x0).| < r0 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R . (x - x0)))

        proof

          let x be Element of ( REAL m);

          assume |.(x - x0).| < r0;

          then x in { s where s be Element of ( REAL m) : |.(s - x0).| < r0 };

          then

           A10: x in { y where y be Point of ( REAL-NS m) : ||.(y - y0).|| < r0 } by Th23;

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

          

           A11: ((g /. y) - (g /. y0)) = ((GL . (y - y0)) + (GR /. (y - y0))) by A3, A10, A2;

          

           A12: y in N & y0 in N by A3, A10, NFCONT_1: 4;

          then (f /. x) = (f . x) & (f /. x0) = (f . x0) by A1, PARTFUN1:def 6;

          then

           A13: (f /. x) = (g /. y) & (f /. x0) = (g /. y0) by A12, A1, PARTFUN1:def 6;

          (x - x0) = (y - y0) by REAL_NS1: 5;

          then (L . (x - x0)) = (GL . (y - y0)) & (R . (x - x0)) = (GR /. (y - y0)) by A5, PARTFUN1:def 6;

          then ((L . (x - x0)) + (R . (x - x0))) = ((GL . (y - y0)) + (GR /. (y - y0))) by REAL_NS1: 2;

          hence ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R . (x - x0))) by A11, A13, REAL_NS1: 5;

        end;

      end;

      assume ex r0 be Real st 0 < r0 & { y where y be Element of ( REAL m) : |.(y - x0).| < r0 } c= ( dom f) & ex L,R be Function of ( REAL m), ( REAL n) st L is LinearOperator of m, n & (for r be Real st r > 0 holds ex d be Real st d > 0 & (for z be Element of ( REAL m), w be Element of ( REAL n) st z <> ( 0* m) & |.z.| < d & w = (R . z) holds (( |.z.| " ) * |.w.|) < r)) & for x be Element of ( REAL m) st |.(x - x0).| < r0 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R . (x - x0)));

      hence f is_differentiable_in x0 by Th24;

    end;

    begin

    theorem :: PDIFF_6:26

    

     Th26: for y1,y2 be Point of ( REAL-NS n) holds (( Proj (i,n)) . (y1 + y2)) = ((( Proj (i,n)) . y1) + (( Proj (i,n)) . y2))

    proof

      let y1,y2 be Point of ( REAL-NS n);

      reconsider yy1 = y1, yy2 = y2 as Element of ( REAL n) by REAL_NS1:def 4;

      reconsider ry1 = (yy1 . i) as Element of REAL by XREAL_0:def 1;

      reconsider ry2 = (yy2 . i) as Element of REAL by XREAL_0:def 1;

      (( Proj (i,n)) . y1) = <*(( proj (i,n)) . y1)*> & (( Proj (i,n)) . y2) = <*(( proj (i,n)) . y2)*> by PDIFF_1:def 4;

      then

       A1: (( Proj (i,n)) . y1) = <*ry1*> & (( Proj (i,n)) . y2) = <*ry2*> by PDIFF_1:def 1;

      

       A2: <*ry1*> is Element of ( REAL 1) & <*ry2*> is Element of ( REAL 1) by FINSEQ_2: 98;

      (( Proj (i,n)) . (y1 + y2)) = <*(( proj (i,n)) . (y1 + y2))*> by PDIFF_1:def 4

      .= <*(( proj (i,n)) . (yy1 + yy2))*> by REAL_NS1: 2

      .= <*((yy1 + yy2) . i)*> by PDIFF_1:def 1

      .= <*((yy1 . i) + (yy2 . i))*> by RVSUM_1: 11

      .= ( <*ry1*> + <*ry2*>) by RVSUM_1: 13;

      hence thesis by A1, A2, REAL_NS1: 2;

    end;

    theorem :: PDIFF_6:27

    

     Th27: for y1 be Point of ( REAL-NS n), r be Real holds (( Proj (i,n)) . (r * y1)) = (r * (( Proj (i,n)) . y1))

    proof

      let y1 be Point of ( REAL-NS n), r be Real;

      reconsider yy1 = y1 as Element of ( REAL n) by REAL_NS1:def 4;

      reconsider y1i = (yy1 . i) as Element of REAL by XREAL_0:def 1;

      (( Proj (i,n)) . y1) = <*(( proj (i,n)) . y1)*> by PDIFF_1:def 4;

      then

       A1: (( Proj (i,n)) . y1) = <*y1i*> by PDIFF_1:def 1;

      

       A2: <*y1i*> is Element of ( REAL 1) by FINSEQ_2: 98;

      (( Proj (i,n)) . (r * y1)) = <*(( proj (i,n)) . (r * y1))*> by PDIFF_1:def 4

      .= <*(( proj (i,n)) . (r * yy1))*> by REAL_NS1: 3

      .= <*((r * yy1) . i)*> by PDIFF_1:def 1

      .= <*(r * (yy1 . i))*> by RVSUM_1: 44

      .= (r * <*y1i*>) by RVSUM_1: 47;

      hence thesis by A1, A2, REAL_NS1: 3;

    end;

    theorem :: PDIFF_6:28

    

     Th28: for m,n be non zero Nat, g be PartFunc of ( REAL-NS m), ( REAL-NS n), x0 be Point of ( REAL-NS m), i be Nat st 1 <= i & i <= n & g is_differentiable_in x0 holds (( Proj (i,n)) * g) is_differentiable_in x0 & (( Proj (i,n)) * ( diff (g,x0))) = ( diff ((( Proj (i,n)) * g),x0))

    proof

      let m,n be non zero Nat;

      let g be PartFunc of ( REAL-NS m), ( REAL-NS n), x0 be Point of ( REAL-NS m), i be Nat;

      assume

       A1: 1 <= i & i <= n & g is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A2: N c= ( dom g) & ex GR be RestFunc of ( REAL-NS m), ( REAL-NS n) st for x be Point of ( REAL-NS m) st x in N holds ((g /. x) - (g /. x0)) = ((( diff (g,x0)) . (x - x0)) + (GR /. (x - x0))) by NDIFF_1:def 7;

      consider GR be RestFunc of ( REAL-NS m), ( REAL-NS n) such that

       A3: for x be Point of ( REAL-NS m) st x in N holds ((g /. x) - (g /. x0)) = ((( diff (g,x0)) . (x - x0)) + (GR /. (x - x0))) by A2;

      set RLB0 = ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS 1)));

      reconsider DFG = ( diff (g,x0)) as LinearOperator of ( REAL-NS m), ( REAL-NS n) by LOPBAN_1:def 9;

      reconsider PG = ( Proj (i,n)) as Function of the carrier of ( REAL-NS n), the carrier of ( REAL-NS 1);

      (PG * DFG) is Function of the carrier of ( REAL-NS m), the carrier of ( REAL-NS 1);

      then

      reconsider L = (( Proj (i,n)) * ( diff (g,x0))) as Function of ( REAL-NS m), ( REAL-NS 1);

      

       A4: for x,y be VECTOR of ( REAL-NS m) holds (L . (x + y)) = ((L . x) + (L . y))

      proof

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

        

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

        

         A6: (DFG . (x + y)) = ((DFG . x) + (DFG . y)) by VECTSP_1:def 20;

        (L . (x + y)) = (( Proj (i,n)) . (DFG . (x + y))) by A5, FUNCT_1: 12

        .= ((( Proj (i,n)) . (DFG . x)) + (( Proj (i,n)) . (DFG . y))) by A6, Th26

        .= ((( Proj (i,n)) . (DFG . x)) + (L . y)) by A5, FUNCT_1: 12;

        hence (L . (x + y)) = ((L . x) + (L . y)) by A5, FUNCT_1: 12;

      end;

      for x be VECTOR of ( REAL-NS m), r be Real holds (L . (r * x)) = (r * (L . x))

      proof

        let x be VECTOR of ( REAL-NS m), r be Real;

        

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

        (DFG . (r * x)) = (r * (DFG . x)) by LOPBAN_1:def 5;

        then (( Proj (i,n)) . (DFG . (r * x))) = (r * (( Proj (i,n)) . (DFG . x))) by Th27;

        then (L . (r * x)) = (r * (( Proj (i,n)) . (DFG . x))) by A7, FUNCT_1: 12;

        hence (L . (r * x)) = (r * (L . x)) by A7, FUNCT_1: 12;

      end;

      then

      reconsider L as LinearOperator of ( REAL-NS m), ( REAL-NS 1) by A4, LOPBAN_1:def 5, VECTSP_1:def 20;

      reconsider L as Point of RLB0 by LOPBAN_1:def 9;

      

       A8: GR is total by NDIFF_1:def 5;

      then

      reconsider FGR = GR as Function of the carrier of ( REAL-NS m), the carrier of ( REAL-NS n);

      

       A9: (( Proj (i,n)) * FGR) is Function of the carrier of ( REAL-NS m), the carrier of ( REAL-NS 1);

      (( Proj (i,n)) * GR) is RestFunc of ( REAL-NS m), ( REAL-NS 1)

      proof

        

         A10: ( dom GR) = the carrier of ( REAL-NS m) by A8, PARTFUN1:def 2;

        reconsider R = (( Proj (i,n)) * GR) as PartFunc of ( REAL-NS m), ( REAL-NS 1);

        for r be Real st r > 0 holds ex d be Real st d > 0 & (for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r)

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider d be Real such that

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

          take d;

          thus d > 0 by A11;

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

          assume

           A12: z <> ( 0. ( REAL-NS m)) & ||.z.|| < d;

          

           A13: (GR /. z) = (GR . z) by A10, PARTFUN1:def 6;

          

           A14: i in ( Seg n) by A1;

          reconsider GRz = (GR /. z) as Point of ( REAL-NS n);

          reconsider GRz1 = GRz as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider GRzi = (GRz1 . i) as Element of REAL by XREAL_0:def 1;

          ( dom ( Proj (i,n))) = the carrier of ( REAL-NS n) by PARTFUN1:def 2;

          then

           A15: z in ( dom (( Proj (i,n)) * GR)) by A10, A13, FUNCT_1: 11;

          

          then ((( Proj (i,n)) * GR) . z) = (( Proj (i,n)) . (GR . z)) by FUNCT_1: 12

          .= <*(( proj (i,n)) . GRz1)*> by A13, PDIFF_1:def 4;

          then

           A16: ((( Proj (i,n)) * GR) . z) = <*GRzi*> by PDIFF_1:def 1;

          

           A17: |.GRzi.| <= ||.(GR /. z).|| by A14, REAL_NS1: 9;

          

           A18: 0 <= ||.z.|| by NORMSP_1: 4;

           0 <= |.GRzi.| by COMPLEX1: 46;

          then

           A19: (( ||.z.|| " ) * |.GRzi.|) <= (( ||.z.|| " ) * ||.(GR /. z).||) by A17, A18, XREAL_1: 66;

          (( ||.z.|| " ) * ||.(GR /. z).||) < r by A11, A12;

          then

           A20: (( ||.z.|| " ) * |.GRzi.|) < r by A19, XXREAL_0: 2;

          ((( Proj (i,n)) * GR) . z) in ( rng (( Proj (i,n)) * GR)) by A15, FUNCT_1: 3;

          then

          reconsider Rz = ((( Proj (i,n)) * GR) . z) as VECTOR of ( REAL-NS 1);

          set VGRzi = <*GRzi*>;

          VGRzi is Element of ( REAL 1) by FINSEQ_2: 98;

          then ||.Rz.|| = |.VGRzi.| by A16, REAL_NS1: 1;

          then (( ||.z.|| " ) * ||.Rz.||) < r by A20, JORDAN2C: 10;

          hence thesis by A15, PARTFUN1:def 6;

        end;

        hence thesis by A9, NDIFF_1: 23;

      end;

      then

      reconsider R = (( Proj (i,n)) * GR) as RestFunc of ( REAL-NS m), ( REAL-NS 1);

      set pg = (( Proj (i,n)) * g);

      

       A21: ( dom ( Proj (i,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

      then ( rng g) c= ( dom ( Proj (i,n)));

      then

       A22: ( dom g) = ( dom (( Proj (i,n)) * g)) by RELAT_1: 27;

      

       A23: ( dom ( Proj (i,n))) = ( REAL n) by A21, REAL_NS1:def 4;

      

       A24: for x be Point of ( REAL-NS m) st x in N holds ((pg /. x) - (pg /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

      proof

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

        now

          assume

           A25: x in N;

          then

           A26: ((g /. x) - (g /. x0)) = ((( diff (g,x0)) . (x - x0)) + (GR /. (x - x0))) by A3;

          

           A27: x0 in N by NFCONT_1: 4;

          then

           A28: (pg /. x) = (pg . x) & (pg /. x0) = (pg . x0) by A2, A22, A25, PARTFUN1:def 6;

          

           A29: (g /. x) = (g . x) & (g /. x0) = (g . x0) by A2, A25, A27, PARTFUN1:def 6;

          reconsider PGSx = ((pg /. x) - (pg /. x0)) as Element of ( REAL 1) by REAL_NS1:def 4;

          (pg . x) in ( rng pg) by A2, A22, A25, FUNCT_1: 3;

          then

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

          (pg . x0) in ( rng pg) by A2, A22, A27, FUNCT_1: 3;

          then

          reconsider PGdx0 = (pg . x0) as Element of ( REAL 1) by REAL_NS1:def 4;

          (g . x) in ( rng g) by A2, A25, FUNCT_1: 3;

          then

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

          (g . x0) in ( rng g) by A2, A27, FUNCT_1: 3;

          then

          reconsider Gx0 = (g . x0) as Element of ( REAL n) by REAL_NS1:def 4;

          set ProjGx = (( Proj (i,n)) . (g . x));

          Gx in ( dom ( Proj (i,n))) by A23;

          then ProjGx in ( rng ( Proj (i,n))) by FUNCT_1: 3;

          then

          reconsider ProjGx as Element of ( REAL 1) by REAL_NS1:def 4;

          set ProjGx0 = (( Proj (i,n)) . (g . x0));

          Gx0 in ( dom ( Proj (i,n))) by A23;

          then ProjGx0 in ( rng ( Proj (i,n))) by FUNCT_1: 3;

          then

          reconsider ProjGx0 as Element of ( REAL 1) by REAL_NS1:def 4;

          reconsider Gx1 = Gx as Element of ( REAL-NS n) by REAL_NS1:def 4;

          reconsider Gx01 = Gx0 as Element of ( REAL-NS n) by REAL_NS1:def 4;

          reconsider Gsx = (g /. x) as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider Gsx0 = (g /. x0) as Element of ( REAL n) by REAL_NS1:def 4;

          set dxx0 = (x - x0);

          reconsider Ldxx0 = (L . (x - x0)) as Element of ( REAL-NS 1);

          

           A30: ( dom R) = the carrier of ( REAL-NS m) by A9, PARTFUN1:def 2;

          then

           A31: (R /. (x - x0)) = (R . dxx0) by PARTFUN1:def 6;

          then

          reconsider Rdxx0 = (R . (x - x0)) as Element of ( REAL-NS 1);

          reconsider Ldiff = (( diff (g,x0)) . (x - x0)) as Element of ( REAL n) by REAL_NS1:def 4;

          set ProjLdiff = (( Proj (i,n)) . Ldiff);

          ProjLdiff in ( rng ( Proj (i,n))) by A21, FUNCT_1: 3;

          then

          reconsider ProjLdiff as Element of ( REAL 1) by REAL_NS1:def 4;

          

           A32: ( dom GR) = the carrier of ( REAL-NS m) by A8, PARTFUN1:def 2;

          then (GR . dxx0) in ( rng GR) by FUNCT_1: 3;

          then

          reconsider Rdiff = (GR . dxx0) as Element of ( REAL n) by REAL_NS1:def 4;

          

           A33: Rdiff = (GR /. dxx0) by A32, PARTFUN1:def 6;

          set ProjRdiff = (( Proj (i,n)) . Rdiff);

          ProjRdiff in ( rng ( Proj (i,n))) by A23, FUNCT_1: 3;

          then

          reconsider ProjRdiff as Element of ( REAL 1) by REAL_NS1:def 4;

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

          then (L . (x - x0)) = (( Proj (i,n)) . Ldiff) & (R . (x - x0)) = (( Proj (i,n)) . Rdiff) by A30, FUNCT_1: 12;

          then

           A34: (Ldxx0 + Rdxx0) = (ProjLdiff + ProjRdiff) by REAL_NS1: 2;

          (( Proj (i,n)) . Ldiff) = <*(( proj (i,n)) . Ldiff)*> by PDIFF_1:def 4;

          then

           A35: (( Proj (i,n)) . Ldiff) = <*(Ldiff . i)*> by PDIFF_1:def 1;

          Rdiff in ( dom ( Proj (i,n))) by A23;

          then (( Proj (i,n)) . Rdiff) = <*(( proj (i,n)) . Rdiff)*> by PDIFF_1:def 4;

          then

           A36: (( Proj (i,n)) . Rdiff) = <*(Rdiff . i)*> by PDIFF_1:def 1;

          reconsider diffGR = ((( diff (g,x0)) . (x - x0)) + (GR /. (x - x0))) as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider Rsdiff = (GR /. (x - x0)) as Element of ( REAL n) by REAL_NS1:def 4;

          PGSx = (PGdx - PGdx0) by A28, REAL_NS1: 5

          .= (ProjGx - PGdx0) by A2, A22, A25, FUNCT_1: 12

          .= (ProjGx - ProjGx0) by A2, A22, A27, FUNCT_1: 12

          .= ( <*(( proj (i,n)) . Gx1)*> - ProjGx0) by PDIFF_1:def 4

          .= ( <*(( proj (i,n)) . Gx1)*> - <*(( proj (i,n)) . Gx01)*>) by PDIFF_1:def 4

          .= ( <*(Gx . i)*> - <*(( proj (i,n)) . Gx01)*>) by PDIFF_1:def 1

          .= ( <*(Gx . i)*> - <*(Gx0 . i)*>) by PDIFF_1:def 1

          .= <*((Gx . i) - (Gx0 . i))*> by RVSUM_1: 29

          .= <*((Gsx - Gsx0) . i)*> by A29, RVSUM_1: 27

          .= <*(diffGR . i)*> by A26, REAL_NS1: 5

          .= <*((Ldiff + Rsdiff) . i)*> by REAL_NS1: 2

          .= <*((Ldiff . i) + (Rsdiff . i))*> by RVSUM_1: 11;

          hence thesis by A31, A34, A35, A36, A33, RVSUM_1: 13;

        end;

        hence thesis;

      end;

      hence (( Proj (i,n)) * g) is_differentiable_in x0 by A2, A22, NDIFF_1:def 6;

      hence (( Proj (i,n)) * ( diff (g,x0))) = ( diff ((( Proj (i,n)) * g),x0)) by A2, A22, A24, NDIFF_1:def 7;

    end;

    theorem :: PDIFF_6:29

    for m,n be non zero Nat, g be PartFunc of ( REAL-NS m), ( REAL-NS n), x0 be Point of ( REAL-NS m) holds g is_differentiable_in x0 iff (for i be Nat st 1 <= i & i <= n holds (( Proj (i,n)) * g) is_differentiable_in x0)

    proof

      let m,n be non zero Nat;

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

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

      set RB = ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS n)));

      (for i be Nat st 1 <= i & i <= n holds (( Proj (i,n)) * g) is_differentiable_in x0) implies g is_differentiable_in x0

      proof

        assume

         A1: for i be Nat st 1 <= i & i <= n holds (( Proj (i,n)) * g) is_differentiable_in x0;

        defpred Pd[ Nat, Element of REAL ] means $2 > 0 & { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < $2 } c= ( dom (( Proj ($1,n)) * g)) & ex Ri be RestFunc of ( REAL-NS m), ( REAL-NS 1) st for x be Point of ( REAL-NS m) st x in { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < $2 } holds (((( Proj ($1,n)) * g) /. x) - ((( Proj ($1,n)) * g) /. x0)) = ((( diff ((( Proj ($1,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)));

        

         A2: for k be Nat st k in ( Seg n) holds ex dk be Element of REAL st Pd[k, dk]

        proof

          let k be Nat;

          assume k in ( Seg n);

          then 1 <= k & k <= n by FINSEQ_1: 1;

          then (( Proj (k,n)) * g) is_differentiable_in x0 by A1;

          then

          consider Nk be Neighbourhood of x0 such that

           A3: Nk c= ( dom (( Proj (k,n)) * g)) & ex Rk be RestFunc of ( REAL-NS m), ( REAL-NS 1) st for x be Point of ( REAL-NS m) st x in Nk holds (((( Proj (k,n)) * g) /. x) - ((( Proj (k,n)) * g) /. x0)) = ((( diff ((( Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0))) by NDIFF_1:def 7;

          consider dk be Real such that

           A4: 0 < dk & { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < dk } c= Nk by NFCONT_1:def 1;

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

          take dk;

          thus 0 < dk by A4;

          thus { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < dk } c= ( dom (( Proj (k,n)) * g)) by A4, A3, XBOOLE_1: 1;

          thus ex Rk be RestFunc of ( REAL-NS m), ( REAL-NS 1) st for x be Point of ( REAL-NS m) st x in { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < dk } holds (((( Proj (k,n)) * g) /. x) - ((( Proj (k,n)) * g) /. x0)) = ((( diff ((( Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)))

          proof

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

             A5: for x be Point of ( REAL-NS m) st x in Nk holds (((( Proj (k,n)) * g) /. x) - ((( Proj (k,n)) * g) /. x0)) = ((( diff ((( Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0))) by A3;

            take Rk;

            thus for x be Point of ( REAL-NS m) st x in { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < dk } holds (((( Proj (k,n)) * g) /. x) - ((( Proj (k,n)) * g) /. x0)) = ((( diff ((( Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0))) by A4, A5;

          end;

        end;

        consider d be FinSequence of REAL such that

         A6: ( dom d) = ( Seg n) & for k be Nat st k in ( Seg n) holds Pd[k, (d /. k)] from RECDEF_1:sch 17( A2);

        set d0 = ( min d);

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

        ( len d) = nn by A6, FINSEQ_1:def 3;

        then

         A7: ( min_p d) in ( dom d) by RFINSEQ2:def 2;

        then (d /. ( min_p d)) > 0 by A6;

        then

         A8: d0 > 0 by A7, PARTFUN1:def 6;

        defpred LX[ set, set] means ex y be Element of ( REAL n) st $2 = y & for i be Nat st i in ( Seg n) holds (y . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . $1));

        

         A9: for x be Point of ( REAL-NS m) holds ex y be Point of ( REAL-NS n) st LX[x, y]

        proof

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

          defpred YX[ Nat, set] means $2 = (( proj (1,1)) . (( diff ((( Proj ($1,n)) * g),x0)) . x));

          

           A10: for i be Nat st i in ( Seg n) holds ex r be Element of REAL st YX[i, r]

          proof

            let i be Nat;

            assume i in ( Seg n);

            (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . x)) in REAL by XREAL_0:def 1;

            hence thesis;

          end;

          consider y be FinSequence of REAL such that

           A11: ( dom y) = ( Seg n) & for i be Nat st i in ( Seg n) holds YX[i, (y /. i)] from RECDEF_1:sch 17( A10);

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

          ( len y) = nn by A11, FINSEQ_1:def 3;

          then

          reconsider y as Element of ( REAL n) by FINSEQ_2: 92;

           A12:

          now

            let i be Nat;

            assume i in ( Seg n);

            then YX[i, (y /. i)] & (y /. i) = (y . i) by A11, PARTFUN1:def 6;

            hence (y . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . x));

          end;

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

          ex y be Element of ( REAL n) st y0 = y & for i be Nat st i in ( Seg n) holds (y . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . x)) by A12;

          hence ex y0 be Point of ( REAL-NS n) st LX[x, y0];

        end;

        consider L be Function of ( REAL-NS m), ( REAL-NS n) such that

         A13: for x be Point of ( REAL-NS m) holds LX[x, (L . x)] from FUNCT_2:sch 3( A9);

        

         A14: for x,y be VECTOR of ( REAL-NS m) holds (L . (x + y)) = ((L . x) + (L . y))

        proof

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

          consider Lx be Element of ( REAL n) such that

           A15: (L . x) = Lx & for i be Nat st i in ( Seg n) holds (Lx . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . x)) by A13;

          consider Ly be Element of ( REAL n) such that

           A16: (L . y) = Ly & for i be Nat st i in ( Seg n) holds (Ly . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . y)) by A13;

          consider Lxy be Element of ( REAL n) such that

           A17: (L . (x + y)) = Lxy & for i be Nat st i in ( Seg n) holds (Lxy . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . (x + y))) by A13;

          ( dom Lxy) = ( Seg n) by FINSEQ_1: 89;

          then

           A18: ( dom Lxy) = ( dom (Lx + Ly)) by FINSEQ_1: 89;

          for i0 be Nat st i0 in ( dom Lxy) holds (Lxy . i0) = ((Lx + Ly) . i0)

          proof

            let i0 be Nat;

            reconsider i = i0 as Nat;

            assume i0 in ( dom Lxy);

            then i in ( Seg n) by FINSEQ_1: 89;

            then

             A19: (Lxy . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . (x + y))) & (Lx . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . x)) & (Ly . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . y)) by A15, A16, A17;

            ( diff ((( Proj (i,n)) * g),x0)) is LinearOperator of ( REAL-NS m), ( REAL-NS 1) by LOPBAN_1:def 9;

            then

             A20: (( diff ((( Proj (i,n)) * g),x0)) . (x + y)) = ((( diff ((( Proj (i,n)) * g),x0)) . x) + (( diff ((( Proj (i,n)) * g),x0)) . y)) by VECTSP_1:def 20;

            reconsider Diffxy = (( diff ((( Proj (i,n)) * g),x0)) . (x + y)) as Element of ( REAL 1) by REAL_NS1:def 4;

            reconsider Diffx = (( diff ((( Proj (i,n)) * g),x0)) . x) as Element of ( REAL 1) by REAL_NS1:def 4;

            reconsider Diffy = (( diff ((( Proj (i,n)) * g),x0)) . y) as Element of ( REAL 1) by REAL_NS1:def 4;

            Diffxy = (Diffx + Diffy) by A20, REAL_NS1: 2;

            then (Lxy . i0) = ((Diffx + Diffy) . 1) by A19, PDIFF_1:def 1;

            then (Lxy . i0) = ((Diffx . 1) + (Diffy . 1)) by RVSUM_1: 11;

            then (Lxy . i0) = ((Lx . i0) + (Diffy . 1)) by A19, PDIFF_1:def 1;

            then (Lxy . i0) = ((Lx . i0) + (Ly . i0)) by A19, PDIFF_1:def 1;

            hence thesis by RVSUM_1: 11;

          end;

          then Lxy = (Lx + Ly) by A18, FINSEQ_1: 13;

          hence thesis by A15, A16, A17, REAL_NS1: 2;

        end;

        for x be VECTOR of ( REAL-NS m), r be Real holds (L . (r * x)) = (r * (L . x))

        proof

          let x be VECTOR of ( REAL-NS m), r be Real;

          consider Lx be Element of ( REAL n) such that

           A21: (L . x) = Lx & for i be Nat st i in ( Seg n) holds (Lx . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . x)) by A13;

          consider Lrx be Element of ( REAL n) such that

           A22: (L . (r * x)) = Lrx & for i be Nat st i in ( Seg n) holds (Lrx . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . (r * x))) by A13;

          ( dom (r * Lx)) = ( Seg n) by FINSEQ_1: 89;

          then

           A23: ( dom (r * Lx)) = ( dom Lrx) by FINSEQ_1: 89;

          for i0 be Nat st i0 in ( dom (r * Lx)) holds ((r * Lx) . i0) = (Lrx . i0)

          proof

            let i0 be Nat;

            reconsider i = i0 as Nat;

            assume i0 in ( dom (r * Lx));

            then i0 in ( Seg n) by FINSEQ_1: 89;

            then

             A24: (Lx . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . x)) & (Lrx . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . (r * x))) by A21, A22;

            ( diff ((( Proj (i,n)) * g),x0)) is LinearOperator of ( REAL-NS m), ( REAL-NS 1) by LOPBAN_1:def 9;

            then

             A25: (( diff ((( Proj (i,n)) * g),x0)) . (r * x)) = (r * (( diff ((( Proj (i,n)) * g),x0)) . x)) by LOPBAN_1:def 5;

            reconsider Diffrx = (( diff ((( Proj (i,n)) * g),x0)) . (r * x)) as Element of ( REAL 1) by REAL_NS1:def 4;

            reconsider Diffx = (( diff ((( Proj (i,n)) * g),x0)) . x) as Element of ( REAL 1) by REAL_NS1:def 4;

            Diffrx = (r * Diffx) by A25, REAL_NS1: 3;

            then (Lrx . i0) = ((r * Diffx) . 1) by A24, PDIFF_1:def 1;

            then (Lrx . i0) = (r * (Diffx . 1)) by RVSUM_1: 45;

            then (Lrx . i0) = (r * (Lx . i0)) by A24, PDIFF_1:def 1;

            hence thesis by RVSUM_1: 45;

          end;

          then (r * Lx) = Lrx by A23, FINSEQ_1: 13;

          hence thesis by A21, A22, REAL_NS1: 3;

        end;

        then

        reconsider L as LinearOperator of ( REAL-NS m), ( REAL-NS n) by A14, LOPBAN_1:def 5, VECTSP_1:def 20;

        reconsider L0 = L as Point of RB by LOPBAN_1:def 9;

        deffunc RD( Element of ( REAL-NS m)) = (((g /. ($1 + x0)) - (g /. x0)) - (L . $1));

        consider R be Function of ( REAL-NS m), ( REAL-NS n) such that

         A26: for x be Element of ( REAL-NS m) holds (R . x) = RD(x) from FUNCT_2:sch 4;

        

         A27: for x be Element of ( REAL-NS m), i be Nat st i in ( Seg n) & (x + x0) in ( dom g) holds ((( Proj (i,n)) * R) . x) = ((((( Proj (i,n)) * g) /. (x + x0)) - ((( Proj (i,n)) * g) /. x0)) - ((( Proj (i,n)) * L) . x))

        proof

          let x be Element of ( REAL-NS m), i be Nat;

          assume that

           A28: i in ( Seg n) and

           A29: (x + x0) in ( dom g);

          (x0 - x0) = ( 0. ( REAL-NS m)) by RLVECT_1: 15;

          then (x0 - x0) = ( 0* m) by REAL_NS1:def 4;

          then ||.(x0 - x0).|| = |.( 0* m).| by REAL_NS1: 1;

          then

           A30: ||.(x0 - x0).|| = 0 by EUCLID: 7;

          

           A31: 0 < (d /. i) & { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < (d /. i) } c= ( dom (( Proj (i,n)) * g)) by A28, A6;

          then x0 in { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < (d /. i) } by A30;

          then

           A32: x0 in ( dom (( Proj (i,n)) * g)) by A31;

          

           A33: ( dom (( Proj (i,n)) * g)) c= ( dom g) by RELAT_1: 25;

          reconsider gxx0 = (g /. (x + x0)), gx0 = (g /. x0), Lx = (L . x) as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider Lx1 = (L . x) as Point of ( REAL-NS n);

          

           A34: ( - gx0) = (( - 1) * (g /. x0)) & ( - Lx) = (( - 1) * (L . x)) by REAL_NS1: 3;

          then (gxx0 + ( - gx0)) = ((g /. (x + x0)) + (( - 1) * (g /. x0))) by REAL_NS1: 2;

          then

           A35: ((gxx0 + ( - gx0)) + ( - Lx)) = (((g /. (x + x0)) + (( - 1) * (g /. x0))) + (( - 1) * (L . x))) by A34, REAL_NS1: 2;

          (gxx0 - gx0) = ((g /. (x + x0)) - (g /. x0)) by REAL_NS1: 5;

          then

           A36: (((g /. (x + x0)) - (g /. x0)) - (L . x)) = ((gxx0 - gx0) - Lx) by REAL_NS1: 5;

          ((( Proj (i,n)) * R) . x) = (( Proj (i,n)) . (R . x)) by FUNCT_2: 15;

          then ((( Proj (i,n)) * R) . x) = (( Proj (i,n)) . (((g /. (x + x0)) - (g /. x0)) - (L . x))) by A26;

          then ((( Proj (i,n)) * R) . x) = ((( Proj (i,n)) . ((g /. (x + x0)) + (( - 1) * (g /. x0)))) + (( Proj (i,n)) . (( - 1) * (L . x)))) by A36, A35, Th26;

          then

           A37: ((( Proj (i,n)) * R) . x) = (((( Proj (i,n)) . (g /. (x + x0))) + (( Proj (i,n)) . (( - 1) * (g /. x0)))) + (( Proj (i,n)) . (( - 1) * (L . x)))) by Th26;

          (( Proj (i,n)) . (( - 1) * (g /. x0))) = (( - 1) * (( Proj (i,n)) . (g /. x0))) & (( Proj (i,n)) . (( - 1) * Lx1)) = (( - 1) * (( Proj (i,n)) . Lx1)) by Th27;

          then ((( Proj (i,n)) * R) . x) = (((( Proj (i,n)) . (g /. (x + x0))) + ( - (( Proj (i,n)) . (g /. x0)))) + (( - 1) * (( Proj (i,n)) . (L . x)))) by A37, RLVECT_1: 16;

          then ((( Proj (i,n)) * R) . x) = (((( Proj (i,n)) . (g /. (x + x0))) + ( - (( Proj (i,n)) . (g /. x0)))) + ( - (( Proj (i,n)) . (L . x)))) by RLVECT_1: 16;

          then ((( Proj (i,n)) * R) . x) = (((( Proj (i,n)) . (g /. (x + x0))) - (( Proj (i,n)) . (g /. x0))) + ( - (( Proj (i,n)) . (L . x)))) by RLVECT_1:def 11;

          then

           A38: ((( Proj (i,n)) * R) . x) = (((( Proj (i,n)) . (g /. (x + x0))) - (( Proj (i,n)) . (g /. x0))) - (( Proj (i,n)) . (L . x))) by RLVECT_1:def 11;

          (g /. (x + x0)) in the carrier of ( REAL-NS n) & (g /. x0) in the carrier of ( REAL-NS n);

          then

           A39: (g /. (x + x0)) in ( dom ( Proj (i,n))) & (g /. x0) in ( dom ( Proj (i,n))) by FUNCT_2:def 1;

          

           A40: (( Proj (i,n)) . (g /. (x + x0))) = (( Proj (i,n)) /. (g /. (x + x0)))

          .= ((( Proj (i,n)) * g) /. (x + x0)) by A29, A39, PARTFUN2: 4;

          (( Proj (i,n)) . (g /. x0)) = (( Proj (i,n)) /. (g /. x0))

          .= ((( Proj (i,n)) * g) /. x0) by A32, A33, A39, PARTFUN2: 4;

          hence thesis by A38, A40, FUNCT_2: 15;

        end;

        for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r

        proof

          let r be Real;

          assume

           A41: r > 0 ;

          set r0 = ((( sqrt n) " ) * r);

          

           A42: ( sqrt n) > 0 by SQUARE_1: 25;

          then

           A43: r0 > 0 by A41, XREAL_1: 129;

          defpred DD[ Nat, Element of REAL ] means $2 > 0 & for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < $2 holds (( ||.z.|| " ) * ||.((( Proj ($1,n)) * R) /. z).||) < r0;

          

           A44: for k be Nat st k in ( Seg n) holds ex dd be Element of REAL st DD[k, dd]

          proof

            let k be Nat;

            assume

             A45: k in ( Seg n);

            then 1 <= k & k <= n by FINSEQ_1: 1;

            then (( Proj (k,n)) * g) is_differentiable_in x0 by A1;

            then

            consider Nk be Neighbourhood of x0 such that

             A46: Nk c= ( dom (( Proj (k,n)) * g)) & ex PR be RestFunc of ( REAL-NS m), ( REAL-NS 1) st for x be Point of ( REAL-NS m) st x in Nk holds (((( Proj (k,n)) * g) /. x) - ((( Proj (k,n)) * g) /. x0)) = ((( diff ((( Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0))) by NDIFF_1:def 7;

            consider d0 be Real such that

             A47: 0 < d0 & { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < d0 } c= Nk by NFCONT_1:def 1;

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

             A48: for x be Point of ( REAL-NS m) st x in Nk holds (((( Proj (k,n)) * g) /. x) - ((( Proj (k,n)) * g) /. x0)) = ((( diff ((( Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0))) by A46;

            PR is total by NDIFF_1:def 5;

            then

            consider d1 be Real such that

             A49: d1 > 0 & for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < d1 holds (( ||.z.|| " ) * ||.(PR /. z).||) < r0 by A43, NDIFF_1: 23;

            reconsider d0, d1 as Real;

            reconsider dd = ( min (d0,d1)) as Element of REAL by XREAL_0:def 1;

            take dd;

            for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < dd holds (( ||.z.|| " ) * ||.((( Proj (k,n)) * R) /. z).||) < r0

            proof

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

              assume

               A50: z <> ( 0. ( REAL-NS m)) & ||.z.|| < dd;

              dd <= d1 by XXREAL_0: 17;

              then ||.z.|| < d1 by A50, XXREAL_0: 2;

              then

               A51: (( ||.z.|| " ) * ||.(PR /. z).||) < r0 by A50, A49;

              dd <= d0 by XXREAL_0: 17;

              then

               A52: ||.z.|| < d0 by A50, XXREAL_0: 2;

              

               A53: ((z + x0) - x0) = z by RLVECT_4: 1;

              then

               A54: (z + x0) in { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < d0 } by A52;

              then (z + x0) in Nk by A47;

              then

               A55: (z + x0) in ( dom (( Proj (k,n)) * g)) by A46;

              (((( Proj (k,n)) * g) /. (z + x0)) - ((( Proj (k,n)) * g) /. x0)) = ((( diff ((( Proj (k,n)) * g),x0)) . ((z + x0) - x0)) + (PR /. ((z + x0) - x0))) by A54, A47, A48;

              then

               A56: (PR /. z) = ((((( Proj (k,n)) * g) /. (z + x0)) - ((( Proj (k,n)) * g) /. x0)) - (( diff ((( Proj (k,n)) * g),x0)) . z)) by A53, RLVECT_4: 1;

              ( dom (( Proj (k,n)) * g)) c= ( dom g) by RELAT_1: 25;

              then

               A57: ((( Proj (k,n)) * R) . z) = ((((( Proj (k,n)) * g) /. (z + x0)) - ((( Proj (k,n)) * g) /. x0)) - ((( Proj (k,n)) * L) . z)) by A55, A45, A27;

              consider y be Element of ( REAL n) such that

               A58: (L . z) = y & for i be Nat st i in ( Seg n) holds (y . i) = (( proj (1,1)) . (( diff ((( Proj (i,n)) * g),x0)) . z)) by A13;

              

               A59: (y . k) = (( proj (1,1)) . (( diff ((( Proj (k,n)) * g),x0)) . z)) by A58, A45;

              (( diff ((( Proj (k,n)) * g),x0)) . z) is Element of ( REAL 1) by REAL_NS1:def 4;

              then

              consider Dk be Element of REAL such that

               A60: (( diff ((( Proj (k,n)) * g),x0)) . z) = <*Dk*> by FINSEQ_2: 97;

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

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

              then ((( Proj (k,n)) * L) . z) = (( Proj (k,n)) . (L . z)) by FUNCT_1: 13;

              then ((( Proj (k,n)) * L) . z) = <*(( proj (k,n)) . y1)*> by A58, PDIFF_1:def 4;

              then ((( Proj (k,n)) * L) . z) = <*(( proj (1,1)) . (( diff ((( Proj (k,n)) * g),x0)) . z))*> by A59, PDIFF_1:def 1;

              hence thesis by A51, A56, A57, A60, PDIFF_1: 1;

            end;

            hence thesis by A47, A49, XXREAL_0: 21;

          end;

          consider dd be FinSequence of REAL such that

           A61: ( dom dd) = ( Seg n) & for i be Nat st i in ( Seg n) holds DD[i, (dd /. i)] from RECDEF_1:sch 17( A44);

          set d = ( min dd);

          take d;

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

          ( len dd) = nn by A61, FINSEQ_1:def 3;

          then

           A62: ( min_p dd) in ( dom dd) by RFINSEQ2:def 2;

          then

           A63: (dd /. ( min_p dd)) > 0 by A61;

          for z be Point of ( REAL-NS m) st z <> ( 0. ( REAL-NS m)) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r

          proof

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

            assume

             A64: z <> ( 0. ( REAL-NS m)) & ||.z.|| < d;

            reconsider Rz = (R /. z) as Element of ( REAL n) by REAL_NS1:def 4;

            reconsider zr = (( ||.z.|| * r0) ^2 ) as Element of REAL by XREAL_0:def 1;

            reconsider R0 = (n |-> zr) as Element of (n -tuples_on REAL );

            reconsider SRz = ( sqr Rz) as Element of (n -tuples_on REAL );

             ||.z.|| <> 0 by A64, NORMSP_0:def 5;

            then

             A65: ||.z.|| > 0 by NORMSP_1: 4;

            

             A66: for i0 be Nat st i0 in ( Seg n) holds (SRz . i0) < (R0 . i0)

            proof

              let i0 be Nat;

              reconsider i = i0 as Nat;

              assume

               A67: i0 in ( Seg n);

              then i in ( dom Rz) by FINSEQ_2: 124;

              then (( sqr Rz) . i) = ( sqrreal . (Rz . i)) by FUNCT_1: 13;

              then

               A68: (( sqr Rz) . i) = ((Rz . i) ^2 ) by RVSUM_1:def 2;

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

              1 <= i & i <= nn by A67, FINSEQ_1: 1;

              then 1 <= i & i <= ( len dd) by A61, FINSEQ_1:def 3;

              then d <= (dd . i) by RFINSEQ2: 2;

              then d <= (dd /. i) by A67, A61, PARTFUN1:def 6;

              then ||.z.|| < (dd /. i) by A64, XXREAL_0: 2;

              then (( ||.z.|| " ) * ||.((( Proj (i,n)) * R) /. z).||) < r0 by A64, A67, A61;

              then

               A69: ||.((( Proj (i,n)) * R) /. z).|| < (r0 / ( ||.z.|| " )) by A65, XREAL_1: 81;

              (Rz . i) in REAL by XREAL_0:def 1;

              then

              reconsider Rzi = <*(Rz . i)*> as Element of ( REAL 1) by FINSEQ_2: 98;

              ((( Proj (i,n)) * R) . z) = (( Proj (i,n)) . (R . z)) by FUNCT_2: 15;

              then ((( Proj (i,n)) * R) . z) = <*(( proj (i,n)) . Rz)*> by PDIFF_1:def 4;

              then ((( Proj (i,n)) * R) . z) = <*(Rz . i)*> by PDIFF_1:def 1;

              then ||.((( Proj (i,n)) * R) . z).|| = |.Rzi.| by REAL_NS1: 1;

              then |.(Rz . i).| < ( ||.z.|| * r0) by A69, JORDAN2C: 10;

              then ( |.(Rz . i).| ^2 ) < (( ||.z.|| * r0) ^2 ) by COMPLEX1: 46, SQUARE_1: 16;

              then ((Rz . i0) ^2 ) < (( ||.z.|| * r0) ^2 ) by COMPLEX1: 75;

              hence thesis by A67, A68, FINSEQ_2: 57;

            end;

            

             A70: for i be Nat st i in ( dom ( sqr Rz)) holds 0 <= (( sqr Rz) . i)

            proof

              let i be Nat;

              assume i in ( dom ( sqr Rz));

              then i in ( dom ( sqrreal * Rz)) & ( dom ( sqrreal * Rz)) c= ( dom Rz) by RELAT_1: 25;

              then (( sqr Rz) . i) = ( sqrreal . (Rz . i)) by FUNCT_1: 13;

              then (( sqr Rz) . i) = ((Rz . i) ^2 ) by RVSUM_1:def 2;

              hence thesis by XREAL_1: 63;

            end;

            

             A71: (( ||.z.|| * r0) ^2 ) >= 0 by XREAL_1: 63;

            

             A72: ex i be Nat st i in ( Seg n) & (SRz . i) < (R0 . i)

            proof

              take 1;

              1 <= n by NAT_1: 14;

              hence 1 in ( Seg n);

              hence (SRz . 1) < (R0 . 1) by A66;

            end;

            

             A73: ( sqrt n) > 0 by SQUARE_1: 25;

            for i0 be Nat st i0 in ( Seg n) holds (SRz . i0) <= (R0 . i0) by A66;

            then ( Sum SRz) < ( Sum R0) by A72, RVSUM_1: 83;

            then ( Sum ( sqr Rz)) < (n * (( ||.z.|| * r0) ^2 )) by RVSUM_1: 80;

            then |.Rz.| < ( sqrt (n * (( ||.z.|| * r0) ^2 ))) by A70, RVSUM_1: 84, SQUARE_1: 27;

            then |.Rz.| < (( sqrt n) * ( sqrt (( ||.z.|| * r0) ^2 ))) by A71, SQUARE_1: 29;

            then |.Rz.| < (( sqrt n) * |.( ||.z.|| * r0).|) by COMPLEX1: 72;

            then |.Rz.| < (( sqrt n) * ( ||.z.|| * r0)) by A42, A41, A65, ABSVALUE:def 1;

            then |.Rz.| < ((( sqrt n) * r0) * ||.z.||);

            then ( |.Rz.| / ||.z.||) < (( sqrt n) * r0) by A65, XREAL_1: 83;

            then (( ||.z.|| " ) * ||.(R /. z).||) < ((( sqrt n) * (( sqrt n) " )) * r) by REAL_NS1: 1;

            then (( ||.z.|| " ) * ||.(R /. z).||) < (1 * r) by A73, XCMPLX_0:def 7;

            hence (( ||.z.|| " ) * ||.(R /. z).||) < r;

          end;

          hence thesis by A63, A62, PARTFUN1:def 6;

        end;

        then

        reconsider R as RestFunc of ( REAL-NS m), ( REAL-NS n) by NDIFF_1: 23;

        set N = { y where y be Point of ( REAL-NS m) : ||.(y - x0).|| < d0 };

        reconsider N as Neighbourhood of x0 by A8, NFCONT_1: 3;

        now

          let x be object;

          assume x in N;

          then

          consider y be Point of ( REAL-NS m) such that

           A74: x = y & ||.(y - x0).|| < d0;

          1 <= n by NAT_1: 14;

          then

           A75: 1 in ( Seg n) & 1 in ( dom d) by A6;

          then

           A76: { z where z be Point of ( REAL-NS m) : ||.(z - x0).|| < (d /. 1) } c= ( dom (( Proj (1,n)) * g)) by A6;

          ( dom (( Proj (1,n)) * g)) c= ( dom g) by RELAT_1: 25;

          then

           A77: { z where z be Point of ( REAL-NS m) : ||.(z - x0).|| < (d /. 1) } c= ( dom g) by A76, XBOOLE_1: 1;

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

          ( len d) = nn by A6, FINSEQ_1:def 3;

          then 1 <= ( len d) by NAT_1: 14;

          then d0 <= (d . 1) by RFINSEQ2: 2;

          then d0 <= (d /. 1) by A75, PARTFUN1:def 6;

          then ||.(y - x0).|| < (d /. 1) by A74, XXREAL_0: 2;

          then y in { z where z be Point of ( REAL-NS m) : ||.(z - x0).|| < (d /. 1) };

          hence x in ( dom g) by A74, A77;

        end;

        then

         A78: N c= ( dom g) by TARSKI:def 3;

        ex L be Point of RB, R be RestFunc of ( REAL-NS m), ( REAL-NS n) st for x be Point of ( REAL-NS m) st x in N holds ((g /. x) - (g /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

        proof

          take L0;

          take R;

          hereby

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

            assume x in N;

            

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

            (R . (x - x0)) = (((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0))) by A26;

            then (R . (x - x0)) = (((g /. (x - (x0 - x0))) - (g /. x0)) - (L0 . (x - x0))) by RLVECT_1: 29;

            then (R . (x - x0)) = (((g /. (x - (x0 + ( - x0)))) - (g /. x0)) - (L0 . (x - x0))) by RLVECT_1:def 11;

            then (R . (x - x0)) = (((g /. (x - ( 0. ( REAL-NS m)))) - (g /. x0)) - (L0 . (x - x0))) by RLVECT_1: 5;

            then (R . (x - x0)) = (((g /. x) - (g /. x0)) - (L0 . (x - x0))) by RLVECT_1: 13;

            then (R . (x - x0)) = (((g /. x) - (g /. x0)) + ( - (L0 . (x - x0)))) by RLVECT_1:def 11;

            then (R /. (x - x0)) = (((g /. x) - (g /. x0)) + ( - (L0 . (x - x0)))) by A79, PARTFUN1:def 6;

            then ((L0 . (x - x0)) + (R /. (x - x0))) = (((g /. x) - (g /. x0)) + (( - (L0 . (x - x0))) + (L0 . (x - x0)))) by RLVECT_1:def 3;

            then ((L0 . (x - x0)) + (R /. (x - x0))) = (((g /. x) - (g /. x0)) + ( 0. ( REAL-NS n))) by RLVECT_1: 5;

            hence ((g /. x) - (g /. x0)) = ((L0 . (x - x0)) + (R /. (x - x0))) by RLVECT_1: 4;

          end;

        end;

        hence thesis by A78, NDIFF_1:def 6;

      end;

      hence thesis by Th28;

    end;

    definition

      let X be set;

      let n,m be non zero Nat;

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

      :: PDIFF_6:def4

      pred f is_differentiable_on X means X c= ( dom f) & for x be Element of ( REAL m) st x in X holds (f | X) is_differentiable_in x;

    end

    theorem :: PDIFF_6:30

    

     Th30: for X be set, m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n) st f = g holds f is_differentiable_on X iff g is_differentiable_on X

    proof

      let X be set, m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n);

      assume

       A1: f = g;

       A2:

      now

        assume

         A3: f is_differentiable_on X;

        then

         A4: X c= ( dom f) & for x be Element of ( REAL m) st x in X holds (f | X) is_differentiable_in x;

        now

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

          reconsider x = y as Element of ( REAL m) by REAL_NS1:def 4;

          assume y in X;

          then (f | X) is_differentiable_in x by A3;

          then ex g be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st (f | X) = g & x = y & g is_differentiable_in y by PDIFF_1:def 7;

          hence (g | X) is_differentiable_in y by A1;

        end;

        hence g is_differentiable_on X by A1, A4, NDIFF_1:def 8;

      end;

      now

        assume

         A5: g is_differentiable_on X;

        hence X c= ( dom f) by A1, NDIFF_1:def 8;

        

         A6: X c= ( dom g) & for x be Point of ( REAL-NS m) st x in X holds (g | X) is_differentiable_in x by A5, NDIFF_1:def 8;

        now

          let y be Element of ( REAL m);

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

          assume y in X;

          then (g | X) is_differentiable_in x by A5, NDIFF_1:def 8;

          hence (f | X) is_differentiable_in y by A1, PDIFF_1:def 7;

        end;

        hence f is_differentiable_on X by A1, A6;

      end;

      hence thesis by A2;

    end;

    theorem :: PDIFF_6:31

    for X be set, m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n) holds f is_differentiable_on X implies X is Subset of ( REAL m) by XBOOLE_1: 1;

    theorem :: PDIFF_6:32

    for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), Z be Subset of ( REAL m) st ex Z0 be Subset of ( REAL-NS m) st Z = Z0 & Z0 is open holds (f is_differentiable_on Z iff Z c= ( dom f) & for x be Element of ( REAL m) st x in Z holds f is_differentiable_in x)

    proof

      let m,n be non zero Nat;

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

      let Z be Subset of ( REAL m);

      assume ex Z0 be Subset of ( REAL-NS m) st Z = Z0 & Z0 is open;

      then

      consider Z0 be Subset of ( REAL-NS m) such that

       A1: Z = Z0 & Z0 is open;

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

      then

      reconsider g = f as PartFunc of ( REAL-NS m), ( REAL-NS n);

      

       A2: g is_differentiable_on Z0 iff Z0 c= ( dom g) & for x be Point of ( REAL-NS m) st x in Z0 holds g is_differentiable_in x by A1, NDIFF_1: 31;

      thus f is_differentiable_on Z implies Z c= ( dom f) & for x be Element of ( REAL m) st x in Z holds f is_differentiable_in x by A1, A2, Th30, PDIFF_1:def 7;

      assume

       A3: Z c= ( dom f) & for x be Element of ( REAL m) st x in Z holds f is_differentiable_in x;

      now

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

        reconsider x = y as Element of ( REAL m) by REAL_NS1:def 4;

        assume y in Z0;

        then f is_differentiable_in x by A1, A3;

        then 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 by PDIFF_1:def 7;

        hence g is_differentiable_in y;

      end;

      hence f is_differentiable_on Z by A1, A2, A3, Th30;

    end;

    theorem :: PDIFF_6:33

    for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), Z be Subset of ( REAL m) st f is_differentiable_on Z holds ex Z0 be Subset of ( REAL-NS m) st Z = Z0 & Z0 is open

    proof

      let m,n be non zero Nat;

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

      assume

       A1: f is_differentiable_on Z;

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

      then

      reconsider g = f as PartFunc of ( REAL-NS m), ( REAL-NS n);

      reconsider Z0 = Z as Subset of ( REAL-NS m) by REAL_NS1:def 4;

      take Z0;

      g is_differentiable_on Z0 by A1, Th30;

      hence thesis by NDIFF_1: 32;

    end;