pdiff_7.miz

    begin

    reserve n for Nat,

p,p1,p2 for Point of ( TOP-REAL n),

x for Real;

    registration

      let n be Nat;

      let p,q be Element of ( TOP-REAL n);

      let f,g be real-valued FinSequence;

      identify f + g with p + q when p = f, q = g;

      compatibility ;

    end

    registration

      let r,s be Real;

      let n be Nat;

      let p be Element of ( TOP-REAL n);

      let f be real-valued FinSequence;

      identify s * f with r * p when r = s, p = f;

      compatibility ;

    end

    registration

      let n be Nat;

      let p be Element of ( TOP-REAL n);

      let f be real-valued FinSequence;

      identify - f with - p when p = f;

      compatibility ;

    end

    registration

      let n be Nat;

      let p,q be Element of ( TOP-REAL n);

      let f,g be real-valued FinSequence;

      identify f - g with p - q when p = f, q = g;

      compatibility ;

    end

    reserve n,m for non zero Nat;

    reserve i,j for Nat;

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

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

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

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

    reserve y for Element of ( REAL m);

    reserve X for set;



     Lm1: for S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x holds (N1 /\ N2) is Neighbourhood of x

    proof

      let S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x;

      consider N be Neighbourhood of x such that

       A1: N c= N1 & N c= N2 by NDIFF_1: 1;



       A2: N c= (N1 /\ N2) by A1, XBOOLE_1: 19;

      consider g be Real such that

       A3: 0 < g and

       A4: { y where y be Point of S : ||.(y - x).|| < g } c= N by NFCONT_1:def 1;

      { y where y be Point of S : ||.(y - x).|| < g } c= (N1 /\ N2) by A2, A4;

      hence thesis by A3, NFCONT_1:def 1;

    end;



     Lm2: i <= j implies (i + (j -' i)) = ((i + j) -' i)

    proof

      assume i <= j;

      then 0 <= (j - i) by XREAL_1: 48;

      then

       A1: (j -' i) = (j - i) by XREAL_0:def 2;

      ((i + j) -' i) = ((i + j) - i) by XREAL_0:def 2;

      hence thesis by A1;

    end;

    theorem :: PDIFF_7:1



     Th1: i <= j implies (( 0* j) | i) = ( 0* i)

    proof

      assume

       A1: i <= j;



       A2: ((( 0* i) ^ ( 0* (j -' i))) | ( len ( 0* i))) = ( 0* i) by FINSEQ_5: 23;

      (i + (j -' i)) = ((i + j) -' i) by A1, Lm2;

      then (i + (j -' i)) = ((i + j) - i) by XREAL_0:def 2;

      then (( 0* i) ^ ( 0* (j -' i))) = ( 0* j) by FINSEQ_2: 123;

      hence thesis by A2, CARD_1:def 7;

    end;

    theorem :: PDIFF_7:2



     Th2: i <= j implies (( 0* j) | (i -' 1)) = ( 0* (i -' 1))

    proof

      assume i <= j;

      then

       A1: (i - 1) <= (j - 1) by XREAL_1: 9;

      (j - 1) <= j by XREAL_1: 43;

      then (i - 1) <= j by A1, XXREAL_0: 2;

      then (i -' 1) <= j by XREAL_0:def 2;

      hence thesis by Th1;

    end;



     Lm3: i <= j implies (( 0* j) /^ i) = ( 0* (j -' i))

    proof

      assume

       A1: i <= j;

      ( len (( 0* j) /^ i)) = (( len ( 0* j)) -' i) by RFINSEQ: 29;

      then

       A2: ( len (( 0* j) /^ i)) = (j -' i) by CARD_1:def 7;



       A3: ( len ( 0* (j -' i))) = (j -' i) by CARD_1:def 7;



       A4: i <= ( len ( 0* j)) by A1, CARD_1:def 7;

      for k be Nat st 1 <= k & k <= ( len (( 0* j) /^ i)) holds ((( 0* j) /^ i) . k) = (( 0* (j -' i)) . k)

      proof

        let k be Nat;

        assume

         A5: 1 <= k & k <= ( len (( 0* j) /^ i));

        k in ( dom (( 0* j) /^ i)) by A5, FINSEQ_3: 25;

        then ((( 0* j) /^ i) . k) = (( 0* j) . (k + i)) by A4, RFINSEQ:def 1;

        then

         A6: ((( 0* j) /^ i) . k) = 0 ;

        thus thesis by A6;

      end;

      hence thesis by A2, A3;

    end;



     Lm4: i > j implies (( 0* j) /^ i) = ( 0* (j -' i))

    proof

      assume

       A1: i > j;

      then

       A2: i > ( len ( 0* j)) by CARD_1:def 7;

       0 > (j - i) by A1, XREAL_1: 49;

      then

       A3: (j -' i) = 0 by XREAL_0:def 2;

      (( 0* j) /^ i) = 0 by A2, RFINSEQ:def 1;

      hence thesis by A3;

    end;

    theorem :: PDIFF_7:3



     Th3: (( 0* j) /^ i) = ( 0* (j -' i))

    proof

      per cases ;

        suppose i <= j;

        hence thesis by Lm3;

      end;

        suppose i > j;

        hence thesis by Lm4;

      end;

    end;

    theorem :: PDIFF_7:4

    (i <= j implies (( 0* j) | (i -' 1)) = ( 0* (i -' 1))) & (( 0* j) /^ i) = ( 0* (j -' i)) by Th2, Th3;

    theorem :: PDIFF_7:5



     Th5: for xi be Element of ( REAL-NS 1) st 1 <= i & i <= j holds ||.(( reproj (i,( 0. ( REAL-NS j)))) . xi).|| = ||.xi.||

    proof

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

      assume

       A1: 1 <= i & i <= j;

      consider q be Element of REAL , y be Element of ( REAL j) such that

       A2: xi = <*q*> & y = ( 0. ( REAL-NS j)) & (( reproj (i,( 0. ( REAL-NS j)))) . xi) = (( reproj (i,y)) . q) by PDIFF_1:def 6;



       A3: (( reproj (i,( 0. ( REAL-NS j)))) . xi) = ( Replace (y,i,q)) by A2, PDIFF_1:def 5;

      ( len y) = j by CARD_1:def 7;

      then (( reproj (i,( 0. ( REAL-NS j)))) . xi) = (((y | (i -' 1)) ^ <*q*>) ^ (y /^ i)) by A1, A3, FINSEQ_7:def 1;

      then

       A4: ||.(( reproj (i,( 0. ( REAL-NS j)))) . xi).|| = |.(((y | (i -' 1)) ^ <*q*>) ^ (y /^ i)).| by A2, REAL_NS1: 1;

      (y | (i -' 1)) = (( 0* j) | (i -' 1)) by A2, REAL_NS1:def 4;

      then ( sqrt ( Sum ( sqr (y | (i -' 1))))) = |.( 0* (i -' 1)).| by A1, Th2;

      then ( sqrt ( Sum ( sqr (y | (i -' 1))))) = 0 by EUCLID: 7;

      then

       A5: ( Sum ( sqr (y | (i -' 1)))) = 0 by RVSUM_1: 86, SQUARE_1: 24;

      (y /^ i) = (( 0* j) /^ i) by A2, REAL_NS1:def 4;

      then ( sqrt ( Sum ( sqr (y /^ i)))) = |.( 0* (j -' i)).| by Th3;

      then

       A6: ( sqrt ( Sum ( sqr (y /^ i)))) = 0 by EUCLID: 7;

      reconsider q2 = (q ^2 ) as Real;

      ( sqr (((y | (i -' 1)) ^ <*q*>) ^ (y /^ i))) = (( sqr ((y | (i -' 1)) ^ <*q*>)) ^ ( sqr (y /^ i))) by RVSUM_1: 144

      .= ((( sqr (y | (i -' 1))) ^ ( sqr <*q*>)) ^ ( sqr (y /^ i))) by RVSUM_1: 144

      .= ((( sqr (y | (i -' 1))) ^ <*(q ^2 )*>) ^ ( sqr (y /^ i))) by RVSUM_1: 55;



      then ( Sum ( sqr (((y | (i -' 1)) ^ <*q*>) ^ (y /^ i)))) = (( Sum (( sqr (y | (i -' 1))) ^ <*q2*>)) + ( Sum ( sqr (y /^ i)))) by RVSUM_1: 75

      .= ((( Sum ( sqr (y | (i -' 1)))) + (q ^2 )) + ( Sum ( sqr (y /^ i)))) by RVSUM_1: 74

      .= (q ^2 ) by A5, A6, RVSUM_1: 86, SQUARE_1: 24;

      then

       A7: ||.(( reproj (i,( 0. ( REAL-NS j)))) . xi).|| = |.q.| by A4, COMPLEX1: 72;

      (( proj (1,1)) . <*q*>) = q by PDIFF_1: 1;

      hence thesis by A7, A2, PDIFF_1: 4;

    end;

    theorem :: PDIFF_7:6



     Th6: for m,i be Nat, x be Element of ( REAL m), r be Real holds ((( reproj (i,x)) . r) - x) = (( reproj (i,( 0* m))) . (r - (( proj (i,m)) . x))) & (x - (( reproj (i,x)) . r)) = (( reproj (i,( 0* m))) . ((( proj (i,m)) . x) - r))

    proof

      let m,i be Nat, x be Element of ( REAL m), r1 be Real;

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

      reconsider rr = (r - (( proj (i,m)) . x)) as Element of REAL ;

      reconsider rs = ((( proj (i,m)) . x) - r) as Element of REAL ;

      reconsider p = ((( reproj (i,x)) . r) - x) as m -element FinSequence;

      reconsider q = (( reproj (i,( 0* m))) . rr) as m -element FinSequence;

      reconsider s = (x - (( reproj (i,x)) . r)) as m -element FinSequence;

      reconsider t = (( reproj (i,( 0* m))) . rs) as m -element FinSequence;



       A1: ( dom p) = ( Seg m) & ( dom q) = ( Seg m) & ( dom s) = ( Seg m) & ( dom t) = ( Seg m) & ( dom x) = ( Seg m) & ( dom ( 0* m)) = ( Seg m) by FINSEQ_1: 89;

      reconsider x1 = x as Element of (m -tuples_on REAL );



       A2: (( reproj (i,x)) . r) = ( Replace (x,i,r)) by PDIFF_1:def 5;

      reconsider y1 = (( reproj (i,x)) . r) as Element of (m -tuples_on REAL );

      reconsider mm = m as Element of NAT by ORDINAL1:def 12;



       A3: ( len x) = mm & ( len ( 0* m)) = mm by A1, FINSEQ_1:def 3;

      then

       A4: ( len ( Replace (x,i,r))) = m by FINSEQ_7: 5;

      for k be Nat st k in ( dom p) holds (p . k) = (q . k)

      proof

        let k be Nat;

        assume

         A5: k in ( dom p);

        then

         A6: 1 <= k & k <= m by A1, FINSEQ_1: 1;

        then k in ( dom ( Replace (x,i,r))) by A4, FINSEQ_3: 25;

        then

         A7: (( Replace (x,i,r)) /. k) = (( Replace (x,i,r)) . k) by PARTFUN1:def 6;



         A8: (p . k) = ((y1 . k) - (x1 . k)) by RVSUM_1: 27;

        q = ( Replace (( 0* m),i,rr)) by PDIFF_1:def 5;

        then

         A9: (q . k) = (( Replace (( 0* m),i,rr)) /. k) by A5, A1, PARTFUN1:def 6;

        per cases ;

          suppose

           A10: k = i;

          then (p . k) = (r - (x1 . k)) & (q . k) = (r - (( proj (i,m)) . x)) by A2, A3, A6, A7, A8, A9, FINSEQ_7: 8;

          hence (p . k) = (q . k) by A10, PDIFF_1:def 1;

        end;

          suppose k <> i;

          then (( Replace (x,i,r)) . k) = (x1 /. k) & (q . k) = (( 0* m) /. k) by A3, A6, A7, A9, FINSEQ_7: 10;

          then (( Replace (x,i,r)) . k) = (x1 . k) & (q . k) = ((m |-> 0 ) . k) by A5, A1, PARTFUN1:def 6;

          hence (p . k) = (q . k) by A2, A8;

        end;

      end;

      then ((( reproj (i,x)) . r) - x) = (( reproj (i,( 0* m))) . (r - (( proj (i,m)) . x))) by A1, FINSEQ_1: 13;

      hence ((( reproj (i,x)) . r1) - x) = (( reproj (i,( 0* m))) . (r1 - (( proj (i,m)) . x)));

      for k be Nat st k in ( dom s) holds (s . k) = (t . k)

      proof

        let k be Nat;

        assume

         A11: k in ( dom s);

        then

         A12: 1 <= k & k <= m by A1, FINSEQ_1: 1;

        then k in ( dom ( Replace (x,i,r))) by A4, FINSEQ_3: 25;

        then

         A13: (( Replace (x,i,r)) /. k) = (( Replace (x,i,r)) . k) by PARTFUN1:def 6;



         A14: (s . k) = ((x1 . k) - (y1 . k)) by RVSUM_1: 27;

        t = ( Replace (( 0* m),i,rs)) by PDIFF_1:def 5;

        then

         A15: (t . k) = (( Replace (( 0* m),i,rs)) /. k) by A1, A11, PARTFUN1:def 6;

        per cases ;

          suppose

           A16: k = i;

          then (s . k) = ((x1 . k) - r) & (t . k) = ((( proj (i,m)) . x) - r) by A2, A3, A12, A13, A14, A15, FINSEQ_7: 8;

          hence (s . k) = (t . k) by A16, PDIFF_1:def 1;

        end;

          suppose k <> i;

          then (( Replace (x,i,r)) . k) = (x1 /. k) & (t . k) = (( 0* m) /. k) by A3, A12, A13, A15, FINSEQ_7: 10;

          then (( Replace (x,i,r)) . k) = (x1 . k) & (t . k) = ((m |-> 0 ) . k) by A1, A11, PARTFUN1:def 6;

          hence (s . k) = (t . k) by A2, A14;

        end;

      end;

      hence (x - (( reproj (i,x)) . r1)) = (( reproj (i,( 0* m))) . ((( proj (i,m)) . x) - r1)) by A1, FINSEQ_1: 13;

    end;

    theorem :: PDIFF_7:7



     Th7: for m,i be Nat, x be Point of ( REAL-NS m), p be Point of ( REAL-NS 1) holds ((( reproj (i,x)) . p) - x) = (( reproj (i,( 0. ( REAL-NS m)))) . (p - (( Proj (i,m)) . x))) & (x - (( reproj (i,x)) . p)) = (( reproj (i,( 0. ( REAL-NS m)))) . ((( Proj (i,m)) . x) - p))

    proof

      let m,i be Nat, x be Point of ( REAL-NS m), p be Point of ( REAL-NS 1);

      consider p1 be Element of REAL , y be Element of ( REAL m) such that

       A1: p = <*p1*> & y = x & (( reproj (i,x)) . p) = (( reproj (i,y)) . p1) by PDIFF_1:def 6;

      reconsider pm = p as Element of ( REAL 1) by REAL_NS1:def 4;

      reconsider rm = (( reproj (i,y)) . p1) as Element of ( REAL m);

      ((( reproj (i,x)) . p) - x) = (rm - y) by A1, REAL_NS1: 5;

      then

       A2: ((( reproj (i,x)) . p) - x) = (( reproj (i,( 0* m))) . (p1 - (( proj (i,m)) . y))) by Th6;



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



       A4: <*(( proj (i,m)) . y)*> = (( Proj (i,m)) . x) by A1, PDIFF_1:def 4;

      reconsider Pr = (( Proj (i,m)) . x) as Element of ( REAL 1) by REAL_NS1:def 4;

      consider r1 be Element of REAL , z be Element of ( REAL m) such that

       A5: (p - (( Proj (i,m)) . x)) = <*r1*> & z = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . (p - (( Proj (i,m)) . x))) = (( reproj (i,z)) . r1) by PDIFF_1:def 6;

      (p - (( Proj (i,m)) . x)) = (pm - Pr) by REAL_NS1: 5;

      then (p - (( Proj (i,m)) . x)) = <*(p1 - (( proj (i,m)) . y))*> by A1, A4, RVSUM_1: 29;

      hence ((( reproj (i,x)) . p) - x) = (( reproj (i,( 0. ( REAL-NS m)))) . (p - (( Proj (i,m)) . x))) by A2, A3, A5, FINSEQ_1: 76;

      (x - (( reproj (i,x)) . p)) = (y - rm) by A1, REAL_NS1: 5;

      then

       A6: (x - (( reproj (i,x)) . p)) = (( reproj (i,( 0* m))) . ((( proj (i,m)) . y) - p1)) by Th6;

      consider r2 be Element of REAL , z be Element of ( REAL m) such that

       A7: ((( Proj (i,m)) . x) - p) = <*r2*> & z = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . ((( Proj (i,m)) . x) - p)) = (( reproj (i,z)) . r2) by PDIFF_1:def 6;

      ((( Proj (i,m)) . x) - p) = (Pr - pm) by REAL_NS1: 5;

      then ((( Proj (i,m)) . x) - p) = <*((( proj (i,m)) . y) - p1)*> by A1, A4, RVSUM_1: 29;

      hence (x - (( reproj (i,x)) . p)) = (( reproj (i,( 0. ( REAL-NS m)))) . ((( Proj (i,m)) . x) - p)) by A3, A7, A6, FINSEQ_1: 76;

    end;



     Lm5: for m be Nat, nx be Point of ( REAL-NS m), Z be Subset of ( REAL-NS m), i be Nat st Z is open & nx in Z & 1 <= i & i <= m holds ex N be Neighbourhood of (( Proj (i,m)) . nx) st for z be Point of ( REAL-NS 1) st z in N holds (( reproj (i,nx)) . z) in Z

    proof

      let m be Nat, nx be Point of ( REAL-NS m), Z be Subset of ( REAL-NS m), i be Nat;

      assume that

       A1: Z is open and

       A2: nx in Z and

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

      consider r be Real such that

       A4: 0 < r & { y where y be Point of ( REAL-NS m) : ||.(y - nx).|| < r } c= Z by A1, A2, NDIFF_1: 3;

      set N = { y where y be Point of ( REAL-NS 1) : ||.(y - (( Proj (i,m)) . nx)).|| < r };

      reconsider N as Neighbourhood of (( Proj (i,m)) . nx) by A4, NFCONT_1: 3;

      take N;

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

      assume z in N;

      then

       A5: ex y be Point of ( REAL-NS 1) st y = z & ||.(y - (( Proj (i,m)) . nx)).|| < r;

       ||.((( reproj (i,nx)) . z) - nx).|| = ||.(( reproj (i,( 0. ( REAL-NS m)))) . (z - (( Proj (i,m)) . nx))).|| by Th7

      .= ||.(z - (( Proj (i,m)) . nx)).|| by A3, Th5;

      then (( reproj (i,nx)) . z) in { y where y be Point of ( REAL-NS m) : ||.(y - nx).|| < r } by A5;

      hence thesis by A4;

    end;

    theorem :: PDIFF_7:8



     Th8: for m,n be non zero Nat, i be Nat, f be PartFunc of ( REAL-NS m), ( REAL-NS n), Z be Subset of ( REAL-NS m) st Z is open & 1 <= i & i <= m holds f is_partial_differentiable_on (Z,i) iff Z c= ( dom f) & for x be Point of ( REAL-NS m) st x in Z holds f is_partial_differentiable_in (x,i)

    proof

      let m,n be non zero Nat, i be Nat, f be PartFunc of ( REAL-NS m), ( REAL-NS n), Z be Subset of ( REAL-NS m);

      assume that

       A1: Z is open and

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

      set S = ( REAL-NS 1);

      set T = ( REAL-NS n);

      set RNS = ( R_NormSpace_of_BoundedLinearOperators (S,T));

      thus f is_partial_differentiable_on (Z,i) implies Z c= ( dom f) & for x be Point of ( REAL-NS m) st x in Z holds f is_partial_differentiable_in (x,i)

      proof

        assume

         A3: f is_partial_differentiable_on (Z,i);

        hence

         A4: Z c= ( dom f);

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

        reconsider x0 = (( Proj (i,m)) . nx0) as Point of S;

        assume

         A5: nx0 in Z;

        then (f | Z) is_partial_differentiable_in (nx0,i) by A3;

        then ((f | Z) * ( reproj (i,nx0))) is_differentiable_in x0;

        then

        consider N0 be Neighbourhood of x0 such that

         A6: N0 c= ( dom ((f | Z) * ( reproj (i,nx0)))) and

         A7: ex L be Point of RNS, R be RestFunc of S, T st for x be Point of S st x in N0 holds ((((f | Z) * ( reproj (i,nx0))) /. x) - (((f | Z) * ( reproj (i,nx0))) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by NDIFF_1:def 6;

        consider L be Point of RNS, R be RestFunc of S, T such that

         A8: for x be Point of S st x in N0 holds ((((f | Z) * ( reproj (i,nx0))) /. x) - (((f | Z) * ( reproj (i,nx0))) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A7;

        consider N1 be Neighbourhood of x0 such that

         A9: for x be Point of S st x in N1 holds (( reproj (i,nx0)) . x) in Z by A1, A2, A5, Lm5;

         A10:

        now

          let x be Point of S;

          assume x in N1;

          then (( reproj (i,nx0)) . x) in Z by A9;

          then (( reproj (i,nx0)) . x) in (( dom f) /\ Z) by A4, XBOOLE_0:def 4;

          hence (( reproj (i,nx0)) . x) in ( dom (f | Z)) by RELAT_1: 61;

        end;

        reconsider N = (N0 /\ N1) as Neighbourhood of x0 by Lm1;

        ((f | Z) * ( reproj (i,nx0))) c= (f * ( reproj (i,nx0))) by RELAT_1: 29, RELAT_1: 59;

        then

         A11: ( dom ((f | Z) * ( reproj (i,nx0)))) c= ( dom (f * ( reproj (i,nx0)))) by RELAT_1: 11;

        N c= N0 by XBOOLE_1: 17;

        then N c= ( dom ((f | Z) * ( reproj (i,nx0)))) by A6;

        then

         A12: N c= ( dom (f * ( reproj (i,nx0)))) by A11;

        now

          let x be Point of S;

          assume

           A13: x in N;

          then

           A14: x in N0 by XBOOLE_0:def 4;



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

          x in N1 by A13, XBOOLE_0:def 4;

          then

           A16: (( reproj (i,nx0)) . x) in ( dom (f | Z)) by A10;

          then

           A17: (( reproj (i,nx0)) . x) in ( dom f) & (( reproj (i,nx0)) . x) in Z by RELAT_1: 57;



           A18: (( reproj (i,nx0)) . x0) in ( dom (f | Z)) by A10, NFCONT_1: 4;

          then

           A19: (( reproj (i,nx0)) . x0) in ( dom f) & (( reproj (i,nx0)) . x0) in Z by RELAT_1: 57;



           A20: (((f | Z) * ( reproj (i,nx0))) /. x) = ((f | Z) /. (( reproj (i,nx0)) /. x)) by A16, A15, PARTFUN2: 4

          .= (f /. (( reproj (i,nx0)) /. x)) by A17, PARTFUN2: 17

          .= ((f * ( reproj (i,nx0))) /. x) by A15, A17, PARTFUN2: 4;

          (((f | Z) * ( reproj (i,nx0))) /. x0) = ((f | Z) /. (( reproj (i,nx0)) /. x0)) by A15, A18, PARTFUN2: 4

          .= (f /. (( reproj (i,nx0)) /. x0)) by A19, PARTFUN2: 17

          .= ((f * ( reproj (i,nx0))) /. x0) by A15, A19, PARTFUN2: 4;

          hence (((f * ( reproj (i,nx0))) /. x) - ((f * ( reproj (i,nx0))) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A8, A14, A20;

        end;

        then (f * ( reproj (i,nx0))) is_differentiable_in x0 by A12, NDIFF_1:def 6;

        hence f is_partial_differentiable_in (nx0,i);

      end;

      assume that

       A21: Z c= ( dom f) and

       A22: for nx be Point of ( REAL-NS m) st nx in Z holds f is_partial_differentiable_in (nx,i);

      thus Z c= ( dom f) by A21;

      now

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

        assume

         A23: nx0 in Z;

        then

         A24: f is_partial_differentiable_in (nx0,i) by A22;

        reconsider x0 = (( Proj (i,m)) . nx0) as Point of S;

        (f * ( reproj (i,nx0))) is_differentiable_in x0 by A24;

        then

        consider N0 be Neighbourhood of x0 such that N0 c= ( dom (f * ( reproj (i,nx0)))) and

         A25: ex L be Point of RNS, R be RestFunc of S, T st for x be Point of S st x in N0 holds (((f * ( reproj (i,nx0))) /. x) - ((f * ( reproj (i,nx0))) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by NDIFF_1:def 6;

        consider N1 be Neighbourhood of x0 such that

         A26: for x be Point of S st x in N1 holds (( reproj (i,nx0)) . x) in Z by A1, A2, A23, Lm5;

         A27:

        now

          let x be Point of S;

          assume x in N1;

          then (( reproj (i,nx0)) . x) in Z by A26;

          then (( reproj (i,nx0)) . x) in (( dom f) /\ Z) by A21, XBOOLE_0:def 4;

          hence (( reproj (i,nx0)) . x) in ( dom (f | Z)) by RELAT_1: 61;

        end;



         A28: N1 c= ( dom ((f | Z) * ( reproj (i,nx0))))

        proof

          let z be object;

          assume

           A29: z in N1;

          then

           A30: z in the carrier of S;

          reconsider x = z as Point of S by A29;



           A31: (( reproj (i,nx0)) . x) in ( dom (f | Z)) by A29, A27;

          z in ( dom ( reproj (i,nx0))) by A30, FUNCT_2:def 1;

          hence z in ( dom ((f | Z) * ( reproj (i,nx0)))) by A31, FUNCT_1: 11;

        end;

        reconsider N = (N0 /\ N1) as Neighbourhood of x0 by Lm1;

        N c= N1 by XBOOLE_1: 17;

        then

         A32: N c= ( dom ((f | Z) * ( reproj (i,nx0)))) by A28;

        consider L be Point of RNS, R be RestFunc of S, T such that

         A33: for x be Point of S st x in N0 holds (((f * ( reproj (i,nx0))) /. x) - ((f * ( reproj (i,nx0))) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A25;

        now

          let x be Point of S;

          assume

           A34: x in N;

          then

           A35: x in N0 by XBOOLE_0:def 4;



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

          x in N1 by A34, XBOOLE_0:def 4;

          then

           A37: (( reproj (i,nx0)) . x) in ( dom (f | Z)) by A27;

          then

           A38: (( reproj (i,nx0)) . x) in (( dom f) /\ Z) by RELAT_1: 61;

          then

           A39: (( reproj (i,nx0)) . x) in ( dom f) by XBOOLE_0:def 4;



           A40: (( reproj (i,nx0)) . x0) in ( dom (f | Z)) by A27, NFCONT_1: 4;

          then

           A41: (( reproj (i,nx0)) . x0) in (( dom f) /\ Z) by RELAT_1: 61;

          then

           A42: (( reproj (i,nx0)) . x0) in ( dom f) by XBOOLE_0:def 4;



           A43: (((f | Z) * ( reproj (i,nx0))) /. x) = ((f | Z) /. (( reproj (i,nx0)) /. x)) by A37, A36, PARTFUN2: 4

          .= (f /. (( reproj (i,nx0)) /. x)) by A38, PARTFUN2: 16

          .= ((f * ( reproj (i,nx0))) /. x) by A36, A39, PARTFUN2: 4;

          (((f | Z) * ( reproj (i,nx0))) /. x0) = ((f | Z) /. (( reproj (i,nx0)) /. x0)) by A36, A40, PARTFUN2: 4

          .= (f /. (( reproj (i,nx0)) /. x0)) by A41, PARTFUN2: 16

          .= ((f * ( reproj (i,nx0))) /. x0) by A36, A42, PARTFUN2: 4;

          hence ((((f | Z) * ( reproj (i,nx0))) /. x) - (((f | Z) * ( reproj (i,nx0))) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A43, A35, A33;

        end;

        then ((f | Z) * ( reproj (i,nx0))) is_differentiable_in x0 by A32, NDIFF_1:def 6;

        hence (f | Z) is_partial_differentiable_in (nx0,i);

      end;

      hence thesis;

    end;



     Lm6: for v be Element of ( REAL m), x be Real, i be Nat holds ( len ( Replace (v,i,x))) = m

    proof

      let v be Element of ( REAL m);

      let x be Real;

      let i be Nat;

      ( len ( Replace (v,i,x))) = ( len v) by FUNCT_7: 97;

      hence ( len ( Replace (v,i,x))) = m by CARD_1:def 7;

    end;



     Lm7: for x be Real, i,j be Nat st 1 <= j & j <= m holds (i = j implies (( Replace (( 0* m),i,x)) . j) = x) & (i <> j implies (( Replace (( 0* m),i,x)) . j) = 0 )

    proof

      let x be Real;

      let i,j be Nat;

      assume 1 <= j & j <= m;

      then

       A1: j in ( Seg m);

      ( len ( 0* m)) = m by CARD_1:def 7;

      then

       A2: j in ( dom ( 0* m)) by A1, FINSEQ_1:def 3;

      now

        assume i <> j;

        then ((( 0* m) +* (i,x)) . j) = (( 0* m) . j) by FUNCT_7: 32;

        hence (( Replace (( 0* m),i,x)) . j) = 0 ;

      end;

      hence thesis by A2, FUNCT_7: 31;

    end;

    theorem :: PDIFF_7:9



     Th9: for x,y be Element of REAL , i be Nat st 1 <= i & i <= m holds ( Replace (( 0* m),i,(x + y))) = (( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y)))

    proof

      let x,y be Element of REAL ;

      let i be Nat;

      assume

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

      reconsider xy = (x + y) as Element of REAL ;



       A2: ( len ( Replace (( 0* m),i,xy))) = m & ( len ( Replace (( 0* m),i,x))) = m & ( len ( Replace (( 0* m),i,y))) = m by Lm6;

      then

       A3: ( len (( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y)))) = ( len ( Replace (( 0* m),i,xy))) by RVSUM_1: 115;

      for j be Nat st 1 <= j & j <= ( len ( Replace (( 0* m),i,xy))) holds (( Replace (( 0* m),i,xy)) . j) = ((( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y))) . j)

      proof

        let j be Nat;

        assume

         A4: 1 <= j & j <= ( len ( Replace (( 0* m),i,xy)));

        reconsider j as Nat;



         A5: ( dom (( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y)))) = (( dom ( Replace (( 0* m),i,x))) /\ ( dom ( Replace (( 0* m),i,y)))) by VALUED_1:def 1;

        j in ( dom ( Replace (( 0* m),i,x))) & j in ( dom ( Replace (( 0* m),i,y))) by A4, A2, FINSEQ_3: 25;

        then j in ( dom (( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y)))) by A5, XBOOLE_0:def 4;

        then

         A6: ((( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y))) . j) = ((( Replace (( 0* m),i,x)) . j) + (( Replace (( 0* m),i,y)) . j)) by VALUED_1:def 1;

        per cases ;

          suppose

           A7: i = j;



          then ((( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y))) . j) = (x + (( Replace (( 0* m),i,y)) . j)) by A1, A6, Lm7

          .= (x + y) by A1, A7, Lm7;

          hence thesis by A1, A7, Lm7;

        end;

          suppose

           A8: i <> j;



          then ((( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,y))) . j) = ( 0 qua Real + (( Replace (( 0* m),i,y)) . j)) by A4, A6, A2, Lm7

          .= 0 by A4, A2, A8, Lm7;

          hence thesis by A4, A2, A8, Lm7;

        end;

      end;

      hence thesis by A3;

    end;

    registration

      let f be real-valued FinSequence;

      let i be Nat;

      let p be Real;

      cluster ( Replace (f,i,p)) -> real-valued;

      coherence

      proof

        ( rng ( Replace (f,i,p))) c= (( rng f) \/ {p}) by FUNCT_7: 100;

        then ( rng ( Replace (f,i,p))) c= REAL by XBOOLE_1: 1;

        hence thesis by VALUED_0:def 3;

      end;

    end

    theorem :: PDIFF_7:10



     Th10: for x,a be Real, i be Nat st 1 <= i & i <= m holds (( 0* m) +* (i,(a * x))) = (a * ( Replace (( 0* m),i,x)))

    proof

      let x,a be Real;

      let i be Nat;

      assume

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

      reconsider ax = (a * x) as Real;



       A2: ( len ( Replace (( 0* m),i,ax))) = m & ( len ( Replace (( 0* m),i,x))) = m by Lm6;

      then

       A3: ( len (a * ( Replace (( 0* m),i,x)))) = ( len ( Replace (( 0* m),i,ax))) by RVSUM_1: 117;

      for j be Nat st 1 <= j & j <= ( len ( Replace (( 0* m),i,ax))) holds (( Replace (( 0* m),i,ax)) . j) = ((a * ( Replace (( 0* m),i,x))) . j)

      proof

        let j be Nat;

        assume

         A4: 1 <= j & j <= ( len ( Replace (( 0* m),i,ax)));

        reconsider j as Nat;

        per cases ;

          suppose

           A5: i = j;



          then (( Replace (( 0* m),i,ax)) . j) = (a * x) by A1, Lm7

          .= (a * (( Replace (( 0* m),i,x)) . j)) by A1, A5, Lm7;

          hence thesis by RVSUM_1: 44;

        end;

          suppose

           A6: i <> j;

          then (( Replace (( 0* m),i,x)) . j) = 0 by A2, A4, Lm7;

          then (( Replace (( 0* m),i,ax)) . j) = (a * (( Replace (( 0* m),i,x)) . j)) by A2, A4, A6, Lm7;

          hence thesis by RVSUM_1: 44;

        end;

      end;

      hence thesis by A3;

    end;

    theorem :: PDIFF_7:11



     Th11: for x be Element of REAL , i be Nat st 1 <= i & i <= m & x <> 0 holds ( Replace (( 0* m),i,x)) <> ( 0* m)

    proof

      let x be Element of REAL ;

      let i be Nat;

      assume

       A1: 1 <= i & i <= m & x <> 0 ;

      then

       A2: i in ( Seg m);

      assume

       A3: ( Replace (( 0* m),i,x)) = ( 0* m);

      ( len ( 0* m)) = m by CARD_1:def 7;

      then ( Seg m) = ( proj1 ( 0* m)) by FINSEQ_1:def 3;

      then x = (( 0* m) . i) by A3, A2, FUNCT_7: 31;

      hence contradiction by A1;

    end;

    theorem :: PDIFF_7:12



     Th12: for x,y be Element of REAL , z be Element of ( REAL m), i be Nat st 1 <= i & i <= m & y = (( proj (i,m)) . z) holds (( Replace (z,i,x)) - z) = (( 0* m) +* (i,(x - y))) & (z - ( Replace (z,i,x))) = (( 0* m) +* (i,(y - x)))

    proof

      let x,y be Element of REAL ;

      let z be Element of ( REAL m);

      let i be Nat;

      assume that

       A1: 1 <= i & i <= m and

       A2: y = (( proj (i,m)) . z);

      reconsider xy = (x - y), my = ( - y) as Element of REAL ;



       A3: ( len ( Replace (( 0* m),i,xy))) = m & ( len ( Replace (( 0* m),i,x))) = m & ( len ( Replace (( 0* m),i,my))) = m by Lm6;



       A4: ( dom ( Replace (z,i,x))) = ( dom z) by FUNCT_7: 30;



       A5: ( dom ( - z)) = ( dom z) & ( dom ( - ( Replace (z,i,x)))) = ( dom ( Replace (z,i,x))) by VALUED_1:def 5;



       A6: ( dom (( Replace (z,i,x)) - z)) = (( dom ( Replace (z,i,x))) /\ ( dom ( - z))) by VALUED_1:def 1;



       A7: ( len ( 0* m)) = m by CARD_1:def 7;

      ( dom (( Replace (z,i,x)) - z)) = ( Seg m) by A4, A5, A6, FINSEQ_1: 89;

      then ( len (( Replace (z,i,x)) - z)) = ( len ( 0* m)) by A7, FINSEQ_1:def 3;

      then

       A8: ( len (( Replace (z,i,x)) - z)) = ( len ( Replace (( 0* m),i,xy))) by FINSEQ_7: 5;

      for j be Nat st 1 <= j & j <= ( len (( Replace (z,i,x)) - z)) holds (( Replace (( 0* m),i,xy)) . j) = ((( Replace (z,i,x)) - z) . j)

      proof

        let j be Nat;

        assume

         A9: 1 <= j & j <= ( len (( Replace (z,i,x)) - z));

        reconsider j as Nat;



         A10: j in ( dom (( Replace (z,i,x)) - z)) by A9, FINSEQ_3: 25;

        (( - z) . j) = (( - 1) * (z . j)) by RVSUM_1: 44;

        then ((( Replace (z,i,x)) - z) . j) = ((( Replace (z,i,x)) . j) + ( - (z . j))) by A10, VALUED_1:def 1;

        then

         A11: ((( Replace (z,i,x)) - z) . j) = ((( Replace (z,i,x)) . j) - (z . j));



         A12: 1 <= i & i <= ( len z) implies (( Replace (z,i,x)) . i) = x

        proof

          assume 1 <= i & i <= ( len z);

          then i in ( dom z) by FINSEQ_3: 25;

          hence thesis by FUNCT_7: 31;

        end;



         A13: ( dom (( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,my)))) = (( dom ( Replace (( 0* m),i,x))) /\ ( dom ( Replace (( 0* m),i,my)))) by VALUED_1:def 1;

        j in ( dom ( Replace (( 0* m),i,x))) & j in ( dom ( Replace (( 0* m),i,my))) by A3, A9, A8, FINSEQ_3: 25;

        then j in ( dom (( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,my)))) by A13, XBOOLE_0:def 4;

        then

         A14: ((( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,my))) . j) = ((( Replace (( 0* m),i,x)) . j) + (( Replace (( 0* m),i,my)) . j)) by VALUED_1:def 1;

        per cases ;

          suppose

           A15: i = j;

          reconsider xmy = (x + my) as Real;

          (( Replace (( 0* m),i,xy)) . j) = (( Replace (( 0* m),i,xmy)) . j)

          .= ((( Replace (( 0* m),i,x)) + ( Replace (( 0* m),i,my))) . j) by A1, Th9

          .= (x + (( Replace (( 0* m),i,my)) . j)) by A1, A14, A15, Lm7

          .= (x + ( - y)) by A1, A15, Lm7

          .= (x - (( proj (i,m)) . z)) by A2;

          hence thesis by A11, A9, A4, A5, A6, A12, A15, FINSEQ_3: 29, PDIFF_1:def 1;

        end;

          suppose

           A16: not (i = j);

          then (( Replace (( 0* m),i,xy)) . j) = ((z . j) - (z . j)) by A3, A9, A8, Lm7;

          hence thesis by A11, A16, FUNCT_7: 32;

        end;

      end;

      hence

       A17: (( Replace (z,i,x)) - z) = (( 0* m) +* (i,(x - y))) by A8;

      reconsider a = ( - 1) as Element of REAL by XREAL_0:def 1;

      reconsider axy = (a * xy) as Element of REAL ;

      (z - ( Replace (z,i,x))) = ( - ( Replace (( 0* m),i,xy))) by A17, RVSUM_1: 35;

      then (z - ( Replace (z,i,x))) = ( Replace (( 0* m),i,axy)) by A1, Th10;

      hence (z - ( Replace (z,i,x))) = (( 0* m) +* (i,(y - x)));

    end;

    theorem :: PDIFF_7:13



     Th13: for x,y be Element of REAL , i be Nat st 1 <= i & i <= m holds (( reproj (i,( 0* m))) . (x + y)) = ((( reproj (i,( 0* m))) . x) + (( reproj (i,( 0* m))) . y))

    proof

      let x,y be Element of REAL , i be Nat;

      assume

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

      reconsider xy = (x + y) as Element of REAL ;

      ( Replace (( 0* m),i,x)) = (( reproj (i,( 0* m))) . x) & ( Replace (( 0* m),i,y)) = (( reproj (i,( 0* m))) . y) & (( reproj (i,( 0* m))) . (x + y)) = ( Replace (( 0* m),i,xy)) by PDIFF_1:def 5;

      hence thesis by A1, Th9;

    end;

    theorem :: PDIFF_7:14



     Th14: for x,y be Point of ( REAL-NS 1), i be Nat st 1 <= i & i <= m holds (( reproj (i,( 0. ( REAL-NS m)))) . (x + y)) = ((( reproj (i,( 0. ( REAL-NS m)))) . x) + (( reproj (i,( 0. ( REAL-NS m)))) . y))

    proof

      let x,y be Point of ( REAL-NS 1), i be Nat;

      assume

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

      consider q1 be Element of REAL , z1 be Element of ( REAL m) such that

       A2: x = <*q1*> & z1 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . x) = (( reproj (i,z1)) . q1) by PDIFF_1:def 6;

      consider q2 be Element of REAL , z2 be Element of ( REAL m) such that

       A3: y = <*q2*> & z2 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . y) = (( reproj (i,z2)) . q2) by PDIFF_1:def 6;

      consider q12 be Element of REAL , z12 be Element of ( REAL m) such that

       A4: (x + y) = <*q12*> & z12 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . (x + y)) = (( reproj (i,z12)) . q12) by PDIFF_1:def 6;



       A5: ( 0. ( REAL-NS m)) = ( 0* m) by REAL_NS1:def 4;

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

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

      (x + y) = (qq1 + qq2) by A2, A3, REAL_NS1: 2;

      then

       A6: (x + y) = <*(q1 + q2)*> by RVSUM_1: 13;

      ((( reproj (i,( 0. ( REAL-NS m)))) . x) + (( reproj (i,( 0. ( REAL-NS m)))) . y)) = ((( reproj (i,( 0* m))) . q1) + (( reproj (i,( 0* m))) . q2)) by A2, A3, A5, REAL_NS1: 2

      .= (( reproj (i,( 0* m))) . (q1 + q2)) by A1, Th13;

      hence thesis by A6, A4, A5, FINSEQ_1: 76;

    end;

    theorem :: PDIFF_7:15



     Th15: for x,a be Real, i be Nat st 1 <= i <= m holds (( reproj (i,( 0* m))) . (a * x)) = (a (#) (( reproj (i,( 0* m))) . x))

    proof

      let x,a be Real, i be Nat;

      assume

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

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

      reconsider ax = (a * x) as Element of REAL ;



       A2: ( Replace (( 0* m),i,ax)) = (a * ( Replace (( 0* m),i,x))) by Th10, A1;

      ( Replace (( 0* m),i,x)) = (( reproj (i,( 0* m))) . x) by PDIFF_1:def 5;

      then (( reproj (i,( 0* m))) . (a * x)) = (a * (( reproj (i,( 0* m))) . x)) by A2, PDIFF_1:def 5;

      hence thesis;

    end;

    theorem :: PDIFF_7:16



     Th16: for x be Point of ( REAL-NS 1), a be Real, i be Nat st 1 <= i & i <= m holds (( reproj (i,( 0. ( REAL-NS m)))) . (a * x)) = (a * (( reproj (i,( 0. ( REAL-NS m)))) . x))

    proof

      let x be Point of ( REAL-NS 1), a be Real, i be Nat;

      assume

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

      consider q1 be Element of REAL , z1 be Element of ( REAL m) such that

       A2: x = <*q1*> & z1 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . x) = (( reproj (i,z1)) . q1) by PDIFF_1:def 6;

      consider q12 be Element of REAL , z12 be Element of ( REAL m) such that

       A3: (a * x) = <*q12*> & z12 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . (a * x)) = (( reproj (i,z12)) . q12) by PDIFF_1:def 6;



       A4: ( 0. ( REAL-NS m)) = ( 0* m) by REAL_NS1:def 4;

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

      (a * x) = (a * qq1) by A2, REAL_NS1: 3;

      then

       A5: (a * x) = <*(a * q1)*> by RVSUM_1: 47;

      (a * (( reproj (i,( 0. ( REAL-NS m)))) . x)) = (a * (( reproj (i,( 0* m))) . q1)) by A2, A4, REAL_NS1: 3

      .= (( reproj (i,( 0* m))) . (a * q1)) by A1, Th15;

      hence thesis by A5, A3, A4, FINSEQ_1: 76;

    end;

    theorem :: PDIFF_7:17



     Th17: for x be Element of REAL , i be Nat st 1 <= i & i <= m & x <> 0 holds (( reproj (i,( 0* m))) . x) <> ( 0* m)

    proof

      let x be Element of REAL , i be Nat;

      assume 1 <= i & i <= m & x <> 0 ;

      then ( Replace (( 0* m),i,x)) <> ( 0* m) by Th11;

      hence thesis by PDIFF_1:def 5;

    end;

    theorem :: PDIFF_7:18



     Th18: for x be Point of ( REAL-NS 1), i be Nat st 1 <= i & i <= m & x <> ( 0. ( REAL-NS 1)) holds (( reproj (i,( 0. ( REAL-NS m)))) . x) <> ( 0. ( REAL-NS m))

    proof

      let x be Point of ( REAL-NS 1), i be Nat;

      assume

       A1: 1 <= i & i <= m & x <> ( 0. ( REAL-NS 1));

      consider q1 be Element of REAL , z1 be Element of ( REAL m) such that

       A2: x = <*q1*> & z1 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . x) = (( reproj (i,z1)) . q1) by PDIFF_1:def 6;



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

      now

        assume q1 = 0 ;

        then <*q1*> = ( 0* 1) by FINSEQ_2: 59;

        hence contradiction by A2, A1, REAL_NS1:def 4;

      end;

      hence thesis by A2, A3, A1, Th17;

    end;

    theorem :: PDIFF_7:19



     Th19: for x,y be Element of REAL , z be Element of ( REAL m), i be Nat st 1 <= i & i <= m & y = (( proj (i,m)) . z) holds ((( reproj (i,z)) . x) - z) = (( reproj (i,( 0* m))) . (x - y)) & (z - (( reproj (i,z)) . x)) = (( reproj (i,( 0* m))) . (y - x))

    proof

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

      reconsider xy = (x - y), yx = (y - x) as Element of REAL ;

      assume 1 <= i & i <= m & y = (( proj (i,m)) . z);

      then

       A1: (( Replace (z,i,x)) - z) = ( Replace (( 0* m),i,xy)) & (z - ( Replace (z,i,x))) = ( Replace (( 0* m),i,yx)) by Th12;

      ( Replace (z,i,x)) = (( reproj (i,z)) . x) by PDIFF_1:def 5;

      hence thesis by A1, PDIFF_1:def 5;

    end;

    theorem :: PDIFF_7:20



     Th20: for x,y be Point of ( REAL-NS 1), i be Nat, z be Point of ( REAL-NS m) st 1 <= i & i <= m & y = (( Proj (i,m)) . z) holds ((( reproj (i,z)) . x) - z) = (( reproj (i,( 0. ( REAL-NS m)))) . (x - y)) & (z - (( reproj (i,z)) . x)) = (( reproj (i,( 0. ( REAL-NS m)))) . (y - x))

    proof

      let x,y be Point of ( REAL-NS 1), i be Nat, z be Point of ( REAL-NS m);

      assume

       A1: 1 <= i & i <= m & y = (( Proj (i,m)) . z);

      consider q1 be Element of REAL , z1 be Element of ( REAL m) such that

       A2: x = <*q1*> & z1 = z & (( reproj (i,z)) . x) = (( reproj (i,z1)) . q1) by PDIFF_1:def 6;

      consider q2 be Element of REAL , z2 be Element of ( REAL m) such that

       A3: y = <*q2*> & z2 = z & (( reproj (i,z)) . y) = (( reproj (i,z2)) . q2) by PDIFF_1:def 6;

      consider q12 be Element of REAL , z12 be Element of ( REAL m) such that

       A4: (x - y) = <*q12*> & z12 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . (x - y)) = (( reproj (i,z12)) . q12) by PDIFF_1:def 6;

      consider q21 be Element of REAL , z21 be Element of ( REAL m) such that

       A5: (y - x) = <*q21*> & z21 = ( 0. ( REAL-NS m)) & (( reproj (i,( 0. ( REAL-NS m)))) . (y - x)) = (( reproj (i,z21)) . q21) by PDIFF_1:def 6;



       A6: ( 0. ( REAL-NS m)) = ( 0* m) by REAL_NS1:def 4;

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

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

      (x - y) = (qq1 - qq2) & (y - x) = (qq2 - qq1) by A2, A3, REAL_NS1: 5;

      then (x - y) = <*(q1 - q2)*> & (y - x) = <*(q2 - q1)*> by RVSUM_1: 29;

      then

       A7: (( reproj (i,( 0. ( REAL-NS m)))) . (x - y)) = (( reproj (i,( 0* m))) . (q1 - q2)) & (( reproj (i,( 0. ( REAL-NS m)))) . (y - x)) = (( reproj (i,( 0* m))) . (q2 - q1)) by A4, A5, A6, FINSEQ_1: 76;

      y = <*(( proj (i,m)) . z)*> by A1, PDIFF_1:def 4;

      then q2 = (( proj (i,m)) . z1) by A2, A3, FINSEQ_1: 76;

      then ((( reproj (i,z1)) . q1) - z1) = (( reproj (i,( 0* m))) . (q1 - q2)) & (z1 - (( reproj (i,z1)) . q1)) = (( reproj (i,( 0* m))) . (q2 - q1)) by Th19, A1;

      hence thesis by A7, A2, REAL_NS1: 5;

    end;

    theorem :: PDIFF_7:21



     Th21: f is_differentiable_in x & 1 <= i & i <= m implies f is_partial_differentiable_in (x,i) & ( partdiff (f,x,i)) = (( diff (f,x)) * ( reproj (i,( 0. ( REAL-NS m)))))

    proof

      assume

       A1: f is_differentiable_in x;

      assume

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

      consider N be Neighbourhood of x such that

       A3: N c= ( dom f) & ex R be RestFunc of ( REAL-NS m), ( REAL-NS n) st for y be Point of ( REAL-NS m) st y in N holds ((f /. y) - (f /. x)) = ((( diff (f,x)) . (y - x)) + (R /. (y - x))) by A1, NDIFF_1:def 7;

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

       A4: for y be Point of ( REAL-NS m) st y in N holds ((f /. y) - (f /. x)) = ((( diff (f,x)) . (y - x)) + (R /. (y - x))) by A3;

      consider r0 be Real such that

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

      set u = (f * ( reproj (i,x)));

      reconsider x0 = (( Proj (i,m)) . x) as Point of ( REAL-NS 1);

      set Z = ( 0. ( REAL-NS m));

      set Nx0 = { z where z be Point of ( REAL-NS 1) : ||.(z - x0).|| < r0 };

      now

        let s be object;

        assume s in Nx0;

        then ex z be Point of ( REAL-NS 1) st s = z & ||.(z - x0).|| < r0;

        hence s in the carrier of ( REAL-NS 1);

      end;

      then Nx0 is Subset of ( REAL-NS 1) by TARSKI:def 3;

      then

      reconsider Nx0 as Neighbourhood of x0 by A5, NFCONT_1:def 1;



       A6: for xi be Element of ( REAL-NS 1) st xi in Nx0 holds (( reproj (i,x)) . xi) in N

      proof

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

        assume xi in Nx0;

        then

         A7: ex z be Point of ( REAL-NS 1) st xi = z & ||.(z - x0).|| < r0;

        ((( reproj (i,x)) . xi) - x) = (( reproj (i,Z)) . (xi - x0)) by A2, Th20;

        then ||.((( reproj (i,x)) . xi) - x).|| < r0 by A2, Th5, A7;

        then (( reproj (i,x)) . xi) in { z where z be Point of ( REAL-NS m) : ||.(z - x).|| < r0 };

        hence thesis by A5;

      end;



       A8: R is total by NDIFF_1:def 5;

      then

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

      reconsider R1 = (R * ( reproj (i,( 0. ( REAL-NS m))))) as PartFunc of ( REAL-NS 1), ( REAL-NS n);



       A10: ( dom ( reproj (i,( 0. ( REAL-NS m))))) = the carrier of ( REAL-NS 1) by FUNCT_2:def 1;



       A11: ( dom R1) = the carrier of ( REAL-NS 1) by A8, PARTFUN1:def 2;

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

      proof

        let r be Real;

        assume r > 0 ;

        then

        consider d be Real such that

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

        take d;

        now

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

          assume

           A13: z <> ( 0. ( REAL-NS 1)) & ||.z.|| < d;



           A14: ||.(( reproj (i,Z)) . z).|| = ||.z.|| by A2, Th5;

          (R /. (( reproj (i,Z)) . z)) = (R . (( reproj (i,Z)) . z)) by A9, PARTFUN1:def 6;

          then (R /. (( reproj (i,Z)) . z)) = (R1 . z) by A10, FUNCT_1: 13;

          then (R /. (( reproj (i,Z)) . z)) = (R1 /. z) by A11, PARTFUN1:def 6;

          hence (( ||.z.|| " ) * ||.(R1 /. z).||) < r by A12, A14, A13, Th18, A2;

        end;

        hence thesis by A12;

      end;

      then

      reconsider R1 as RestFunc of ( REAL-NS 1), ( REAL-NS n) by A8, NDIFF_1: 23;

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

      reconsider LD1 = (dfx * ( reproj (i,( 0. ( REAL-NS m))))) as Function of ( REAL-NS 1), ( REAL-NS n);

       A15:

      now

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

        (LD1 . (x + y)) = (dfx . (( reproj (i,Z)) . (x + y))) by FUNCT_2: 15;

        then (LD1 . (x + y)) = (dfx . ((( reproj (i,Z)) . x) + (( reproj (i,Z)) . y))) by Th14, A2;

        then (LD1 . (x + y)) = ((dfx . (( reproj (i,Z)) . x)) + (dfx . (( reproj (i,Z)) . y))) by VECTSP_1:def 20;

        then (LD1 . (x + y)) = ((LD1 . x) + (dfx . (( reproj (i,Z)) . y))) by FUNCT_2: 15;

        hence (LD1 . (x + y)) = ((LD1 . x) + (LD1 . y)) by FUNCT_2: 15;

      end;

      now

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

        (LD1 . (a * x)) = (dfx . (( reproj (i,Z)) . (a * x))) by FUNCT_2: 15;

        then (LD1 . (a * x)) = (dfx . (a * (( reproj (i,Z)) . x))) by Th16, A2;

        then (LD1 . (a * x)) = (a * (dfx . (( reproj (i,Z)) . x))) by LOPBAN_1:def 5;

        hence (LD1 . (a * x)) = (a * (LD1 . x)) by FUNCT_2: 15;

      end;

      then

      reconsider LD1 as LinearOperator of ( REAL-NS 1), ( REAL-NS n) by A15, LOPBAN_1:def 5, VECTSP_1:def 20;

      reconsider LD1 as Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),( REAL-NS n))) by LOPBAN_1:def 9;

      now

        let s be object;

        assume s in (( reproj (i,x)) .: Nx0);

        then ex t be Element of ( REAL-NS 1) st t in Nx0 & s = (( reproj (i,x)) . t) by FUNCT_2: 65;

        then s in N by A6;

        hence s in ( dom f) by A3;

      end;

      then

       A16: (( reproj (i,x)) .: Nx0) c= ( dom f);

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

      then

       A17: Nx0 c= ( dom u) by A16, FUNCT_3: 3;



       A18: for y be Point of ( REAL-NS 1) st y in Nx0 holds ((u /. y) - (u /. x0)) = ((LD1 . (y - x0)) + (R1 /. (y - x0)))

      proof

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

        assume

         A19: y in Nx0;

        then

         A20: (( reproj (i,x)) . y) in N by A6;

        consider q be Element of REAL , z be Element of ( REAL m) such that

         A21: x0 = <*q*> & z = x & (( reproj (i,x)) . x0) = (( reproj (i,z)) . q) by PDIFF_1:def 6;

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

        x0 = <*(( proj (i,m)) . x)*> by PDIFF_1:def 4;

        then q = (( proj (i,m)) . z) by A21, FINSEQ_1: 76;

        then (( reproj (i,x)) . x0) = (( reproj (i,z)) . (z . i)) by A21, PDIFF_1:def 1;

        then (( reproj (i,x)) . x0) = ( Replace (z,i,zi)) by PDIFF_1:def 5;

        then

         A22: (( reproj (i,x)) . x0) = x by A21, FUNCT_7: 35;



         A23: x0 in Nx0 by NFCONT_1: 4;



         A24: (( reproj (i,x)) . x0) in N by A6, NFCONT_1: 4;

        (u /. y) = (u . y) by A19, A17, PARTFUN1:def 6;

        then (u /. y) = (f . (( reproj (i,x)) . y)) by FUNCT_2: 15;

        then

         A25: (u /. y) = (f /. (( reproj (i,x)) . y)) by A20, A3, PARTFUN1:def 6;

        (u /. x0) = (u . x0) by A23, A17, PARTFUN1:def 6;

        then (u /. x0) = (f . (( reproj (i,x)) . x0)) by FUNCT_2: 15;

        then

         A26: ((u /. y) - (u /. x0)) = ((f /. (( reproj (i,x)) . y)) - (f /. x)) by A25, A22, A24, A3, PARTFUN1:def 6;

        (R /. (( reproj (i,Z)) . (y - x0))) = (R . (( reproj (i,Z)) . (y - x0))) by A9, PARTFUN1:def 6;

        then (R /. (( reproj (i,Z)) . (y - x0))) = (R1 . (y - x0)) by A10, FUNCT_1: 13;

        then

         A27: (R /. (( reproj (i,Z)) . (y - x0))) = (R1 /. (y - x0)) by A11, PARTFUN1:def 6;

        ((u /. y) - (u /. x0)) = ((( diff (f,x)) . ((( reproj (i,x)) . y) - x)) + (R /. ((( reproj (i,x)) . y) - x))) by A26, A4, A19, A6;

        then ((u /. y) - (u /. x0)) = ((dfx . (( reproj (i,Z)) . (y - x0))) + (R /. ((( reproj (i,x)) . y) - x))) by A2, Th20;

        then ((u /. y) - (u /. x0)) = ((dfx . (( reproj (i,Z)) . (y - x0))) + (R /. (( reproj (i,Z)) . (y - x0)))) by A2, Th20;

        hence ((u /. y) - (u /. x0)) = ((LD1 . (y - x0)) + (R1 /. (y - x0))) by A27, FUNCT_2: 15;

      end;

      then

       A28: u is_differentiable_in x0 by A17, NDIFF_1:def 6;

      hence f is_partial_differentiable_in (x,i);

      thus ( partdiff (f,x,i)) = (( diff (f,x)) * ( reproj (i,( 0. ( REAL-NS m))))) by A28, A17, A18, NDIFF_1:def 7;

    end;

    theorem :: PDIFF_7:22



     Th22: g is_differentiable_in y & 1 <= i & i <= m implies g is_partial_differentiable_in (y,i) & ( partdiff (g,y,i)) = ((( diff (g,y)) * ( reproj (i,( 0. ( REAL-NS m))))) . <*1*>)

    proof

      assume

       A1: g is_differentiable_in y & 1 <= i & i <= m;

      then

      consider f be PartFunc of ( REAL-NS m), ( REAL-NS n), x be Point of ( REAL-NS m) such that

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



       A3: ex f2 be PartFunc of ( REAL-NS m), ( REAL-NS n), x2 be Point of ( REAL-NS m) st f2 = g & x2 = y & ( diff (g,y)) = ( diff (f2,x2)) by A1, PDIFF_1:def 8;



       A4: f is_partial_differentiable_in (x,i) & ( partdiff (f,x,i)) = (( diff (f,x)) * ( reproj (i,( 0. ( REAL-NS m))))) by Th21, A2, A1;

      then g is_partial_differentiable_in (y,i) by A2;

      then ex f1 be PartFunc of ( REAL-NS m), ( REAL-NS n), x1 be Point of ( REAL-NS m) st f1 = g & x1 = y & ( partdiff (g,y,i)) = (( partdiff (f1,x1,i)) . <*1*>) by PDIFF_1:def 14;

      hence thesis by A4, A3, A2;

    end;

    definition

      let n be non zero Nat;

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

      let x be Element of ( REAL n);

      :: PDIFF_7:def1

      pred f is_differentiable_in x means ( <>* f) is_differentiable_in x;

    end

    definition

      let n be non zero Nat;

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

      let x be Element of ( REAL n);

      :: PDIFF_7:def2

      func diff (f,x) -> Function of ( REAL n), REAL equals (( proj (1,1)) * ( diff (( <>* f),x)));

      coherence ;

    end

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

    theorem :: PDIFF_7:23

    h is_differentiable_in y & 1 <= i & i <= m implies h is_partial_differentiable_in (y,i) & ( partdiff (h,y,i)) = ( diff ((h * ( reproj (i,y))),(( proj (i,m)) . y))) & ( partdiff (h,y,i)) = (( diff (h,y)) . (( reproj (i,( 0* m))) . 1))

    proof

      assume

       A1: h is_differentiable_in y & 1 <= i & i <= m;



       A2: ( <>* h) is_partial_differentiable_in (y,i) & ( partdiff (( <>* h),y,i)) = ((( diff (( <>* h),y)) * ( reproj (i,( 0. ( REAL-NS m))))) . <*1*>) by Th22, A1;

      then

       A3: ex g be PartFunc of ( REAL-NS m), ( REAL-NS 1), x be Point of ( REAL-NS m) st ( <>* h) = g & x = y & g is_partial_differentiable_in (x,i);

      hence h is_partial_differentiable_in (y,i) by PDIFF_1: 14;

      thus ( partdiff (h,y,i)) = ( diff ((h * ( reproj (i,y))),(( proj (i,m)) . y)));



       A4: ex k be PartFunc of ( REAL-NS m), ( REAL-NS 1), z be Point of ( REAL-NS m) st ( <>* h) = k & y = z & ( partdiff (( <>* h),y,i)) = (( partdiff (k,z,i)) . <*1*>) by A2, PDIFF_1:def 14;

       <*jj*> in ( REAL 1) by FINSEQ_2: 98;

      then

       A5: <*1*> in the carrier of ( REAL-NS 1) by REAL_NS1:def 4;

       <*( partdiff (h,y,i))*> = ( partdiff (( <>* h),y,i)) by A4, A3, PDIFF_1: 15;

      then

       A6: <*( partdiff (h,y,i))*> = (( diff (( <>* h),y)) . (( reproj (i,( 0. ( REAL-NS m)))) . <*1*>)) by A2, A5, FUNCT_2: 15;

      ( 0. ( REAL-NS m)) = ( 0* m) by REAL_NS1:def 4;

      then ex q be Element of REAL , z be Element of ( REAL m) st <*1*> = <*q*> & z = ( 0* m) & (( reproj (i,( 0. ( REAL-NS m)))) . <*1*>) = (( reproj (i,z)) . q) by A5, PDIFF_1:def 6;

      then (( reproj (i,( 0. ( REAL-NS m)))) . <*1*>) = (( reproj (i,( 0* m))) . 1) by FINSEQ_1: 76;

      then ( partdiff (h,y,i)) = (( proj (1,1)) . (( diff (( <>* h),y)) . (( reproj (i,( 0* m))) . jj))) by A6, PDIFF_1: 1;

      hence ( partdiff (h,y,i)) = (( diff (h,y)) . (( reproj (i,( 0* m))) . 1)) by FUNCT_2: 15;

    end;

    theorem :: PDIFF_7:24



     Th24: for m be non zero Nat, v,w,u be FinSequence of ( REAL m) st ( dom v) = ( dom w) & u = (v + w) holds ( Sum u) = (( Sum v) + ( Sum w))

    proof

      let m be non zero Nat;

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



       A1: P[ 0 ]

      proof

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

        assume

         A2: 0 = ( len zseq) & ( len zseq) = ( len xseq) & ( len zseq) = ( len yseq) & for i be Nat st i in ( dom zseq) holds (zseq /. i) = ((xseq /. i) + (yseq /. i));

        then

         A3: ( Sum zseq) = ( 0* m) & ( Sum yseq) = ( 0* m) by EUCLID_7:def 11;

        ( 0* m) = ( 0. ( TOP-REAL m)) by EUCLID: 70;



        then (( Sum xseq) + ( Sum yseq)) = (( 0. ( TOP-REAL m)) + ( 0. ( TOP-REAL m))) by A2, A3, EUCLID_7:def 11

        .= ( 0. ( TOP-REAL m)) by RLVECT_1: 4;

        hence thesis by A3, EUCLID: 70;

      end;

       A4:

      now

        let i be Nat;

        assume

         A5: P[i];

        now

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

          assume

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

          set xseq0 = (xseq | i);

          set yseq0 = (yseq | i);

          set zseq0 = (zseq | i);



           A7: ( dom xseq) = ( dom yseq) & ( dom zseq) = ( dom yseq) by A6, FINSEQ_3: 29;



           A8: i = ( len xseq0) by A6, FINSEQ_1: 59, NAT_1: 11;

          then

           A9: ( len xseq0) = ( len yseq0) & ( len xseq0) = ( len zseq0) by A6, FINSEQ_1: 59, NAT_1: 11;

          for k be Nat st k in ( dom zseq0) holds (zseq0 /. k) = ((xseq0 /. k) + (yseq0 /. k))

          proof

            let k be Nat;

            assume

             A10: k in ( dom zseq0);

            then

             A11: k in ( dom (yseq | ( Seg i))) & k in ( dom (xseq | ( Seg i))) & k in ( dom (zseq | ( Seg i))) by A9, FINSEQ_3: 29;



             A12: k in ( Seg i) & k in ( dom zseq) by A10, RELAT_1: 57;

            then

             A13: (zseq /. k) = ((xseq /. k) + (yseq /. k)) by A6;



             A14: (xseq /. k) = (xseq . k) by A12, A7, PARTFUN1:def 6

            .= ((xseq | ( Seg i)) . k) by A12, FUNCT_1: 49

            .= ((xseq | ( Seg i)) /. k) by A11, PARTFUN1:def 6;



             A15: (yseq /. k) = (yseq . k) by A7, A12, PARTFUN1:def 6

            .= ((yseq | ( Seg i)) . k) by A12, FUNCT_1: 49

            .= ((yseq | ( Seg i)) /. k) by A11, PARTFUN1:def 6;

            (zseq0 /. k) = ((zseq | ( Seg i)) . k) by A10, PARTFUN1:def 6

            .= (zseq . k) by A12, FUNCT_1: 49;

            hence (zseq0 /. k) = ((xseq0 /. k) + (yseq0 /. k)) by A13, A14, A15, A12, PARTFUN1:def 6;

          end;

          then

           A16: ( Sum zseq0) = (( Sum xseq0) + ( Sum yseq0)) by A8, A9, A5;

          consider v be Element of ( REAL m) such that

           A17: v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum xseq0) + v) by A6, A8, PDIFF_6: 15;

          consider w be Element of ( REAL m) such that

           A18: w = (yseq . ( len yseq)) & ( Sum yseq) = (( Sum yseq0) + w) by A6, A8, A9, PDIFF_6: 15;

          consider t be Element of ( REAL m) such that

           A19: t = (zseq . ( len zseq)) & ( Sum zseq) = (( Sum zseq0) + t) by A6, A8, A9, PDIFF_6: 15;



           A20: ( dom zseq) = ( Seg (i + 1)) by A6, FINSEQ_1:def 3;

          then ( len zseq) in ( dom zseq) by A6, FINSEQ_1: 4;

          then t = (zseq /. ( len zseq)) by A19, PARTFUN1:def 6;

          then

           A21: t = ((xseq /. ( len xseq)) + (yseq /. ( len yseq))) by A6, A20, FINSEQ_1: 4;

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

          then

           A22: v = (xseq /. ( len xseq)) & w = (yseq /. ( len yseq)) by A6, A17, A18, FINSEQ_1: 4, PARTFUN1:def 6;

          reconsider F1 = ( Sum xseq0) as real-valued FinSequence;

          reconsider F2 = ( Sum yseq0) as real-valued FinSequence;

          reconsider F3 = (xseq /. ( len xseq)) as real-valued FinSequence;

          reconsider F4 = (yseq /. ( len yseq)) as real-valued FinSequence;

          ( Sum zseq) = (((F1 + F2) + F3) + F4) by A19, A16, A21, RVSUM_1: 15;

          then ( Sum zseq) = (((F1 + F3) + F2) + F4) by RVSUM_1: 15;

          hence ( Sum zseq) = (( Sum xseq) + ( Sum yseq)) by A22, A17, A18, RVSUM_1: 15;

        end;

        hence P[(i + 1)];

      end;



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

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

      assume

       A24: ( dom xseq) = ( dom yseq) & zseq = (xseq + yseq);

      then

       A25: ( len yseq) = ( len xseq) by FINSEQ_3: 29;

      (xseq + yseq) = (xseq <++> yseq) by INTEGR15:def 9;

      then ( dom zseq) = (( dom xseq) /\ ( dom yseq)) by A24, VALUED_2:def 45;

      then

       A26: ( len zseq) = ( len xseq) by A24, FINSEQ_3: 29;

      for i be Nat st i in ( dom zseq) holds (zseq /. i) = ((xseq /. i) + (yseq /. i)) by A24, INTEGR15: 21;

      hence ( Sum zseq) = (( Sum xseq) + ( Sum yseq)) by A25, A26, A23;

    end;

    theorem :: PDIFF_7:25



     Th25: for m be non zero Nat, r be Real, w,u be FinSequence of ( REAL m) st u = (r (#) w) holds ( Sum u) = (r * ( Sum w))

    proof

      let m be non zero Nat, r be Real;

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



       A1: P[ 0 ]

      proof

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

        assume

         A2: 0 = ( len xseq) & ( len xseq) = ( len yseq) & for i be Nat st i in ( dom xseq) holds (yseq /. i) = (r * (xseq /. i));

        reconsider r1 = r as Real;

        ( Sum xseq) = ( 0* m) by A2, EUCLID_7:def 11;



        then (r * ( Sum xseq)) = (r1 * ( 0. ( TOP-REAL m))) by EUCLID: 70

        .= ( 0. ( TOP-REAL m)) by RLVECT_1: 10

        .= ( 0* m) by EUCLID: 70;

        hence thesis by A2, EUCLID_7:def 11;

      end;

       A3:

      now

        let i be Nat;

        assume

         A4: P[i];

        now

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

          assume

           A5: (i + 1) = ( len xseq) & ( len xseq) = ( len yseq) & for k be Nat st k in ( dom xseq) holds (yseq /. k) = (r * (xseq /. k));

          then

           A6: ( dom xseq) = ( dom yseq) by FINSEQ_3: 29;

          set xseq0 = (xseq | i);

          set yseq0 = (yseq | i);



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

          then

           A8: ( len xseq0) = ( len yseq0) by A5, FINSEQ_1: 59, NAT_1: 11;

          for k be Nat st k in ( dom xseq0) holds (yseq0 /. k) = (r * (xseq0 /. k))

          proof

            let k be Nat;

            assume

             A9: k in ( dom xseq0);

            then

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



             A11: k in ( dom (yseq | ( Seg i))) by A9, A8, FINSEQ_3: 29;



             A12: (xseq /. k) = (xseq . k) by A10, PARTFUN1:def 6

            .= ((xseq | ( Seg i)) . k) by A10, FUNCT_1: 49

            .= (xseq0 /. k) by A9, PARTFUN1:def 6;

            (yseq0 /. k) = ((yseq | ( Seg i)) . k) by A11, PARTFUN1:def 6

            .= (yseq . k) by A10, FUNCT_1: 49

            .= (yseq /. k) by A10, A6, PARTFUN1:def 6;

            hence (yseq0 /. k) = (r * (xseq0 /. k)) by A5, A10, A12;

          end;

          then

           A13: ( Sum yseq0) = (r * ( Sum xseq0)) by A7, A8, A4;

          consider v be Element of ( REAL m) such that

           A14: v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum xseq0) + v) by A5, A7, PDIFF_6: 15;

          consider w be Element of ( REAL m) such that

           A15: w = (yseq . ( len yseq)) & ( Sum yseq) = (( Sum yseq0) + w) by A5, A7, A8, PDIFF_6: 15;



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

          then

           A17: ( len yseq) in ( dom xseq) by A5, FINSEQ_1: 4;



          then w = (yseq /. ( len yseq)) by A15, A6, PARTFUN1:def 6

          .= (r * (xseq /. ( len yseq))) by A5, A16, FINSEQ_1: 4

          .= (r * v) by A17, A5, A14, PARTFUN1:def 6;

          hence ( Sum yseq) = (r * ( Sum xseq)) by A15, A13, A14, RVSUM_1: 51;

        end;

        hence P[(i + 1)];

      end;



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

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



       A19: (r (#) xseq) = (xseq [#] r) by INTEGR15:def 11;

      assume

       A20: yseq = (r (#) xseq);

      then

       A21: ( dom yseq) = ( dom xseq) by A19, VALUED_2:def 39;

      then

       A22: ( len xseq) = ( len yseq) by FINSEQ_3: 29;

      for i be Nat st i in ( dom xseq) holds (yseq /. i) = (r * (xseq /. i)) by A20, A21, INTEGR15: 23;

      hence ( Sum yseq) = (r * ( Sum xseq)) by A22, A18;

    end;



     Lm8: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), x be Element of ( REAL m) holds ex L be Lipschitzian LinearOperator of m, n st for h be Element of ( REAL m) holds ex w be FinSequence of ( REAL n) st ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . h) * ( partdiff (f,x,i)))) & (L . h) = ( Sum w)

    proof

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

      defpred LX[ set, set] means ex w be FinSequence of ( REAL n) st ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . $1) * ( partdiff (f,x,i)))) & $2 = ( Sum w);



       A1: for v be Element of ( REAL m) holds ex y be Element of ( REAL n) st LX[v, y]

      proof

        let v be Element of ( REAL m);

        defpred YX[ set, set] means ex i be Nat st i = $1 & $2 = ((( proj (i,m)) . v) * ( partdiff (f,x,i)));



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

        proof

          let i be Nat;

          assume i in ( Seg m);

          reconsider i0 = i as Nat;

          ((( proj (i0,m)) . v) * ( partdiff (f,x,i0))) in ( REAL n);

          hence thesis;

        end;

        consider w be FinSequence of ( REAL n) such that

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

         A4:

        now

          let i be Nat;

          assume i in ( Seg m);

          then YX[i, (w . i)] by A3;

          hence (w . i) = ((( proj (i,m)) . v) * ( partdiff (f,x,i)));

        end;

        reconsider w0 = ( Sum w) as Element of ( REAL n);

        ex w be FinSequence of ( REAL n) st ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . v) * ( partdiff (f,x,i)))) & w0 = ( Sum w) by A4, A3;

        hence ex y0 be Element of ( REAL n) st LX[v, y0];

      end;

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

       A5: for h be Element of ( REAL m) holds LX[h, (L . h)] from FUNCT_2:sch 3( A1);



       A6: for s,t be Element of ( REAL m) holds (L . (s + t)) = ((L . s) + (L . t))

      proof

        let s,t be Element of ( REAL m);

        consider w be FinSequence of ( REAL n) such that

         A7: ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . s) * ( partdiff (f,x,i)))) & (L . s) = ( Sum w) by A5;

        consider v be FinSequence of ( REAL n) such that

         A8: ( dom v) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (v . i) = ((( proj (i,m)) . t) * ( partdiff (f,x,i)))) & (L . t) = ( Sum v) by A5;

        consider u be FinSequence of ( REAL n) such that

         A9: ( dom u) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (u . i) = ((( proj (i,m)) . (s + t)) * ( partdiff (f,x,i)))) & (L . (s + t)) = ( Sum u) by A5;



         A10: (w + v) = (w <++> v) by INTEGR15:def 9;



         A11: ( dom u) = (( dom w) /\ ( dom v)) by A7, A8, A9;

        now

          let j be object;

          assume

           A12: j in ( dom u);

          then

          reconsider i = j as Nat;



           A13: (w . i) = ((( proj (i,m)) . s) * ( partdiff (f,x,i))) by A7, A9, A12;



           A14: (v . i) = ((( proj (i,m)) . t) * ( partdiff (f,x,i))) by A8, A9, A12;



          thus (u . j) = ((( proj (i,m)) . (s + t)) * ( partdiff (f,x,i))) by A9, A12

          .= (((s + t) . i) * ( partdiff (f,x,i))) by PDIFF_1:def 1

          .= (((s . i) + (t . i)) * ( partdiff (f,x,i))) by RVSUM_1: 11

          .= (((( proj (i,m)) . s) + (t . i)) * ( partdiff (f,x,i))) by PDIFF_1:def 1

          .= (((( proj (i,m)) . s) + (( proj (i,m)) . t)) * ( partdiff (f,x,i))) by PDIFF_1:def 1

          .= ((w . j) + (v . j)) by A13, A14, RVSUM_1: 50;

        end;

        then u = (w + v) by A10, A11, VALUED_2:def 45;

        hence (L . (s + t)) = ((L . s) + (L . t)) by A9, A7, A8, Th24;

      end;

      for s be Element of ( REAL m), r be Real holds (L . (r * s)) = (r * (L . s))

      proof

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

        consider w be FinSequence of ( REAL n) such that

         A15: ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . s) * ( partdiff (f,x,i)))) & (L . s) = ( Sum w) by A5;

        consider u be FinSequence of ( REAL n) such that

         A16: ( dom u) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (u . i) = ((( proj (i,m)) . (r * s)) * ( partdiff (f,x,i)))) & (L . (r * s)) = ( Sum u) by A5;



         A17: (r (#) w) = (w [#] r) by INTEGR15:def 11;

        now

          let j be object;

          assume

           A18: j in ( dom u);

          then

          reconsider i = j as Nat;



           A19: (w . i) = ((( proj (i,m)) . s) * ( partdiff (f,x,i))) by A15, A16, A18;



          thus (u . j) = ((( proj (i,m)) . (r * s)) * ( partdiff (f,x,i))) by A16, A18

          .= (((r * s) . i) * ( partdiff (f,x,i))) by PDIFF_1:def 1

          .= ((r * (s . i)) * ( partdiff (f,x,i))) by RVSUM_1: 45

          .= ((r * (( proj (i,m)) . s)) * ( partdiff (f,x,i))) by PDIFF_1:def 1

          .= (r (#) (w . j)) by A19, RVSUM_1: 49;

        end;

        then u = (r (#) w) by A17, A15, A16, VALUED_2:def 39;

        hence (L . (r * s)) = (r * (L . s)) by A15, A16, Th25;

      end;

      then

      reconsider L as LinearOperator of m, n by A6, PDIFF_6:def 1, PDIFF_6:def 2;

      take L;

      thus thesis by A5;

    end;

    theorem :: PDIFF_7:26



     Th26: for n be non zero Nat, h,g be FinSequence of ( REAL n) st ( len h) = (( len g) + 1) & (for i be Nat st i in ( dom g) holds (g /. i) = ((h /. i) - (h /. (i + 1)))) holds ((h /. 1) - (h /. ( len h))) = ( Sum g)

    proof

      let n be non zero Nat, h,g be FinSequence of ( REAL n);

      assume that

       A1: ( len h) = (( len g) + 1) and

       A2: for i be Nat st i in ( dom g) holds (g /. i) = ((h /. i) - (h /. (i + 1)));

      per cases ;

        suppose

         A3: ( len g) = 0 ;

        then ((h /. 1) - (h /. ( len h))) = ( 0* n) by A1, EUCLIDLP: 9;

        hence thesis by A3, EUCLID_7:def 11;

      end;

        suppose

         A4: ( len g) > 0 ;

        then

         A5: ( Sum g) = (( accum g) . ( len g)) by EUCLID_7:def 11;

        defpred P[ Nat] means $1 <= ( len g) implies (( accum g) . $1) = ((h /. 1) - (h /. ($1 + 1)));



         A6: P[1]

        proof

          assume 1 <= ( len g);

          then 1 in ( Seg ( len g));

          then

           A7: 1 in ( dom g) by FINSEQ_1:def 3;

          (( accum g) . 1) = (g . 1) by EUCLID_7:def 10;

          then (( accum g) . 1) = (g /. 1) by A7, PARTFUN1:def 6;

          hence (( accum g) . 1) = ((h /. 1) - (h /. (1 + 1))) by A7, A2;

        end;



         A8: for j be Nat st 1 <= j holds P[j] implies P[(j + 1)]

        proof

          let j be Nat;

          assume

           A9: 1 <= j;

          assume

           A10: P[j];

          assume

           A11: (j + 1) <= ( len g);

          then

           A12: j < ( len g) by NAT_1: 13;

          1 <= (j + 1) by XREAL_1: 38;

          then

           A13: (j + 1) in ( dom g) by A11, FINSEQ_3: 25;

          ( len g) = ( len ( accum g)) by EUCLID_7:def 10;

          then

           A14: j in ( dom ( accum g)) by A9, A12, FINSEQ_3: 25;

          (( accum g) . (j + 1)) = ((( accum g) /. j) + (g /. (j + 1))) by A9, A12, EUCLID_7:def 10;

          then

           A15: (( accum g) . (j + 1)) = ((( accum g) /. j) + ((h /. (j + 1)) - (h /. ((j + 1) + 1)))) by A2, A13;

          reconsider hj1 = (h /. (j + 1)) as Point of ( TOP-REAL n) by EUCLID: 22;

          reconsider hj2 = (h /. (j + 2)) as Point of ( TOP-REAL n) by EUCLID: 22;

          reconsider hj3 = ((h /. 1) - (h /. (j + 1))) as Point of ( TOP-REAL n) by EUCLID: 22;

          (( accum g) . (j + 1)) = (hj3 + (hj1 - hj2)) by A15, A10, A11, A14, NAT_1: 13, PARTFUN1:def 6;

          then (( accum g) . (j + 1)) = ((hj3 + hj1) - hj2) by RLVECT_1:def 3;

          hence thesis by RVSUM_1: 43;

        end;



         A16: 1 <= ( len g) by A4, NAT_1: 14;

        for i be Nat st 1 <= i holds P[i] from NAT_1:sch 8( A6, A8);

        hence thesis by A5, A1, A16;

      end;

    end;

    theorem :: PDIFF_7:27



     Th27: for n be non zero Nat, h,g,j be FinSequence of ( REAL n) st ( len h) = ( len j) & ( len g) = ( len j) & (for i be Nat st i in ( dom j) holds (j /. i) = ((h /. i) - (g /. i))) holds ( Sum j) = (( Sum h) - ( Sum g))

    proof

      let n be non zero Nat, h,g,j be FinSequence of ( REAL n);

      assume that

       A1: ( len h) = ( len j) & ( len g) = ( len j) and

       A2: for i be Nat st i in ( dom j) holds (j /. i) = ((h /. i) - (g /. i));



       A3: ( dom j) = ( Seg ( len j)) & ( dom g) = ( Seg ( len g)) & ( dom h) = ( Seg ( len h)) by FINSEQ_1:def 3;



       A4: for i be Nat st i in ( dom h) holds (h /. i) = ((j /. i) + (g /. i))

      proof

        let i be Nat;

        reconsider ji = (j /. i), hi = (h /. i), gi = (g /. i) as Point of ( TOP-REAL n) by EUCLID: 22;

        assume i in ( dom h);

        then ji = (hi - gi) by A1, A2, A3;

        then (ji + gi) = hi by RLVECT_4: 1;

        hence thesis;

      end;

      (j + g) = (j <++> g) by INTEGR15:def 9;

      then

       A5: ( dom (j + g)) = (( dom j) /\ ( dom g)) by VALUED_2:def 45;

      reconsider Sj = ( Sum j), Sh = ( Sum h), Sg = ( Sum g) as Point of ( TOP-REAL n) by EUCLID: 22;

      for k be Element of NAT st k in ( dom h) holds (h . k) = ((j + g) . k)

      proof

        let k be Element of NAT ;

        assume

         A6: k in ( dom h);

        then (h /. k) = ((j /. k) + (g /. k)) by A4;

        then

         A7: (h . k) = ((j /. k) + (g /. k)) by A6, PARTFUN1:def 6;

        ((j + g) /. k) = ((j /. k) + (g /. k)) by A6, A1, A3, A5, INTEGR15: 21;

        hence thesis by A7, A6, A1, A3, A5, PARTFUN1:def 6;

      end;

      then Sh = (Sj + Sg) by A1, A3, Th24, A5, PARTFUN1: 5;

      then (Sh - Sg) = Sj by RLVECT_4: 1;

      hence (( Sum h) - ( Sum g)) = ( Sum j);

    end;

    theorem :: PDIFF_7:28



     Th28: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), x,y be Element of ( REAL m) holds ex h be FinSequence of ( REAL m), g be FinSequence of ( REAL n) st ( len h) = (m + 1) & ( len g) = m & (for i be Nat st i in ( dom h) holds (h /. i) = ((y | ((m + 1) -' i)) ^ ( 0* (i -' 1)))) & (for i be Nat st i in ( dom g) holds (g /. i) = ((f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))))) & (for i be Nat, hi be Element of ( REAL m) st i in ( dom h) & (h /. i) = hi holds |.hi.| <= |.y.|) & ((f /. (x + y)) - (f /. x)) = ( Sum g)

    proof

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

      reconsider mm = m as Element of NAT by ORDINAL1:def 12;



       A1: ( len y) = mm by FINSEQ_2: 133;

      defpred H[ Nat, set] means $2 = ((y | ((m + 1) -' $1)) ^ ( 0* ($1 -' 1)));



       A2: for k be Nat st k in ( Seg (m + 1)) holds ex x be Element of ( REAL m) st H[k, x]

      proof

        let k be Nat;

        assume k in ( Seg (m + 1));

        then

         A3: 1 <= k & k <= (m + 1) by FINSEQ_1: 1;

        then (k - 1) >= 0 & ((m + 1) - k) >= 0 by XREAL_1: 48;

        then

         A4: ((m + 1) -' k) = ((m + 1) - k) & (k -' 1) = (k - 1) by XREAL_0:def 2;

        set l1 = ((m + 1) -' k);

        set l2 = (k -' 1);

        (m + 1) <= (m + k) by A3, XREAL_1: 6;

        then l1 <= ( len y) by A1, A4, XREAL_1: 20;

        then

         A5: ( len (y | l1)) = l1 by FINSEQ_1: 59;

        ( len ( 0* l2)) = l2 by FINSEQ_2: 132;

        then ( len ((y | l1) ^ ( 0* l2))) = (l1 + l2) by A5, FINSEQ_1: 22;

        then ((y | l1) ^ ( 0* l2)) is Element of ((l1 + l2) -tuples_on REAL ) by FINSEQ_2: 133;

        hence thesis by A4;

      end;

      consider h be FinSequence of ( REAL m) such that

       A6: ( dom h) = ( Seg (m + 1)) & for j be Nat st j in ( Seg (m + 1)) holds H[j, (h . j)] from FINSEQ_1:sch 5( A2);

       A7:

      now

        let j be Nat;

        assume

         A8: j in ( dom h);

        then (h /. j) = (h . j) by PARTFUN1:def 6;

        hence (h /. j) = ((y | ((m + 1) -' j)) ^ ( 0* (j -' 1))) by A8, A6;

      end;

      deffunc Z( Nat) = (f /. (x + (h /. $1)));

      consider z be FinSequence of ( REAL n) such that

       A9: ( len z) = (m + 1) & for j be Nat st j in ( dom z) holds (z . j) = Z(j) from FINSEQ_2:sch 1;

       A10:

      now

        let j be Nat;

        assume

         A11: j in ( dom z);

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

        hence (z /. j) = (f /. (x + (h /. j))) by A11, A9;

      end;

      deffunc G( Nat) = ((z /. $1) - (z /. ($1 + 1)));

      consider g be FinSequence of ( REAL n) such that

       A12: ( len g) = m & for j be Nat st j in ( dom g) holds (g . j) = G(j) from FINSEQ_2:sch 1;

       A13:

      now

        let j be Nat;

        assume

         A14: j in ( dom g);

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

        hence (g /. j) = ((z /. j) - (z /. (j + 1))) by A14, A12;

      end;



       A15: 1 <= (m + 1) by NAT_1: 11;



       A16: ((m + 1) -' 1) = ((m + 1) - 1) by NAT_1: 11, XREAL_1: 233;

      1 in ( dom h) by A6, A15;

      then (h /. 1) = ((y | ((m + 1) -' 1)) ^ ( 0* (1 -' 1))) by A7;

      then (h /. 1) = ((y | m) ^ ( 0* 0 )) by A16, XREAL_1: 232;

      then (h /. 1) = (y ^ ( 0* 0 )) by A1, FINSEQ_1: 58;

      then

       A17: (h /. 1) = y by FINSEQ_1: 34;



       A18: 1 <= ( len z) & ( len z) <= (m + 1) by A9, NAT_1: 14;



       A19: ((m + 1) -' ( len z)) = ((m + 1) - ( len z)) by A9, XREAL_1: 233;



       A20: (( len z) -' 1) = (( len z) - 1) by A9, NAT_1: 14, XREAL_1: 233;

      ( len z) in ( dom h) by A6, A18;

      then (h /. ( len z)) = ((y | 0 ) ^ ( 0* (( len z) -' 1))) by A7, A19, A9;

      then

       A21: (h /. ( len z)) = ( 0* m) by A20, A9, FINSEQ_1: 34;

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

      then 1 in ( Seg (m + 1));

      then 1 in ( dom z) by A9, FINSEQ_1:def 3;

      then

       A22: (z /. 1) = (f /. (x + y)) by A10, A17;

      ( len z) in ( Seg (m + 1)) by A9, FINSEQ_1: 4;

      then ( len z) in ( dom z) by A9, FINSEQ_1:def 3;

      then (z /. ( len z)) = (f /. (x + (h /. ( len z)))) by A10;

      then

       A23: (z /. ( len z)) = (f /. x) by A21, EUCLID_4: 1;

      take h, g;

      (m + 1) in NAT by ORDINAL1:def 12;

      hence ( len h) = (m + 1) & ( len g) = m by A6, A12, FINSEQ_1:def 3;

       A24:

      now

        let i be Nat;

        assume

         A25: i in ( dom g);

        then

         A26: i in ( Seg m) by A12, FINSEQ_1:def 3;

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

        then

         A27: ( Seg m) c= ( Seg (m + 1)) by FINSEQ_1: 5;

        ( dom h) = ( dom z) by A6, A9, FINSEQ_1:def 3;

        then

         A28: (z /. i) = (f /. (x + (h /. i))) by A10, A27, A6, A26;

        i in ( Seg m) by A12, A25, FINSEQ_1:def 3;

        then 1 <= i & i <= m by FINSEQ_1: 1;

        then

         A29: (i + 1) <= (m + 1) by XREAL_1: 6;

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

        then (i + 1) in ( Seg (m + 1)) by A29;

        then (i + 1) in ( dom z) by A9, FINSEQ_1:def 3;

        then (z /. (i + 1)) = (f /. (x + (h /. (i + 1)))) by A10;

        hence (g /. i) = ((f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1))))) by A13, A25, A28;

      end;

      for i be Nat, hi be Element of ( REAL m) st i in ( dom h) & (h /. i) = hi holds |.hi.| <= |.y.|

      proof

        let i be Nat, hi be Element of ( REAL m);

        assume i in ( dom h) & (h /. i) = hi;

        then

         A30: hi = ((y | ((m + 1) -' i)) ^ ( 0* (i -' 1))) by A7;



         A31: for j be Nat st j in ( Seg m) holds (( sqr hi) . j) <= (( sqr y) . j)

        proof

          let j be Nat;

          assume

           A32: j in ( Seg m);

          ( len hi) = m by CARD_1:def 7;

          then

           A33: j in ( dom ((y | ((m + 1) -' i)) ^ ( 0* (i -' 1)))) by A32, A30, FINSEQ_1:def 3;

          per cases by A33, FINSEQ_1: 25;

            suppose

             A34: j in ( dom (y | ((m + 1) -' i)));

            then j in ( Seg ( len (y | ((m + 1) -' i)))) by FINSEQ_1:def 3;

            then

             A35: j <= ( len (y | ((m + 1) -' i))) by FINSEQ_1: 1;



             A36: ( len (y | ((m + 1) -' i))) <= ((m + 1) -' i) by FINSEQ_5: 17;

            (( sqr hi) . j) = (( sqrreal * hi) . j) by RVSUM_1:def 8

            .= ( sqrreal . (((y | ((m + 1) -' i)) ^ ( 0* (i -' 1))) . j)) by A30, A33, FUNCT_1: 13

            .= ( sqrreal . ((y | ((m + 1) -' i)) . j)) by A34, FINSEQ_1:def 7

            .= ( sqrreal . (y . j)) by A36, A35, FINSEQ_3: 112, XXREAL_0: 2

            .= ((y . j) ^2 ) by RVSUM_1:def 2

            .= (( sqr y) . j) by VALUED_1: 11;

            hence thesis;

          end;

            suppose ex k be Nat st k in ( dom ( 0* (i -' 1))) & j = (( len (y | ((m + 1) -' i))) + k);

            then

            consider k be Nat such that

             A37: k in ( dom ( 0* (i -' 1))) & j = (( len (y | ((m + 1) -' i))) + k);



             A38: (( sqr hi) . j) = (( sqrreal * hi) . j) by RVSUM_1:def 8

            .= ( sqrreal . (((y | ((m + 1) -' i)) ^ ( 0* (i -' 1))) . j)) by A30, A33, FUNCT_1: 13

            .= ( sqrreal . (( 0* (i -' 1)) . k)) by A37, FINSEQ_1:def 7

            .= ((( 0* (i -' 1)) . k) ^2 ) by RVSUM_1:def 2

            .= 0 ;

            (( sqr y) . j) = ((y . j) ^2 ) by VALUED_1: 11

            .= ((y . j) * (y . j));

            hence thesis by A38, XREAL_1: 63;

          end;

        end;

         0 <= ( Sum ( sqr hi)) by RVSUM_1: 86;

        hence |.hi.| <= |.y.| by A31, RVSUM_1: 82, SQUARE_1: 26;

      end;

      hence thesis by A7, A22, A23, A24, A9, A12, A13, Th26;

    end;

    theorem :: PDIFF_7:29



     Th29: for m be non zero Nat, f be PartFunc of ( REAL m), ( REAL 1) holds ex f0 be PartFunc of ( REAL m), REAL st f = ( <>* f0)

    proof

      let m be non zero Nat, f be PartFunc of ( REAL m), ( REAL 1);

      defpred P[ object] means $1 in ( dom f);

      deffunc F( object) = (( proj (1,1)) . (f /. $1));



       A1: for x be object st P[x] holds F(x) in REAL ;

      consider f0 be PartFunc of ( REAL m), REAL such that

       A2: (for x be object holds x in ( dom f0) iff x in ( REAL m) & P[x]) & for x be object st x in ( dom f0) holds (f0 . x) = F(x) from PARTFUN1:sch 3( A1);

      take f0;

      for x be object st x in ( dom f) holds x in ( dom f0) by A2;

      then

       A3: ( dom f) c= ( dom f0);

      for x be object st x in ( dom f0) holds x in ( dom f) by A2;

      then

       A4: ( dom f0) c= ( dom f);

      then

       A5: ( dom f) = ( dom f0) by A3;



       A6: ( rng f0) c= ( dom (( proj (1,1)) qua Function " )) by PDIFF_1: 2;

      then

       A7: ( dom ((( proj (1,1)) qua Function " ) * f0)) = ( dom f0) by RELAT_1: 27;

      for x be Element of ( REAL m) st x in ( dom ( <>* f0)) holds (( <>* f0) . x) = (f . x)

      proof

        let x be Element of ( REAL m);

        assume

         A8: x in ( dom ( <>* f0));

        then (( <>* f0) . x) = ((( proj (1,1)) qua Function " ) . (f0 . x)) by FUNCT_1: 12;

        then

         A9: (( <>* f0) . x) = ((( proj (1,1)) qua Function " ) . (( proj (1,1)) . (f /. x))) by A8, A7, A2;

        (f /. x) is Element of (1 -tuples_on REAL );

        then

        consider x0 be Element of REAL such that

         A10: (f /. x) = <*x0*> by FINSEQ_2: 97;

        (( proj (1,1)) . (f /. x)) = x0 by A10, PDIFF_1: 1;

        then (( <>* f0) . x) = (f /. x) by A9, A10, PDIFF_1: 1;

        hence thesis by A7, A4, A8, PARTFUN1:def 6;

      end;

      hence f = ( <>* f0) by A6, A5, PARTFUN1: 5, RELAT_1: 27;

    end;

    theorem :: PDIFF_7:30



     Th30: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), f0 be PartFunc of ( REAL-NS m), ( REAL-NS n), x be Element of ( REAL m), x0 be Element of ( REAL-NS m) st x in ( dom f) & x = x0 & f = f0 holds (f /. x) = (f0 /. x0)

    proof

      let m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), f0 be PartFunc of ( REAL-NS m), ( REAL-NS n), x be Element of ( REAL m), x0 be Element of ( REAL-NS m);

      assume

       A1: x in ( dom f) & x = x0 & f = f0;

      then (f /. x) = (f0 . x0) by PARTFUN1:def 6;

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

    end;

    definition

      let m be non zero Nat;

      let X be Subset of ( REAL m);

      :: PDIFF_7:def3

      attr X is open means ex X0 be Subset of ( REAL-NS m) st X0 = X & X0 is open;

    end

    theorem :: PDIFF_7:31



     Th31: for m be non zero Nat, X be Subset of ( REAL m) holds X is open iff for x be Element of ( REAL m) st x in X holds ex r be Real st r > 0 & { y where y be Element of ( REAL m) : |.(y - x).| < r } c= X

    proof

      let m be non zero Nat, X be Subset of ( REAL m);

      hereby

        assume X is open;

        then

        consider VV0 be Subset of ( REAL-NS m) such that

         A1: X = VV0 & VV0 is open;

        let x be Element of ( REAL m);

        assume

         A2: x in X;

        reconsider V0 = VV0 as Subset of ( TopSpaceNorm ( REAL-NS m));

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

        V0 is open by A1, NORMSP_2: 16;

        then

        consider d0 be Real such that

         A3: d0 > 0 & { w where w be Point of ( REAL-NS m) : ||.(v0 - w).|| < d0 } c= V0 by A2, A1, NORMSP_2: 7;

        take d0;

        thus 0 < d0 by A3;

        thus { y where y be Element of ( REAL m) : |.(y - x).| < d0 } c= X

        proof

          let z be object;

          assume z in { y where y be Element of ( REAL m) : |.(y - x).| < d0 };

          then

          consider y be Element of ( REAL m) such that

           A4: z = y & |.(y - x).| < d0;

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

           |.(y - x).| = ||.(w - v0).|| by REAL_NS1: 1, REAL_NS1: 5;

          then ||.(v0 - w).|| < d0 by A4, NORMSP_1: 7;

          then w in { w1 where w1 be Point of ( REAL-NS m) : ||.(v0 - w1).|| < d0 };

          hence z in X by A4, A1, A3;

        end;

      end;

      assume

       A5: for x be Element of ( REAL m) st x in X holds ex r be Real st r > 0 & { y where y be Element of ( REAL m) : |.(y - x).| < r } c= X;

      reconsider VV0 = X as Subset of ( REAL-NS m) by REAL_NS1:def 4;

      reconsider V0 = VV0 as Subset of ( TopSpaceNorm ( REAL-NS m));

      for v be Point of ( REAL-NS m) st v in V0 holds ex r be Real st r > 0 & { w where w be Point of ( REAL-NS m) : ||.(v - w).|| < r } c= V0

      proof

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

        assume

         A6: v in V0;

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

        consider d0 be Real such that

         A7: d0 > 0 & { y where y be Element of ( REAL m) : |.(y - x).| < d0 } c= X by A5, A6;

        take d0;

        thus 0 < d0 by A7;

        thus { w where w be Point of ( REAL-NS m) : ||.(v - w).|| < d0 } c= V0

        proof

          let z be object;

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

          then

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

           A8: z = w & ||.(v - w).|| < d0;

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

           |.(y - x).| = ||.(w - v).|| by REAL_NS1: 1, REAL_NS1: 5;

          then |.(y - x).| < d0 by A8, NORMSP_1: 7;

          then y in { t where t be Element of ( REAL m) : |.(t - x).| < d0 };

          hence z in V0 by A8, A7;

        end;

      end;

      then V0 is open by NORMSP_2: 7;

      then VV0 is open by NORMSP_2: 16;

      hence X is open;

    end;

    definition

      let m,n be non zero Nat;

      let i be Nat;

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

      let X be set;

      :: PDIFF_7:def4

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

    end

    theorem :: PDIFF_7:32



     Th32: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n) st f is_partial_differentiable_on (X,i) holds X is Subset of ( REAL m) by XBOOLE_1: 1;

    theorem :: PDIFF_7:33



     Th33: for m,n be non zero Nat, i be Nat, f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n), Z be set st f = g holds f is_partial_differentiable_on (Z,i) iff g is_partial_differentiable_on (Z,i)

    proof

      let m,n be non zero Nat, i be Nat, f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n), Z be set;

      assume

       A1: f = g;

      hereby

        assume

         A2: f is_partial_differentiable_on (Z,i);

        then

         A3: Z c= ( dom f) & for x be Element of ( REAL m) st x in Z holds (f | Z) is_partial_differentiable_in (x,i);

        now

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

          assume

           A4: y in Z;

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

          (f | Z) is_partial_differentiable_in (x,i) by A2, A4;

          then ex gZ be PartFunc of ( REAL-NS m), ( REAL-NS n), y be Point of ( REAL-NS m) st (f | Z) = gZ & x = y & gZ is_partial_differentiable_in (y,i);

          hence (g | Z) is_partial_differentiable_in (y,i) by A1;

        end;

        hence g is_partial_differentiable_on (Z,i) by A1, A3;

      end;

      assume

       A5: g is_partial_differentiable_on (Z,i);

      then

       A6: Z c= ( dom g) & for y be Point of ( REAL-NS m) st y in Z holds (g | Z) is_partial_differentiable_in (y,i);

      now

        let x be Element of ( REAL m);

        assume

         A7: x in Z;

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

        (g | Z) is_partial_differentiable_in (y,i) by A5, A7;

        hence (f | Z) is_partial_differentiable_in (x,i) by A1;

      end;

      hence f is_partial_differentiable_on (Z,i) by A1, A6;

    end;

    theorem :: PDIFF_7:34



     Th34: for m,n be non zero Nat, i be Nat, f be PartFunc of ( REAL m), ( REAL n), Z be Subset of ( REAL m) st Z is open & 1 <= i & i <= m holds f is_partial_differentiable_on (Z,i) iff Z c= ( dom f) & for x be Element of ( REAL m) st x in Z holds f is_partial_differentiable_in (x,i)

    proof

      let m,n be non zero Nat, i be Nat, f be PartFunc of ( REAL m), ( REAL n), Z be Subset of ( REAL m);

      assume

       A1: Z is open & 1 <= i & i <= m;

      then

      consider Z0 be Subset of ( REAL-NS m) such that

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

      hereby

        assume f is_partial_differentiable_on (Z,i);

        then

         A3: g is_partial_differentiable_on (Z0,i) by A2, Th33;

        hence Z c= ( dom f) by A2;

        thus for x be Element of ( REAL m) st x in Z holds f is_partial_differentiable_in (x,i)

        proof

          let x be Element of ( REAL m);

          assume

           A4: x in Z;

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

          g is_partial_differentiable_in (y,i) by A2, A3, A4, A1, Th8;

          hence f is_partial_differentiable_in (x,i);

        end;

      end;

      assume

       A5: Z c= ( dom f) & for x be Element of ( REAL m) st x in Z holds f is_partial_differentiable_in (x,i);

      now

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

        assume

         A6: y in Z0;

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

        f is_partial_differentiable_in (x,i) by A2, A6, A5;

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

        hence g is_partial_differentiable_in (y,i);

      end;

      then g is_partial_differentiable_on (Z0,i) by A1, Th8, A2, A5;

      hence f is_partial_differentiable_on (Z,i) by Th33, A2;

    end;

    definition

      let m,n be non zero Nat;

      let i be Nat;

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

      let X;

      assume

       A1: f is_partial_differentiable_on (X,i);

      :: PDIFF_7:def5

      func f `partial| (X,i) -> PartFunc of ( REAL m), ( REAL n) means

      : Def5: ( dom it ) = X & for x be Element of ( REAL m) st x in X holds (it /. x) = ( partdiff (f,x,i));

      existence

      proof

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

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

        consider F be PartFunc of ( REAL m), ( REAL n) such that

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

        take F;

        now



           A3: X is Subset of ( REAL m) by A1, Th32;

          let y be object;

          assume y in X;

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

        end;

        then

         A4: X c= ( dom F);

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

        then ( dom F) c= X;

        hence ( dom F) = X by A4;

        hereby

          let x be Element of ( REAL m);

          assume x in X;

          then

           A5: x in ( dom F) by A2;

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

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

        end;

      end;

      uniqueness

      proof

        let F,G be PartFunc of ( REAL m), ( REAL n);

        assume that

         A6: ( dom F) = X and

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

         A8: ( dom G) = X and

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

        now

          let x be Element of ( REAL m);

          assume

           A10: x in ( dom F);

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

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

        end;

        hence thesis by A6, A8, PARTFUN2: 1;

      end;

    end

    definition

      let m,n be non zero Nat;

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

      let x0 be Element of ( REAL m);

      :: PDIFF_7:def6

      pred f is_continuous_in x0 means ex y0 be Point of ( REAL-NS m), g be PartFunc of ( REAL-NS m), ( REAL-NS n) st x0 = y0 & f = g & g is_continuous_in y0;

    end

    theorem :: PDIFF_7:35

    for m,n 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_continuous_in x iff g is_continuous_in y;

    theorem :: PDIFF_7:36

    for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), x0 be Element of ( REAL m) holds f is_continuous_in x0 iff (x0 in ( dom f) & for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r)

    proof

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

      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 y0 = x0 as Point of ( REAL-NS m) by REAL_NS1:def 4;

      hereby

        assume f is_continuous_in x0;

        then

         A1: g is_continuous_in y0;

        then

         A2: y0 in ( dom g) & for r be Real st 0 < r holds ex s be Real st 0 < s & for y1 be Point of ( REAL-NS m) st y1 in ( dom g) & ||.(y1 - y0).|| < s holds ||.((g /. y1) - (g /. y0)).|| < r by NFCONT_1: 7;

        thus x0 in ( dom f) by A1, NFCONT_1: 7;

        thus for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider s be Real such that

           A3: 0 < s & for y1 be Point of ( REAL-NS m) st y1 in ( dom g) & ||.(y1 - y0).|| < s holds ||.((g /. y1) - (g /. y0)).|| < r by A1, NFCONT_1: 7;

          take s;

          thus 0 < s by A3;

          hereby

            let x1 be Element of ( REAL m);

            assume

             A4: x1 in ( dom f) & |.(x1 - x0).| < s;

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

            y1 in ( dom g) & ||.(y1 - y0).|| < s by A4, REAL_NS1: 1, REAL_NS1: 5;

            then

             A5: ||.((g /. y1) - (g /. y0)).|| < r by A3;

            (g /. y1) = (f /. x1) & (g /. y0) = (f /. x0) by A2, Th30, A4;

            hence |.((f /. x1) - (f /. x0)).| < r by A5, REAL_NS1: 1, REAL_NS1: 5;

          end;

        end;

      end;

      assume

       A6: x0 in ( dom f) & for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r;

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

      for r be Real st 0 < r holds ex s be Real st 0 < s & for y1 be Point of ( REAL-NS m) st y1 in ( dom g) & ||.(y1 - y0).|| < s holds ||.((g /. y1) - (g /. y0)).|| < r

      proof

        let r be Real;

        assume 0 < r;

        then

        consider s be Real such that

         A7: 0 < s & for x1 be Element of ( REAL m) st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r by A6;

        take s;

        thus 0 < s by A7;

        hereby

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

          assume

           A8: y1 in ( dom g) & ||.(y1 - y0).|| < s;

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

          x1 in ( dom f) & |.(x1 - x0).| < s by A8, REAL_NS1: 1, REAL_NS1: 5;

          then

           A9: |.((f /. x1) - (f /. x0)).| < r by A7;

          (g /. y1) = (f /. x1) & (g /. y0) = (f /. x0) by A8, A6, Th30;

          hence ||.((g /. y1) - (g /. y0)).|| < r by A9, REAL_NS1: 1, REAL_NS1: 5;

        end;

      end;

      then g is_continuous_in y0 by A6, NFCONT_1: 7;

      hence f is_continuous_in x0;

    end;

    definition

      let m,n be non zero Nat;

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

      let X;

      :: PDIFF_7:def7

      pred f is_continuous_on X means X c= ( dom f) & for x0 be Element of ( REAL m) st x0 in X holds (f | X) is_continuous_in x0;

    end

    theorem :: PDIFF_7:37



     Th37: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n), X be set st f = g holds f is_continuous_on X iff g is_continuous_on X

    proof

      let m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), g be PartFunc of ( REAL-NS m), ( REAL-NS n), X be set;

      assume

       A1: f = g;

      hereby

        assume

         A2: f is_continuous_on X;

        then

         A3: X c= ( dom f) & for x0 be Element of ( REAL m) st x0 in X holds (f | X) is_continuous_in x0;

        now

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

          assume

           A4: y0 in X;

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

          (f | X) is_continuous_in x0 by A2, A4;

          hence (g | X) is_continuous_in y0 by A1;

        end;

        hence g is_continuous_on X by A3, A1, NFCONT_1:def 7;

      end;

      assume

       A5: g is_continuous_on X;

      then

       A6: X c= ( dom g) & for y0 be Point of ( REAL-NS m) st y0 in X holds (g | X) is_continuous_in y0 by NFCONT_1:def 7;

      now

        let x0 be Element of ( REAL m);

        assume

         A7: x0 in X;

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

        (g | X) is_continuous_in y0 by A5, A7, NFCONT_1:def 7;

        hence (f | X) is_continuous_in x0 by A1;

      end;

      hence f is_continuous_on X by A6, A1;

    end;

    theorem :: PDIFF_7:38



     Th38: for m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), X be set holds f is_continuous_on X iff X c= ( dom f) & for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

    proof

      let m,n be non zero Nat, f be PartFunc of ( REAL m), ( REAL n), X be set;

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

      hereby

        assume f is_continuous_on X;

        then

         A1: g is_continuous_on X by Th37;

        hence

         A2: X c= ( dom f) by NFCONT_1: 19;

        thus for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

        proof

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

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

          assume

           A3: x0 in X & 0 < r;

          then

          consider s be Real such that

           A4: 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.((g /. y1) - (g /. y0)).|| < r by A1, NFCONT_1: 19;

          take s;

          thus 0 < s by A4;

          hereby

            let x1 be Element of ( REAL m);

            assume

             A5: x1 in X & |.(x1 - x0).| < s;

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

            y1 in X & ||.(y1 - y0).|| < s by A5, REAL_NS1: 1, REAL_NS1: 5;

            then

             A6: ||.((g /. y1) - (g /. y0)).|| < r by A4;

            (g /. y1) = (f /. x1) & (g /. y0) = (f /. x0) by A5, A2, A3, Th30;

            hence |.((f /. x1) - (f /. x0)).| < r by A6, REAL_NS1: 1, REAL_NS1: 5;

          end;

        end;

      end;

      assume

       A7: X c= ( dom f) & for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r;

      for y0 be Point of ( REAL-NS m), r be Real st y0 in X & 0 < r holds ex s be Real st 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.((g /. y1) - (g /. y0)).|| < r

      proof

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

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

        assume

         A8: y0 in X & 0 < r;

        then

        consider s be Real such that

         A9: 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r by A7;

        take s;

        thus 0 < s by A9;

        hereby

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

          assume

           A10: y1 in X & ||.(y1 - y0).|| < s;

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

          x1 in X & |.(x1 - x0).| < s by A10, REAL_NS1: 1, REAL_NS1: 5;

          then

           A11: |.((f /. x1) - (f /. x0)).| < r by A9;

          (g /. y1) = (f /. x1) & (g /. y0) = (f /. x0) by A10, A7, A8, Th30;

          hence ||.((g /. y1) - (g /. y0)).|| < r by A11, REAL_NS1: 1, REAL_NS1: 5;

        end;

      end;

      then g is_continuous_on X by A7, NFCONT_1: 19;

      hence f is_continuous_on X by Th37;

    end;

    theorem :: PDIFF_7:39



     Th39: for m be non zero Nat, x,y be Element of ( REAL m), i be Nat, xi be Real st 1 <= i & i <= m & y = (( reproj (i,x)) . xi) holds (( proj (i,m)) . y) = xi

    proof

      let m be non zero Nat, x,y be Element of ( REAL m), i be Nat, xi be Real;

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

      assume

       A1: 1 <= i & i <= m & y = (( reproj (i,x)) . xi);

      then

       A2: y = ( Replace (x,i,xx)) by PDIFF_1:def 5;



       A3: ( len x) = m & ( len y) = m by CARD_1:def 7;

      then

       A4: i in ( dom y) by A1, FINSEQ_3: 25;

      (y /. i) = xi by A1, A2, A3, FINSEQ_7: 8;

      then (y . i) = xi by A4, PARTFUN1:def 6;

      hence (( proj (i,m)) . y) = xi by PDIFF_1:def 1;

    end;

    theorem :: PDIFF_7:40



     Th40: for m be non zero Nat, f be PartFunc of ( REAL m), REAL , x,y be Element of ( REAL m), i be Nat, xi be Real st 1 <= i & i <= m & y = (( reproj (i,x)) . xi) holds ( reproj (i,x)) = ( reproj (i,y))

    proof

      let m be non zero Nat, f be PartFunc of ( REAL m), REAL , x,y be Element of ( REAL m), i be Nat, xi be Real;

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

      assume

       A1: 1 <= i & i <= m & y = (( reproj (i,x)) . xi);

      then

       A2: y = ( Replace (x,i,xx)) by PDIFF_1:def 5;



       A3: ( len x) = m & ( len y) = m by CARD_1:def 7;

      then

       A4: y = (((x | (i -' 1)) ^ <*xi*>) ^ (x /^ i)) by A1, A2, FINSEQ_7:def 1;



       A5: ( dom ( reproj (i,x))) = REAL by PDIFF_1:def 5

      .= ( dom ( reproj (i,y))) by PDIFF_1:def 5;

      for r be object st r in ( dom ( reproj (i,x))) holds (( reproj (i,x)) . r) = (( reproj (i,y)) . r)

      proof

        let r be object;

        assume

         A6: r in ( dom ( reproj (i,x)));



         A7: (i -' 1) <= ( len y) & (i -' 1) <= ( len x) by A1, A3, NAT_D: 44;

        reconsider r1 = r as Element of REAL by A6;

        (( reproj (i,x)) . r) = ( Replace (x,i,r1)) by PDIFF_1:def 5;

        then

         A8: (( reproj (i,x)) . r) = (((x | (i -' 1)) ^ <*r1*>) ^ (x /^ i)) by A1, A3, FINSEQ_7:def 1;

        (( reproj (i,y)) . r) = ( Replace (y,i,r1)) by PDIFF_1:def 5;

        then

         A9: (( reproj (i,y)) . r) = (((y | (i -' 1)) ^ <*r1*>) ^ (y /^ i)) by A1, A3, FINSEQ_7:def 1;



         A10: ( dom (y | (i -' 1))) = ( Seg (i -' 1)) by A7, FINSEQ_1: 17;

        then

         A11: ( dom (y | (i -' 1))) = ( dom (x | (i -' 1))) by A7, FINSEQ_1: 17;



         A12: for n be Nat st n in ( dom (y | (i -' 1))) holds ((y | (i -' 1)) /. n) = ((x | (i -' 1)) /. n)

        proof

          let n be Nat;

          assume

           A13: n in ( dom (y | (i -' 1)));

          then n in ( Seg ( len (x | (i -' 1)))) by A7, A10, FINSEQ_1: 17;

          then

           A14: n <= ( len (x | (i -' 1))) by FINSEQ_1: 1;



           A15: ( len (x | (i -' 1))) <= (i -' 1) by FINSEQ_5: 17;



           A16: 1 <= n & n <= ( len (x | (i -' 1))) by A13, A11, FINSEQ_3: 25;

          ((y | (i -' 1)) /. n) = ((y | (i -' 1)) . n) by A13, PARTFUN1:def 6

          .= ((((x | (i -' 1)) ^ <*xi*>) ^ (x /^ i)) . n) by A4, A15, A14, FINSEQ_3: 112, XXREAL_0: 2

          .= (((x | (i -' 1)) ^ ( <*xi*> ^ (x /^ i))) . n) by FINSEQ_1: 32

          .= ((x | (i -' 1)) . n) by A16, FINSEQ_1: 64

          .= ((x | (i -' 1)) /. n) by A13, A11, PARTFUN1:def 6;

          hence thesis;

        end;



         A17: ( len (y /^ i)) = (( len y) -' i) & ( len (x /^ i)) = (( len x) -' i) by RFINSEQ: 29;

        for n be Nat st 1 <= n & n <= ( len (y /^ i)) holds ((y /^ i) . n) = ((x /^ i) . n)

        proof

          let n be Nat;

          assume

           A18: 1 <= n & n <= ( len (y /^ i));

          then

           A19: n in ( dom (y /^ i)) & n in ( dom (x /^ i)) by A17, A3, FINSEQ_3: 25;



           A20: ( len (x | (i -' 1))) = (i -' 1) by A1, A3, FINSEQ_1: 59, NAT_D: 44;



           A21: ( len <*xi*>) = 1 by FINSEQ_1: 39;

          (i - 1) >= 0 by A1, XREAL_1: 48;

          then (i -' 1) = (i - 1) by XREAL_0:def 2;



          then

           A22: ( len ((x | (i -' 1)) ^ <*xi*>)) = ((i - 1) + 1) by A20, A21, FINSEQ_1: 22

          .= i;

          ((y /^ i) . n) = (y . (i + n)) by A19, FINSEQ_7: 4

          .= ((x /^ i) . n) by A18, A4, A22, FINSEQ_1: 65;

          hence thesis;

        end;

        then (y /^ i) = (x /^ i) by A17, A3;

        hence thesis by A8, A9, A11, A12, FINSEQ_5: 12;

      end;

      hence thesis by A5, FUNCT_1: 2;

    end;

    theorem :: PDIFF_7:41



     Th41: for m be non zero Nat, f be PartFunc of ( REAL m), REAL , g be PartFunc of REAL , REAL , x,y be Element of ( REAL m), i be Nat, xi be Real st 1 <= i & i <= m & y = (( reproj (i,x)) . xi) & g = (f * ( reproj (i,x))) holds ( diff (g,xi)) = ( partdiff (f,y,i))

    proof

      let m be non zero Nat, f be PartFunc of ( REAL m), REAL , g be PartFunc of REAL , REAL , x,y be Element of ( REAL m), i be Nat, xi be Real;

      assume

       A1: 1 <= i & i <= m & y = (( reproj (i,x)) . xi) & g = (f * ( reproj (i,x)));

      then ( reproj (i,x)) = ( reproj (i,y)) & (( proj (i,m)) . y) = xi by Th39, Th40;

      hence ( partdiff (f,y,i)) = ( diff (g,xi)) by A1;

    end;

    theorem :: PDIFF_7:42



     Th42: for m be non zero Nat, f be PartFunc of ( REAL m), REAL , p,q be Real, x be Element of ( REAL m), i be Nat st 1 <= i & i <= m & p < q & (for h be Real st h in [.p, q.] holds (( reproj (i,x)) . h) in ( dom f)) & (for h be Element of REAL st h in [.p, q.] holds f is_partial_differentiable_in ((( reproj (i,x)) . h),i)) holds ex r be Real, y be Element of ( REAL m) st r in ].p, q.[ & y = (( reproj (i,x)) . r) & ((f /. (( reproj (i,x)) . q)) - (f /. (( reproj (i,x)) . p))) = ((q - p) * ( partdiff (f,y,i)))

    proof

      let m be non zero Nat, f be PartFunc of ( REAL m), REAL , p,q be Real, x be Element of ( REAL m), i be Nat;

      assume

       A1: 1 <= i & i <= m & p < q & (for h be Real st h in [.p, q.] holds (( reproj (i,x)) . h) in ( dom f)) & (for h be Element of REAL st h in [.p, q.] holds f is_partial_differentiable_in ((( reproj (i,x)) . h),i));

      set g = (f * ( reproj (i,x)));

      now

        let h be object;

        assume

         A2: h in [.p, q.];

        then

        reconsider h1 = h as Element of REAL ;



         A3: ( dom ( reproj (i,x))) = REAL by PDIFF_1:def 5;

        (( reproj (i,x)) . h1) in ( dom f) by A1, A2;

        hence h in ( dom g) by A3, FUNCT_1: 11;

      end;

      then

       A4: [.p, q.] c= ( dom g);

       A5:

      now

        let x0 be Real;

        assume

         A6: x0 in [.p, q.];

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

        set y = (( reproj (i,x)) . xx);



         A7: (( proj (i,m)) . y) = x0 by Th39, A1;

        f is_partial_differentiable_in (y,i) by A1, A6;

        then (f * ( reproj (i,y))) is_differentiable_in x0 by A7;

        hence g is_differentiable_in x0 by Th40, A1;

      end;

      now

        let z be object;

        assume z in ].p, q.[;

        then ex z1 be Real st z = z1 & p < z1 & z1 < q;

        hence z in [.p, q.];

      end;

      then

       A8: ].p, q.[ c= [.p, q.];

      then

       A9: ].p, q.[ c= ( dom g) by A4;

      for x be Real st x in ].p, q.[ holds g is_differentiable_in x by A5, A8;

      then

       A10: g is_differentiable_on ].p, q.[ by A9, FDIFF_1: 9;

      now

        let x0,r be Real;

        assume

         A11: x0 in [.p, q.] & 0 < r;

        then g is_continuous_in x0 by A5, FDIFF_1: 24;

        then

        consider s be Real such that

         A12: 0 < s & for x1 be Real st x1 in ( dom g) & |.(x1 - x0).| < s holds |.((g . x1) - (g . x0)).| < r by A11, FCONT_1: 3;

        take s;

        thus 0 < s by A12;

        thus for x1 be Real st x1 in [.p, q.] & |.(x1 - x0).| < s holds |.((g . x1) - (g . x0)).| < r by A4, A12;

      end;

      then (g | [.p, q.]) is continuous by A4, FCONT_1: 14;

      then

      consider r be Real such that

       A13: r in ].p, q.[ & ( diff (g,r)) = (((g . q) - (g . p)) / (q - p)) by A1, A4, A10, ROLLE: 3;

      (q - p) <> 0 by A1;

      then

       A14: (( diff (g,r)) * (q - p)) = ((g . q) - (g . p)) by A13, XCMPLX_1: 87;



       A15: p in { s where s be Real : p <= s & s <= q } by A1;



      then

       A16: (f /. (( reproj (i,x)) . p)) = (f . (( reproj (i,x)) . p)) by A1, PARTFUN1:def 6

      .= (g . p) by A4, A15, FUNCT_1: 12;



       A17: q in { s where s be Real : p <= s & s <= q } by A1;



      then

       A18: (f /. (( reproj (i,x)) . q)) = (f . (( reproj (i,x)) . q)) by A1, PARTFUN1:def 6

      .= (g . q) by A4, A17, FUNCT_1: 12;

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

      set y = (( reproj (i,x)) . r);

      ( diff (g,r)) = ( partdiff (f,y,i)) by A1, Th41;

      hence thesis by A13, A14, A16, A18;

    end;

    theorem :: PDIFF_7:43



     Th43: for m be non zero Nat, f be PartFunc of ( REAL m), REAL , p,q be Real, x be Element of ( REAL m), i be Nat st 1 <= i & i <= m & p <= q & (for h be Real st h in [.p, q.] holds (( reproj (i,x)) . h) in ( dom f)) & (for h be Element of REAL st h in [.p, q.] holds f is_partial_differentiable_in ((( reproj (i,x)) . h),i)) holds ex r be Real, y be Element of ( REAL m) st r in [.p, q.] & y = (( reproj (i,x)) . r) & ((f /. (( reproj (i,x)) . q)) - (f /. (( reproj (i,x)) . p))) = ((q - p) * ( partdiff (f,y,i)))

    proof

      let m be non zero Nat, f be PartFunc of ( REAL m), REAL , p,q be Real, x be Element of ( REAL m), i be Nat;

      assume

       A1: 1 <= i & i <= m & p <= q & (for h be Real st h in [.p, q.] holds (( reproj (i,x)) . h) in ( dom f)) & (for h be Element of REAL st h in [.p, q.] holds f is_partial_differentiable_in ((( reproj (i,x)) . h),i));

      per cases ;

        suppose

         A2: p = q;

        then

         A3: p in [.p, q.];

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

        reconsider y = (( reproj (i,x)) . p) as Element of ( REAL m);

        ((q - p) * ( partdiff (f,y,i))) = 0 by A2;

        hence thesis by A3, A2;

      end;

        suppose p <> q;

        then p < q by A1, XXREAL_0: 1;

        then

         A4: ex r be Real, y be Element of ( REAL m) st r in ].p, q.[ & y = (( reproj (i,x)) . r) & ((f /. (( reproj (i,x)) . q)) - (f /. (( reproj (i,x)) . p))) = ((q - p) * ( partdiff (f,y,i))) by Th42, A1;

         ].p, q.[ c= [.p, q.] by XXREAL_1: 25;

        hence thesis by A4;

      end;

    end;

    theorem :: PDIFF_7:44



     Th44: for m be non zero Nat, x,y,z,w be Element of ( REAL m), i be Nat, d,p,q,r be Real st 1 <= i & i <= m & |.(y - x).| < d & |.(z - x).| < d & p = (( proj (i,m)) . y) & z = (( reproj (i,y)) . q) & r in [.p, q.] & w = (( reproj (i,y)) . r) holds |.(w - x).| < d

    proof

      let m be non zero Nat, x,y,z,w be Element of ( REAL m), i be Nat, d,p,q,r be Real;

      assume that

       A1: 1 <= i & i <= m and

       A2: |.(y - x).| < d & |.(z - x).| < d and

       A3: p = (( proj (i,m)) . y) & z = (( reproj (i,y)) . q) and

       A4: r in [.p, q.] and

       A5: w = (( reproj (i,y)) . r);

      set wx = (w - x);

      set yx = (y - x);

      set zx = (z - x);



       A6: ( Sum ( sqr yx)) = ( |.yx.| ^2 ) & ( Sum ( sqr wx)) = ( |.wx.| ^2 ) & ( Sum ( sqr zx)) = ( |.zx.| ^2 ) by TOPREAL9: 5;



       A7: (( proj (i,m)) . z) = q & (( proj (i,m)) . w) = r by A1, A3, A5, Th39;



       A8: p <= r & r <= q by A4, XXREAL_1: 1;

      i in ( Seg m) by A1;

      then

       A9: i in ( dom yx) & i in ( dom wx) & i in ( dom zx) by FINSEQ_1: 89;

      set x1 = x;

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



       A10: for l be Nat st l in ( Seg m) & l <> i holds (( sqr yx) . l) = (( sqr wx) . l)

      proof

        let l be Nat;

        assume

         A11: l in ( Seg m) & l <> i;

        then

         A12: l in ( dom yx) & l in ( dom wx) & l in ( dom y) by FINSEQ_1: 89;

        then

         A13: l in ( Seg ( len y)) by FINSEQ_1:def 3;

        then

         A14: 1 <= l & l <= ( len y) by FINSEQ_1: 1;

        l in ( Seg ( len y)) & l in ( Seg ( len ( Replace (y,i,r)))) by A13, FINSEQ_7: 5;

        then

         A15: l in ( dom y) & l in ( dom ( Replace (y,i,r))) by FINSEQ_1:def 3;

        ( sqr yx) = ( sqrreal * yx) & ( sqr wx) = ( sqrreal * wx) by RVSUM_1:def 8;

        then (( sqr yx) . l) = ( sqrreal . (yx . l)) & (( sqr wx) . l) = ( sqrreal . (wx . l)) by A12, FUNCT_1: 13;

        then (( sqr yx) . l) = ((yx . l) ^2 ) & (( sqr wx) . l) = ((wx . l) ^2 ) by RVSUM_1:def 2;

        then

         A16: (( sqr yx) . l) = (((y . l) - (x1 . l)) ^2 ) & (( sqr wx) . l) = (((w . l) - (x1 . l)) ^2 ) by A12, VALUED_1: 13;

        (w . l) = (( Replace (y,i,r)) . l) by A5, PDIFF_1:def 5;

        then (w . l) = (( Replace (y,i,r)) /. l) by A15, PARTFUN1:def 6;

        then (w . l) = (y /. l) by A11, A14, FINSEQ_7: 10;

        hence thesis by A15, A16, PARTFUN1:def 6;

      end;



       A17: for l be Nat st l in ( Seg m) & l <> i holds (( sqr zx) . l) = (( sqr wx) . l)

      proof

        let l be Nat;

        assume

         A18: l in ( Seg m) & l <> i;

        then

         A19: l in ( dom zx) & l in ( dom wx) & l in ( dom z) by FINSEQ_1: 89;

        then

         A20: l in ( Seg ( len z)) by FINSEQ_1:def 3;

        then

         A21: 1 <= l & l <= ( len z) by FINSEQ_1: 1;

        l in ( Seg ( len z)) & l in ( Seg ( len ( Replace (z,i,r)))) by A20, FINSEQ_7: 5;

        then

         A22: l in ( dom z) & l in ( dom ( Replace (z,i,r))) by FINSEQ_1:def 3;

        ( sqr zx) = ( sqrreal * zx) & ( sqr wx) = ( sqrreal * wx) by RVSUM_1:def 8;

        then (( sqr zx) . l) = ( sqrreal . (zx . l)) & (( sqr wx) . l) = ( sqrreal . (wx . l)) by A19, FUNCT_1: 13;

        then (( sqr zx) . l) = ((zx . l) ^2 ) & (( sqr wx) . l) = ((wx . l) ^2 ) by RVSUM_1:def 2;

        then

         A23: (( sqr zx) . l) = (((z . l) - (x1 . l)) ^2 ) & (( sqr wx) . l) = (((w . l) - (x1 . l)) ^2 ) by A19, VALUED_1: 13;

        (w . l) = ((( reproj (i,z)) . r) . l) by A1, A3, Th40, A5;

        then (w . l) = (( Replace (z,i,r)) . l) by PDIFF_1:def 5;

        then (w . l) = (( Replace (z,i,r)) /. l) by A22, PARTFUN1:def 6;

        then (w . l) = (z /. l) by A18, A21, FINSEQ_7: 10;

        hence thesis by A22, A23, PARTFUN1:def 6;

      end;

       A24:

      now

        assume

         A25: |.(w - x).| > |.(y - x).| & |.(w - x).| > |.(z - x).|;

         A26:

        now

          assume

           A27: (( sqr wx) . i) <= (( sqr yx) . i);



           A28: ( len ( sqr wx)) = m by CARD_1:def 7

          .= ( len ( sqr yx)) by CARD_1:def 7;

          for l be Element of NAT st l in ( dom ( sqr wx)) holds (( sqr wx) . l) <= (( sqr yx) . l)

          proof

            let l be Element of NAT ;

            assume l in ( dom ( sqr wx));

            then

             A29: l in ( Seg m) by FINSEQ_1: 89;

            per cases ;

              suppose l = i;

              hence (( sqr wx) . l) <= (( sqr yx) . l) by A27;

            end;

              suppose l <> i;

              hence (( sqr wx) . l) <= (( sqr yx) . l) by A29, A10;

            end;

          end;

          hence contradiction by A28, A6, A25, INTEGRA5: 3, SQUARE_1: 16;

        end;

         A30:

        now

          assume

           A31: (( sqr wx) . i) <= (( sqr zx) . i);



           A32: ( len ( sqr wx)) = m by CARD_1:def 7

          .= ( len ( sqr zx)) by CARD_1:def 7;

          for l be Element of NAT st l in ( dom ( sqr wx)) holds (( sqr wx) . l) <= (( sqr zx) . l)

          proof

            let l be Element of NAT ;

            assume l in ( dom ( sqr wx));

            then

             A33: l in ( Seg m) by FINSEQ_1: 89;

            per cases ;

              suppose l = i;

              hence (( sqr wx) . l) <= (( sqr zx) . l) by A31;

            end;

              suppose l <> i;

              hence (( sqr wx) . l) <= (( sqr zx) . l) by A33, A17;

            end;

          end;

          hence contradiction by A32, A6, A25, INTEGRA5: 3, SQUARE_1: 16;

        end;

        ( sqr yx) = ( sqrreal * yx) & ( sqr wx) = ( sqrreal * wx) & ( sqr zx) = ( sqrreal * zx) by RVSUM_1:def 8;

        then (( sqr yx) . i) = ( sqrreal . (yx . i)) & (( sqr wx) . i) = ( sqrreal . (wx . i)) & (( sqr zx) . i) = ( sqrreal . (zx . i)) by A9, FUNCT_1: 13;

        then

         A34: (( sqr yx) . i) = ((yx . i) ^2 ) & (( sqr wx) . i) = ((wx . i) ^2 ) & (( sqr zx) . i) = ((zx . i) ^2 ) by RVSUM_1:def 2;

        (y . i) = p & (w . i) = r & (z . i) = q by A3, A7, PDIFF_1:def 1;

        then

         A35: (( sqr yx) . i) = ((p - (x1 . i)) ^2 ) & (( sqr wx) . i) = ((r - (x1 . i)) ^2 ) & (( sqr zx) . i) = ((q - (x1 . i)) ^2 ) by A34, A9, VALUED_1: 13;



         A36: p <= q by A8, XXREAL_0: 2;

        per cases ;

          suppose (x1 . i) < p;

          then (x1 . i) < r & (x1 . i) < q by A8, A36, XXREAL_0: 2;

          then (q - (x1 . i)) > 0 & (r - (x1 . i)) > 0 by XREAL_1: 50;

          then (q - (x1 . i)) < (r - (x1 . i)) by A35, A30, SQUARE_1: 15;

          hence contradiction by A8, XREAL_1: 13;

        end;

          suppose

           A37: p <= (x1 . i) & (x1 . i) <= r;

          then (x1 . i) <= q by A8, XXREAL_0: 2;

          then (r - (x1 . i)) >= 0 & (q - (x1 . i)) >= 0 by A37, XREAL_1: 48;

          then (q - (x1 . i)) < (r - (x1 . i)) by A35, A30, SQUARE_1: 15;

          hence contradiction by A8, XREAL_1: 13;

        end;

          suppose

           A38: r < (x1 . i) & (x1 . i) <= q;

          then p < (x1 . i) by A8, XXREAL_0: 2;

          then

           A39: ((x1 . i) - p) >= 0 & ((x1 . i) - r) >= 0 by A38, XREAL_1: 48;

          ((p - (x1 . i)) ^2 ) = (((x1 . i) - p) ^2 ) & ((r - (x1 . i)) ^2 ) = (((x1 . i) - r) ^2 );

          then ((x1 . i) - p) < ((x1 . i) - r) by A35, A26, A39, SQUARE_1: 15;

          hence contradiction by A8, XREAL_1: 13;

        end;

          suppose q < (x1 . i);

          then r < (x1 . i) by A8, XXREAL_0: 2;

          then p < (x1 . i) & r < (x1 . i) by A8, XXREAL_0: 2;

          then

           A40: ((x1 . i) - r) >= 0 & ((x1 . i) - p) >= 0 by XREAL_1: 48;

          ((p - (x1 . i)) ^2 ) = (((x1 . i) - p) ^2 ) & ((r - (x1 . i)) ^2 ) = (((x1 . i) - r) ^2 );

          then ((x1 . i) - p) < ((x1 . i) - r) by A35, A26, A40, SQUARE_1: 15;

          hence contradiction by A8, XREAL_1: 13;

        end;

      end;

      per cases by A24;

        suppose |.(w - x).| <= |.(y - x).|;

        hence |.(w - x).| < d by A2, XXREAL_0: 2;

      end;

        suppose |.(w - x).| <= |.(z - x).|;

        hence |.(w - x).| < d by A2, XXREAL_0: 2;

      end;

    end;

    theorem :: PDIFF_7:45



     Th45: for m be non zero Nat, f be PartFunc of ( REAL m), REAL , X be Subset of ( REAL m), x,y,z be Element of ( REAL m), i be Nat, d,p,q be Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= ( dom f) & (for x be Element of ( REAL m) st x in X holds f is_partial_differentiable_in (x,i)) & 0 < d & (for z be Element of ( REAL m) st |.(z - x).| < d holds z in X) & z = (( reproj (i,y)) . p) & q = (( proj (i,m)) . y) holds ex w be Element of ( REAL m) st |.(w - x).| < d & f is_partial_differentiable_in (w,i) & ((f /. z) - (f /. y)) = ((p - q) * ( partdiff (f,w,i)))

    proof

      let m be non zero Nat, f be PartFunc of ( REAL m), REAL , X be Subset of ( REAL m), x,y,z be Element of ( REAL m), i be Nat, d,p,q be Real;

      assume

       A1: 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= ( dom f) & (for x be Element of ( REAL m) st x in X holds f is_partial_differentiable_in (x,i)) & 0 < d & (for z be Element of ( REAL m) st |.(z - x).| < d holds z in X) & z = (( reproj (i,y)) . p) & q = (( proj (i,m)) . y);

      then

       A2: p = (( proj (i,m)) . z) by Th39;

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

      (( reproj (i,y)) . q) = (( reproj (i,y)) . (y . i)) by A1, PDIFF_1:def 1;

      then (( reproj (i,y)) . q) = ( Replace (y,i,yi)) by PDIFF_1:def 5;

      then

       A3: y = (( reproj (i,y)) . q) by FUNCT_7: 35;

      per cases ;

        suppose

         A4: q <= p;



         A5: for h be Element of REAL st h in [.q, p.] holds (( reproj (i,y)) . h) in X

        proof

          let h be Element of REAL ;

          assume h in [.q, p.];

          then |.((( reproj (i,y)) . h) - x).| < d by A1, Th44;

          hence (( reproj (i,y)) . h) in X by A1;

        end;

        then

         A6: for h be Real st h in [.q, p.] holds (( reproj (i,y)) . h) in ( dom f) by A1;

        reconsider p, q as Real;

        for h be Element of REAL st h in [.q, p.] holds f is_partial_differentiable_in ((( reproj (i,y)) . h),i) by A1, A5;

        then

        consider r be Real, w be Element of ( REAL m) such that

         A7: r in [.q, p.] & w = (( reproj (i,y)) . r) & ((f /. (( reproj (i,y)) . p)) - (f /. (( reproj (i,y)) . q))) = ((p - q) * ( partdiff (f,w,i))) by Th43, A1, A4, A6;



         A8: |.(w - x).| < d by A7, A1, Th44;

        then f is_partial_differentiable_in (w,i) by A1;

        hence thesis by A7, A3, A1, A8;

      end;

        suppose

         A9: p < q;

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

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;



         A10: ( dom y) = ( Seg m) by FINSEQ_1: 89;

        then

         A11: i in ( dom y) & ( len y) = mm by A1, FINSEQ_1:def 3;

        then ( len ( Replace (y,i,p))) = m by FINSEQ_7: 5;

        then

         A12: ( dom y) = ( dom ( Replace (y,i,p))) by A10, FINSEQ_1:def 3;

        z = ( Replace (y,i,p)) by A1, PDIFF_1:def 5;

        then (z . i) = (( Replace (y,i,p)) /. i) by A11, A12, PARTFUN1:def 6;

        then

         A13: (z . i) = p by A1, A11, FINSEQ_7: 8;



         A14: y = (( reproj (i,z)) . q) by A1, Th40, A3;



         A15: for h be Element of REAL st h in [.p, q.] holds (( reproj (i,z)) . h) in X

        proof

          let h be Element of REAL ;

          assume h in [.p, q.];

          then |.((( reproj (i,z)) . h) - x).| < d by A2, A14, A1, Th44;

          then (( reproj (i,z)) . h) in X by A1;

          hence thesis;

        end;



         A16: for h be Real st h in [.p, q.] holds (( reproj (i,z)) . h) in ( dom f) by A15, A1;

        for h be Element of REAL st h in [.p, q.] holds f is_partial_differentiable_in ((( reproj (i,z)) . h),i) by A15, A1;

        then

        consider r be Real, w be Element of ( REAL m) such that

         A17: r in [.p, q.] & w = (( reproj (i,z)) . r) & ((f /. (( reproj (i,z)) . q)) - (f /. (( reproj (i,z)) . p))) = ((q - p) * ( partdiff (f,w,i))) by Th43, A1, A9, A16;



         A18: |.(w - x).| < d by A2, A14, A17, A1, Th44;

        then

         A19: f is_partial_differentiable_in (w,i) by A1;

        reconsider zi = (z . i) as Real;

        (( reproj (i,z)) . p) = ( Replace (z,i,zi)) by A13, PDIFF_1:def 5;

        then ((f /. y) - (f /. z)) = ((q - p) * ( partdiff (f,w,i))) by A14, A17, FUNCT_7: 35;

        then ((f /. z) - (f /. y)) = ((p - q) * ( partdiff (f,w,i)));

        hence thesis by A18, A19;

      end;

    end;

    theorem :: PDIFF_7:46



     Th46: for m be non zero Nat, h be FinSequence of ( REAL m), y,x be Element of ( REAL m), j be Nat st ( len h) = (m + 1) & 1 <= j & j <= m & (for i be Nat st i in ( dom h) holds (h /. i) = ((y | ((m + 1) -' i)) ^ ( 0* (i -' 1)))) holds (x + (h /. j)) = (( reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . (( proj (((m + 1) -' j),m)) . (x + y)))

    proof

      let m be non zero Nat, h be FinSequence of ( REAL m), y,x be Element of ( REAL m), j be Nat such that

       A1: ( len h) = (m + 1) & 1 <= j & j <= m & (for i be Nat st i in ( dom h) holds (h /. i) = ((y | ((m + 1) -' i)) ^ ( 0* (i -' 1))));

      reconsider mj = (m - j) as Nat by A1, NAT_1: 21;

      reconsider xxx = ((x /. ((m + 1) -' j)) + (y /. ((m + 1) -' j))) as Element of REAL ;

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

      then

       A2: ( Seg m) c= ( Seg (m + 1)) by FINSEQ_1: 5;



       A3: j in ( Seg m) by A1;

      then j in ( Seg (m + 1)) by A2;

      then j in ( dom h) by A1, FINSEQ_1:def 3;

      then

       A4: (h /. j) = ((y | ((m + 1) -' j)) ^ ( 0* (j -' 1))) by A1;

      (j + 1) in ( Seg (m + 1)) by A3, FINSEQ_1: 60;

      then (j + 1) in ( dom h) by A1, FINSEQ_1:def 3;

      then

       A5: (h /. (j + 1)) = ((y | ((m + 1) -' (j + 1))) ^ ( 0* ((j + 1) -' 1))) by A1;

      ((m + 1) -' j) = ((m -' j) + 1) by A1, NAT_D: 38;

      then

       A6: 1 <= ((m + 1) -' j) by NAT_1: 11;



       A7: (1 - j) <= 0 by A1, XREAL_1: 47;

      ((m + 1) -' j) = ((m + 1) - j) by A1, NAT_D: 37

      .= (m + (1 - j));

      then

       A8: ((m + 1) -' j) <= m by A7, XREAL_1: 32;

      then ((m + 1) -' j) in ( Seg m) by A6;

      then

       A9: ((m + 1) -' j) in ( dom (x + y)) & ((m + 1) -' j) in ( dom y) & ((m + 1) -' j) in ( dom x) by FINSEQ_1: 89;

      ((m + 1) -' j) <= ( len y) by A8, CARD_1:def 7;

      then

       A10: ( len (y | ((m + 1) -' j))) = ((m + 1) -' j) by FINSEQ_1: 59;

      (j + 1) <= (m + 1) by A1, XREAL_1: 6;

      then

       A11: ((m + 1) -' (j + 1)) = ((m + 1) - (j + 1)) by XREAL_1: 233;

      then ((m + 1) -' (j + 1)) = (m - j) & j >= 0 ;

      then ((m + 1) -' (j + 1)) <= m by XREAL_1: 43;

      then ((m + 1) -' (j + 1)) <= ( len y) by CARD_1:def 7;

      then

       A12: ( len (y | ((m + 1) -' (j + 1)))) = ((m + 1) -' (j + 1)) by FINSEQ_1: 59;

      (( proj (((m + 1) -' j),m)) . (x + y)) = ((x + y) . ((m + 1) -' j)) by PDIFF_1:def 1

      .= ((x . ((m + 1) -' j)) + (y . ((m + 1) -' j))) by A9, VALUED_1:def 1

      .= ((x . ((m + 1) -' j)) + (y /. ((m + 1) -' j))) by A9, PARTFUN1:def 6

      .= ((x /. ((m + 1) -' j)) + (y /. ((m + 1) -' j))) by A9, PARTFUN1:def 6;

      then

       A13: (( reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . (( proj (((m + 1) -' j),m)) . (x + y))) = ( Replace ((x + (h /. (j + 1))),((m + 1) -' j),xxx)) by PDIFF_1:def 5;

      (( reproj (((m + 1) -' j),(x + (h /. (j + 1))))) /. (( proj (((m + 1) -' j),m)) . (x + y))) is Element of ( REAL m);

      then

      reconsider rep = (( reproj (((m + 1) -' j),(x + (h /. (j + 1))))) /. (( proj (((m + 1) -' j),m)) . (x + y))) as FinSequence of REAL ;

      reconsider hj = (h /. j) as Element of ( REAL m);

      reconsider hj1 = (h /. (j + 1)) as Element of ( REAL m);



       A14: ( len (x + hj)) = m by CARD_1:def 7

      .= ( len rep) by CARD_1:def 7;

      now

        let n be Nat;

        assume

         A15: 1 <= n & n <= ( len rep);

        then

         A16: 1 <= n & n <= m by CARD_1:def 7;

        then n in ( Seg m);

        then

         A17: n in ( Seg ( len (x + (h /. j)))) & n in ( Seg ( len (x + (h /. (j + 1))))) & n in ( Seg ( len x)) & n in ( Seg ( len y)) by CARD_1:def 7;

        then

         A18: n in ( dom (x + (h /. j))) & n in ( dom (x + (h /. (j + 1)))) & n in ( dom rep) & n in ( dom x) & n in ( dom y) by A14, FINSEQ_1:def 3;

        then

         A19: ((x + (h /. j)) . n) = ((x . n) + (hj . n)) & ((x + (h /. (j + 1))) . n) = ((x . n) + (hj1 . n)) by VALUED_1:def 1;

        per cases by XXREAL_0: 1;

          suppose

           A20: n < ((m + 1) -' j);

          then

           A21: n in ( Seg ((m + 1) -' j)) by A15;



           A22: (hj . n) = ((y | ( Seg ((m + 1) -' j))) . n) by A4, A10, A15, A20, FINSEQ_1: 64

          .= (y . n) by A21, FUNCT_1: 49;

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

          then n < ((m + 1) - j) by A1, A20, XREAL_1: 233, XXREAL_0: 2;

          then n < (mj + 1);

          then

           A23: n <= mj by NAT_1: 13;

          then

           A24: n in ( Seg mj) by A15;



           A25: (hj1 . n) = ((y | ( Seg mj)) . n) by A11, A23, A12, A5, A15, FINSEQ_1: 64

          .= (y . n) by A24, FUNCT_1: 49;

          n <> ((m + 1) -' j) & n <= ( len (x + (h /. (j + 1)))) by A20, A17, FINSEQ_1: 1;

          then (rep /. n) = ((x + (h /. (j + 1))) /. n) by A13, A15, FINSEQ_7: 10;



          then (rep . n) = ((x + (h /. (j + 1))) /. n) by A18, PARTFUN1:def 6

          .= ((x + (h /. (j + 1))) . n) by A18, PARTFUN1:def 6;

          hence ((x + (h /. j)) . n) = (rep . n) by A19, A25, A22;

        end;

          suppose

           A26: n = ((m + 1) -' j);

          then

           A27: n in ( Seg ((m + 1) -' j)) by A15;



           A28: (hj . n) = ((y | ( Seg ((m + 1) -' j))) . n) by A4, A10, A15, A26, FINSEQ_1: 64

          .= (y . n) by A27, FUNCT_1: 49;

          n <= ( len (x + (h /. (j + 1)))) by A17, FINSEQ_1: 1;

          then (rep /. n) = ((x /. n) + (y /. n)) by A26, A13, A15, FINSEQ_7: 8;

          then

           A29: (rep . n) = ((x /. n) + (y /. n)) by A18, PARTFUN1:def 6;



          thus ((x + (h /. j)) . n) = ((x /. n) + (y . n)) by A18, A19, A28, PARTFUN1:def 6

          .= (rep . n) by A29, A18, PARTFUN1:def 6;

        end;

          suppose

           A30: n > ((m + 1) -' j);

          then

          reconsider nm = (n - ((m + 1) -' j)) as Nat by NAT_1: 21;



           A31: m <= (m + 1) by NAT_1: 11;

          n <= ( len hj) by A16, CARD_1:def 7;



          then

           A32: (hj . n) = (( 0* (j -' 1)) . nm) by A4, A10, A30, FINSEQ_1: 24

          .= 0 ;



           A33: ( len y) = m by CARD_1:def 7;

          (j + 1) <= (m + 1) by A1, XREAL_1: 6;



          then ((m + 1) -' (j + 1)) = ((m + 1) - (j + 1)) by XREAL_1: 233

          .= (m - j)

          .= (m -' j) by A1, XREAL_1: 233;

          then

           A34: ( len (y | ((m + 1) -' (j + 1)))) = (m -' j) by A33, FINSEQ_1: 59, NAT_D: 35;

          n > ((m + 1) - j) by A30, A31, A1, XREAL_1: 233, XXREAL_0: 2;

          then n > ((m - j) + 1) & ((m - j) + 1) > ((m - j) + 0 qua Real) by XREAL_1: 8;

          then n > (m - j) by XXREAL_0: 2;

          then

           A35: n > (m -' j) by A1, XREAL_1: 233;

          then

          reconsider nmj = (n - (m -' j)) as Nat by NAT_1: 21;

          n <= ( len hj1) by A16, CARD_1:def 7;



          then

           A36: (hj1 . n) = (( 0* ((j + 1) -' 1)) . (n - (m -' j))) by A5, A34, A35, FINSEQ_1: 24

          .= 0 ;

          n <> ((m + 1) -' j) & n <= ( len (x + (h /. (j + 1)))) by A30, A17, FINSEQ_1: 1;

          then (rep /. n) = ((x + (h /. (j + 1))) /. n) by A13, A15, FINSEQ_7: 10;



          then (rep . n) = ((x + (h /. (j + 1))) /. n) by A18, PARTFUN1:def 6

          .= ((x + (h /. (j + 1))) . n) by A18, PARTFUN1:def 6;

          hence ((x + (h /. j)) . n) = (rep . n) by A19, A36, A32;

        end;

      end;

      hence (x + (h /. j)) = (( reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . (( proj (((m + 1) -' j),m)) . (x + y))) by A14;

    end;

    theorem :: PDIFF_7:47



     Th47: for m be non zero Nat, f be PartFunc of ( REAL m), ( REAL 1), X be Subset of ( REAL m), x be Element of ( REAL m) st X is open & x in X & (for i be Nat st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X) holds f is_differentiable_in x & for h be Element of ( REAL m) holds ex w be FinSequence of ( REAL 1) st ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . h) * ( partdiff (f,x,i)))) & (( diff (f,x)) . h) = ( Sum w)

    proof

      let m be non zero Nat, f be PartFunc of ( REAL m), ( REAL 1), X be Subset of ( REAL m), x be Element of ( REAL m);

      assume

       A1: X is open & x in X & for i be Nat st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X;

      consider L be Lipschitzian LinearOperator of m, 1 such that

       A2: for h be Element of ( REAL m) holds ex w be FinSequence of ( REAL 1) st ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . h) * ( partdiff (f,x,i)))) & (L . h) = ( Sum w) by Lm8;

      consider d0 be Real such that

       A3: d0 > 0 and

       A4: { y where y be Element of ( REAL m) : |.(y - x).| < d0 } c= X by A1, Th31;

      set N = { y where y be Element of ( REAL m) : |.(y - x).| < d0 };

      1 <= m by NAT_1: 14;

      then f is_partial_differentiable_on (X,m) by A1;

      then X c= ( dom f);

      then

       A5: N c= ( dom f) by A4;

      deffunc RF( Element of ( REAL m)) = (((f /. (x + $1)) - (f /. x)) - (L . $1));

      consider R be Function of ( REAL m), ( REAL 1) such that

       A6: for h be Element of ( REAL m) holds (R . h) = RF(h) from FUNCT_2:sch 4;

      consider f0 be PartFunc of ( REAL m), REAL such that

       A7: f = ( <>* f0) by Th29;

       A8:

      now

        let r0 be Real;

        assume

         A9: r0 > 0 ;

        set r1 = (r0 / 2);

        set r = (r1 / m);

        defpred DSQ[ Nat, Real] means ex k be Nat st $1 = k & 0 < $2 & for q be Element of ( REAL m) st q in X & |.(q - x).| < $2 holds |.(( partdiff (f,q,k)) - ( partdiff (f,x,k))).| < r;



         A10: for k0 be Nat st k0 in ( Seg m) holds ex d be Element of REAL st DSQ[k0, d]

        proof

          let k0 be Nat;

          assume

           A11: k0 in ( Seg m);

          reconsider k = k0 as Nat;



           A12: 1 <= k & k <= m by A11, FINSEQ_1: 1;

          then (f `partial| (X,k)) is_continuous_on X by A1;

          then

          consider d be Real such that

           A13: 0 < d & for q be Element of ( REAL m) st q in X & |.(q - x).| < d holds |.(((f `partial| (X,k)) /. q) - ((f `partial| (X,k)) /. x)).| < r by A9, A1, Th38;

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

          take d;

          for q be Element of ( REAL m) st q in X & |.(q - x).| < d holds |.(( partdiff (f,q,k)) - ( partdiff (f,x,k))).| < r

          proof

            let q be Element of ( REAL m);

            assume

             A14: q in X & |.(q - x).| < d;

            then

             A15: |.(((f `partial| (X,k)) /. q) - ((f `partial| (X,k)) /. x)).| < r by A13;



             A16: f is_partial_differentiable_on (X,k) by A1, A12;

            then ((f `partial| (X,k)) /. q) = ( partdiff (f,q,k)) by A14, Def5;

            hence |.(( partdiff (f,q,k)) - ( partdiff (f,x,k))).| < r by A15, A16, A1, Def5;

          end;

          hence ex k be Nat st k0 = k & 0 < d & for q be Element of ( REAL m) st q in X & |.(q - x).| < d holds |.(( partdiff (f,q,k)) - ( partdiff (f,x,k))).| < r by A13;

        end;

        consider Dseq be FinSequence of REAL such that

         A17: ( dom Dseq) = ( Seg m) & for i be Nat st i in ( Seg m) holds DSQ[i, (Dseq . i)] from FINSEQ_1:sch 5( A10);



         A18: ( rng Dseq) is finite by A17, FINSET_1: 8;

        m in ( Seg m) by FINSEQ_1: 3;

        then

        reconsider rDseq = ( rng Dseq) as non empty ext-real-membered set by A17, FUNCT_1: 3;

        reconsider rDseq as left_end right_end non empty ext-real-membered set by A18;



         A19: ( min rDseq) in ( rng Dseq) by XXREAL_2:def 7;

        reconsider d1 = ( min rDseq) as Real;

        set d = ( min (d0,d1));

        consider i1 be object such that

         A20: i1 in ( dom Dseq) & d1 = (Dseq . i1) by A19, FUNCT_1:def 3;

        reconsider i1 as Nat by A20;



         A21: ex k be Nat st i1 = k & 0 < (Dseq . i1) & for q be Element of ( REAL m) st q in X & |.(q - x).| < (Dseq . i1) holds |.(( partdiff (f,q,k)) - ( partdiff (f,x,k))).| < r by A17, A20;

         A22:

        now

          let q be Element of ( REAL m);

          assume

           A23: |.(q - x).| < d;

          d <= d0 by XXREAL_0: 17;

          then |.(q - x).| < d0 by A23, XXREAL_0: 2;

          then q in { y where y be Element of ( REAL m) : |.(y - x).| < d0 };

          hence q in X by A4;

        end;

         A24:

        now

          let q be Element of ( REAL m), i be Nat;

          assume

           A25: |.(q - x).| < d & i in ( Seg m);

          reconsider i0 = i as Nat;

          consider k be Nat such that

           A26: i0 = k & 0 < (Dseq . i0) & for q be Element of ( REAL m) st q in X & |.(q - x).| < (Dseq . i0) holds |.(( partdiff (f,q,k)) - ( partdiff (f,x,k))).| < r by A17, A25;

          (Dseq . i0) in ( rng Dseq) by A17, A25, FUNCT_1: 3;

          then

           A27: d1 <= (Dseq . i0) by XXREAL_2:def 7;

          d <= d1 by XXREAL_0: 17;

          then d <= (Dseq . i0) by A27, XXREAL_0: 2;

          then |.(q - x).| < (Dseq . i0) by A25, XXREAL_0: 2;

          hence |.(( partdiff (f,q,i)) - ( partdiff (f,x,i))).| < r by A22, A25, A26;

        end;

        take d;

        thus 0 < d by A3, A20, A21, XXREAL_0: 21;

        thus for y be Element of ( REAL m), z be Element of ( REAL 1) st y <> ( 0* m) & |.y.| < d & z = (R . y) holds (( |.y.| " ) * |.z.|) < r0

        proof

          let y be Element of ( REAL m), z be Element of ( REAL 1);

          assume

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

          consider h be FinSequence of ( REAL m), g be FinSequence of ( REAL 1) such that

           A29: ( len h) = (m + 1) & ( len g) = m & (for i be Nat st i in ( dom h) holds (h /. i) = ((y | ((m + 1) -' i)) ^ ( 0* (i -' 1)))) & (for i be Nat st i in ( dom g) holds (g /. i) = ((f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))))) & (for i be Nat, hi be Element of ( REAL m) st i in ( dom h) & (h /. i) = hi holds |.hi.| <= |.y.|) & ((f /. (x + y)) - (f /. x)) = ( Sum g) by Th28;



           A30: (R /. y) = (( Sum g) - (L . y)) by A6, A29;

          consider w be FinSequence of ( REAL 1) such that

           A31: ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . y) * ( partdiff (f,x,i)))) & (L . y) = ( Sum w) by A2;

          ( idseq m) is Permutation of ( Seg m) by FINSEQ_2: 55;

          then

           A32: ( dom ( idseq m)) = ( Seg m) & ( rng ( idseq m)) = ( Seg m) & ( idseq m) is one-to-one by FUNCT_2:def 1, FUNCT_2:def 3;

          then

           A33: ( dom ( Rev ( idseq m))) = ( Seg m) & ( rng ( Rev ( idseq m))) = ( Seg m) by FINSEQ_5: 57;

          then

          reconsider Ri = ( Rev ( idseq m)) as Function of ( Seg m), ( Seg m) by FUNCT_2: 1;

          Ri is one-to-one onto by A33, FUNCT_2:def 3;

          then

          reconsider Ri = ( Rev ( idseq m)) as Permutation of ( dom w) by A31;

          reconsider mm = m as Element of NAT by ORDINAL1:def 12;



           A34: ( len ( idseq m)) = mm by A32, FINSEQ_1:def 3

          .= ( len w) by A31, FINSEQ_1:def 3;



           A35: ( dom (w (*) Ri)) = ( dom Ri) by A33, RELAT_1: 27

          .= ( dom ( Rev w)) by A33, A31, FINSEQ_5: 57;

          now

            let k be Nat;

            assume

             A36: k in ( dom ( Rev w));

            then

             A37: k in ( dom ( Rev ( idseq m))) by A33, A31, FINSEQ_5: 57;

            then

             A38: 1 <= k & k <= m by A33, FINSEQ_1: 1;

            then

            reconsider mk = (m - k) as Nat by NAT_1: 21;

            reconsider mm = m as Element of NAT by ORDINAL1:def 12;



             A39: ( len ( idseq m)) = mm by A32, FINSEQ_1:def 3;

             0 <= mk;

            then

             A40: ( 0 + 1) <= ((m - k) + 1) by XREAL_1: 6;

            (k - 1) >= (1 - 1) by A38, XREAL_1: 9;

            then (m - (k - 1)) <= m by XREAL_1: 43;

            then

             A41: (mk + 1) in ( Seg m) by A40;



            thus (( Rev w) . k) = (w . ((( len ( idseq m)) - k) + 1)) by A34, A36, FINSEQ_5:def 3

            .= (w . (( idseq m) . ((( len ( idseq m)) - k) + 1))) by A41, A39, FINSEQ_2: 49

            .= (w . (( Rev ( idseq m)) . k)) by A37, FINSEQ_5:def 3

            .= ((w (*) Ri) . k) by A36, A35, FUNCT_1: 12;

          end;

          then

           A42: ( Sum ( Rev w)) = ( Sum w) by A35, EUCLID_7: 21, FINSEQ_1: 13;

          deffunc GW( Nat) = ((g /. $1) - (( Rev w) /. $1));

          consider gw be FinSequence of ( REAL 1) such that

           A43: ( len gw) = m & for j be Nat st j in ( dom gw) holds (gw . j) = GW(j) from FINSEQ_2:sch 1;

           A44:

          now

            let j be Nat;

            assume

             A45: j in ( dom gw);



            hence (gw /. j) = (gw . j) by PARTFUN1:def 6

            .= ((g /. j) - (( Rev w) /. j)) by A45, A43;

          end;

          reconsider mm = m as Element of NAT by ORDINAL1:def 12;



           A46: ( len w) = mm by A31, FINSEQ_1:def 3;

          then ( len ( Rev w)) = m by FINSEQ_5:def 3;

          then

           A47: (R /. y) = ( Sum gw) by A29, A30, A31, A43, A44, A42, Th27;



           A48: for j be Nat st j in ( dom gw) holds ex gwj be Element of ( REAL 1) st (gw . j) = gwj & |.gwj.| <= ( |.y.| * r)

          proof

            let j be Nat;

            assume

             A49: j in ( dom gw);

            then

             A50: j in ( Seg m) by A43, FINSEQ_1:def 3;

            then j in ( dom g) by A29, FINSEQ_1:def 3;

            then

             A51: (g /. j) = ((f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1))))) by A29;



             A52: 1 <= j & j <= m by A50, FINSEQ_1: 1;

            then (m + 1) <= (m + j) & (j + 1) <= (m + 1) by XREAL_1: 6;

            then ((m + 1) - j) <= m & 1 <= ((m + 1) - j) by XREAL_1: 19, XREAL_1: 20;

            then

             A53: ((m + 1) -' j) <= m & 1 <= ((m + 1) -' j) by A52, NAT_D: 37;

            then

             A54: f is_partial_differentiable_on (X,((m + 1) -' j)) by A1;

            then

             A55: X c= ( dom f) & for x be Element of ( REAL m) st x in X holds f is_partial_differentiable_in (x,((m + 1) -' j)) by A53, Th34, A1;



             A56: ((m + 1) -' j) in ( Seg m) by A53;



            then

             A57: (w /. ((m + 1) -' j)) = (w . ((m + 1) -' j)) by A31, PARTFUN1:def 6

            .= ((( proj (((m + 1) -' j),m)) . y) * ( partdiff (f,x,((m + 1) -' j)))) by A31, A56;

             A58:

            now

              let j be Nat;

              assume 1 <= j & j <= (m + 1);

              then j in ( Seg (m + 1));

              then

               A59: j in ( dom h) by A29, FINSEQ_1:def 3;



               A60: ((x + (h /. j)) - x) = (h /. j) by RVSUM_1: 42;

              reconsider hj = (h /. j) as Element of ( REAL m);

               |.hj.| <= |.y.| by A29, A59;

              hence |.((x + (h /. j)) - x).| < d by A60, A28, XXREAL_0: 2;

            end;

            ( rng f0) c= ( dom (( proj (1,1)) qua Function " )) by PDIFF_1: 2;

            then

             A61: ( dom f) = ( dom f0) by A7, RELAT_1: 27;

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

            then ( Seg m) c= ( Seg (m + 1)) by FINSEQ_1: 5;

            then 1 <= j & j <= (m + 1) by A50, FINSEQ_1: 1;

            then

             A62: |.((x + (h /. j)) - x).| < d by A58;

            then

             A63: (x + (h /. j)) in X by A22;



            then

             A64: (f /. (x + (h /. j))) = (( <>* f0) . (x + (h /. j))) by A55, A7, PARTFUN1:def 6

            .= ((( proj (1,1)) qua Function " ) . (f0 . (x + (h /. j)))) by A63, A55, A61, FUNCT_1: 13

            .= <*(f0 . (x + (h /. j)))*> by PDIFF_1: 1

            .= <*(f0 /. (x + (h /. j)))*> by A63, A55, A61, PARTFUN1:def 6;



             A65: 1 <= j & j <= m by A50, FINSEQ_1: 1;



             A66: 1 <= (j + 1) by NAT_1: 11;



             A67: (j + 1) <= (m + 1) by A65, XREAL_1: 6;

            then

             A68: |.((x + (h /. (j + 1))) - x).| < d by A66, A58;

            then

             A69: (x + (h /. (j + 1))) in X by A22;



            then

             A70: (f /. (x + (h /. (j + 1)))) = (( <>* f0) . (x + (h /. (j + 1)))) by A55, A7, PARTFUN1:def 6

            .= ((( proj (1,1)) qua Function " ) . (f0 . (x + (h /. (j + 1))))) by A69, A55, A61, FUNCT_1: 13

            .= <*(f0 . (x + (h /. (j + 1))))*> by PDIFF_1: 1

            .= <*(f0 /. (x + (h /. (j + 1))))*> by A69, A55, A61, PARTFUN1:def 6;

            f is_partial_differentiable_in (x,((m + 1) -' j)) by A54, A53, Th34, A1;

            then

             A71: ( partdiff (f,x,((m + 1) -' j))) = <*( partdiff (f0,x,((m + 1) -' j)))*> by A7, PDIFF_1: 19;

            then

             A72: ((( proj (((m + 1) -' j),m)) . y) * ( partdiff (f,x,((m + 1) -' j)))) = <*((( proj (((m + 1) -' j),m)) . y) * ( partdiff (f0,x,((m + 1) -' j))))*> by RVSUM_1: 47;



             A73: ((f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1))))) = <*((f0 /. (x + (h /. j))) - (f0 /. (x + (h /. (j + 1)))))*> by A64, A70, RVSUM_1: 29;



             A74: X c= ( dom f0) & for x be Element of ( REAL m) st x in X holds f0 is_partial_differentiable_in (x,((m + 1) -' j))

            proof

              thus X c= ( dom f0) by A54, A61;

              let x be Element of ( REAL m);

              assume x in X;

              then f is_partial_differentiable_in (x,((m + 1) -' j)) by A54, A53, Th34, A1;

              hence f0 is_partial_differentiable_in (x,((m + 1) -' j)) by A7, PDIFF_1: 18;

            end;



             A75: (x + (h /. j)) = (( reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . (( proj (((m + 1) -' j),m)) . (x + y))) by Th46, A29, A65;

            ((m + 1) -' (j + 1)) = ((m + 1) - (j + 1)) by A67, XREAL_1: 233;

            then ((m + 1) -' (j + 1)) = (m - j);

            then

             A76: ((m + 1) -' (j + 1)) = (m -' j) by A65, XREAL_1: 233;



             A77: ((j + 1) -' 1) = ((j + 1) - 1) by NAT_1: 11, XREAL_1: 233;

            consider q be Element of ( REAL m) such that

             A78: |.(q - x).| < d & f0 is_partial_differentiable_in (q,((m + 1) -' j)) & ((f0 /. (x + (h /. j))) - (f0 /. (x + (h /. (j + 1))))) = (((( proj (((m + 1) -' j),m)) . (x + y)) - (( proj (((m + 1) -' j),m)) . (x + (h /. (j + 1))))) * ( partdiff (f0,q,((m + 1) -' j)))) by A62, A68, A75, A53, A74, A22, A1, Th45;



             A79: |.(( partdiff (f,q,((m + 1) -' j))) - ( partdiff (f,x,((m + 1) -' j)))).| < r by A78, A56, A24;

            f is_partial_differentiable_in (q,((m + 1) -' j)) by A78, A7, PDIFF_1: 18;

            then

             A80: ( partdiff (f,q,((m + 1) -' j))) = <*( partdiff (f0,q,((m + 1) -' j)))*> by A7, PDIFF_1: 19;

            set mij = ((m + 1) -' j);

            set mj = (m -' j);

            reconsider hj1 = (h /. (j + 1)) as Element of ( REAL m);



             A81: ( len x) = m & ( len y) = m & ( len hj1) = m by CARD_1:def 7;

            then mij in ( dom x) & mij in ( dom y) & mij in ( dom hj1) by A56, FINSEQ_1:def 3;

            then mij in (( dom x) /\ ( dom y)) & mij in (( dom x) /\ ( dom hj1)) by XBOOLE_0:def 4;

            then

             A82: mij in ( dom (x + y)) & mij in ( dom (x + hj1)) by VALUED_1:def 1;

            (j + 1) in ( Seg (m + 1)) by A66, A67;

            then (j + 1) in ( dom h) by A29, FINSEQ_1:def 3;

            then

             A83: (h /. (j + 1)) = ((y | mj) ^ ( 0* j)) by A29, A76, A77;



             A84: ( len (y | mj)) = mj by A81, FINSEQ_1: 59, NAT_D: 35;

            mij = (mj + 1) by A65, NAT_D: 38;

            then mij > ( len (y | mj)) by A84, NAT_1: 13;



            then

             A85: (hj1 . mij) = (( 0* j) . (mij - mj)) by A53, A81, A83, A84, FINSEQ_1: 24

            .= 0 ;



             A86: ((( proj (((m + 1) -' j),m)) . (x + y)) - (( proj (((m + 1) -' j),m)) . (x + (h /. (j + 1))))) = (((x + y) . mij) - (( proj (((m + 1) -' j),m)) . (x + (h /. (j + 1))))) by PDIFF_1:def 1

            .= (((x + y) . mij) - ((x + (h /. (j + 1))) . mij)) by PDIFF_1:def 1

            .= (((x . mij) + (y . mij)) - ((x + (h /. (j + 1))) . mij)) by A82, VALUED_1:def 1

            .= (((x . mij) + (y . mij)) - ((x . mij) + 0 )) by A85, A82, VALUED_1:def 1

            .= (( proj (((m + 1) -' j),m)) . y) by PDIFF_1:def 1;

            reconsider gwj = (gw /. j) as Element of ( REAL 1);

            take gwj;

            thus (gw . j) = gwj by A49, PARTFUN1:def 6;



             A87: ((m + 1) -' j) = ((m + 1) - j) by A65, NAT_1: 12, XREAL_1: 233;

            j in ( Seg ( len ( Rev w))) by A50, A46, FINSEQ_5:def 3;

            then

             A88: j in ( dom ( Rev w)) by FINSEQ_1:def 3;



            then (( Rev w) /. j) = (( Rev w) . j) by PARTFUN1:def 6

            .= (w . ((m - j) + 1)) by A46, A88, FINSEQ_5:def 3

            .= (w /. ((m + 1) -' j)) by A87, A56, A31, PARTFUN1:def 6;



            then (gw /. j) = ((g /. j) - (w /. ((m + 1) -' j))) by A49, A44

            .= <*(((( proj (((m + 1) -' j),m)) . y) * ( partdiff (f0,q,((m + 1) -' j)))) - ((( proj (((m + 1) -' j),m)) . y) * ( partdiff (f0,x,((m + 1) -' j)))))*> by A78, A86, A57, A51, A72, A73, RVSUM_1: 29

            .= <*((( proj (((m + 1) -' j),m)) . y) * (( partdiff (f0,q,((m + 1) -' j))) - ( partdiff (f0,x,((m + 1) -' j)))))*>

            .= ((( proj (((m + 1) -' j),m)) . y) * <*(( partdiff (f0,q,((m + 1) -' j))) - ( partdiff (f0,x,((m + 1) -' j))))*>) by RVSUM_1: 47

            .= ((( proj (((m + 1) -' j),m)) . y) * (( partdiff (f,q,((m + 1) -' j))) - ( partdiff (f,x,((m + 1) -' j))))) by A71, A80, RVSUM_1: 29;

            then

             A89: |.gwj.| = ( |.(( proj (((m + 1) -' j),m)) . y).| * |.(( partdiff (f,q,((m + 1) -' j))) - ( partdiff (f,x,((m + 1) -' j)))).|) by EUCLID: 11;

             0 <= |.(( proj (((m + 1) -' j),m)) . y).| by COMPLEX1: 46;

            then

             A90: |.gwj.| <= ( |.(( proj (((m + 1) -' j),m)) . y).| * r) by A89, A79, XREAL_1: 64;

             |.(y . ((m + 1) -' j)).| <= |.y.| by A56, REAL_NS1: 8;

            then |.(( proj (((m + 1) -' j),m)) . y).| <= |.y.| by PDIFF_1:def 1;

            then ( |.(( proj (((m + 1) -' j),m)) . y).| * r) <= ( |.y.| * r) by A9, XREAL_1: 64;

            hence |.gwj.| <= ( |.y.| * r) by A90, XXREAL_0: 2;

          end;

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

           A91:

          now

            let k be Nat;

            assume k in ( Seg m);

            then k in ( dom gw) by A43, FINSEQ_1:def 3;

            then

            reconsider v = (gw . k) as Element of ( REAL 1) by PARTFUN1: 4;

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

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

          end;

          consider yseq be FinSequence of REAL such that

           A92: ( dom yseq) = ( Seg m) & for i be Nat st i in ( Seg m) holds YSQ[i, (yseq . i)] from FINSEQ_1:sch 5( A91);



           A93: ( len gw) = ( len yseq) by A43, A92, FINSEQ_1:def 3;

           A94:

          now

            let i be Nat;

            assume i in ( dom gw);

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

            hence ex v be Element of ( REAL 1) st v = (gw . i) & (yseq . i) = |.v.| by A92;

          end;

          reconsider yseq as Element of ( REAL m) by A93, A43, FINSEQ_2: 92;



           A95: |.( Sum gw).| <= ( Sum yseq) by A94, A93, PDIFF_6: 17;

          reconsider yr = ( |.y.| * r) as Element of REAL by XREAL_0:def 1;

          for j be Nat st j in ( Seg m) holds (yseq . j) <= ((m |-> yr) . j)

          proof

            let j be Nat;

            assume

             A96: j in ( Seg m);

            then

             A97: j in ( dom gw) by A43, FINSEQ_1:def 3;

            then

             A98: ex v be Element of ( REAL 1) st v = (gw . j) & (yseq . j) = |.v.| by A94;

            ex gwj be Element of ( REAL 1) st (gw . j) = gwj & |.gwj.| <= ( |.y.| * r) by A48, A97;

            hence (yseq . j) <= ((m |-> yr) . j) by A98, A96, FINSEQ_2: 57;

          end;

          then ( Sum yseq) <= ( Sum (m |-> yr)) by RVSUM_1: 82;

          then ( Sum yseq) <= (m * ( |.y.| * r)) by RVSUM_1: 80;

          then |.z.| <= (m * ( |.y.| * r)) by A47, A28, A95, XXREAL_0: 2;

          then ( |.z.| * ( |.y.| " )) <= (((m * |.y.|) * r) * ( |.y.| " )) by XREAL_1: 64;

          then ( |.z.| * ( |.y.| " )) <= (m * ((r * |.y.|) * ( |.y.| " )));

          then (( |.y.| " ) * |.z.|) <= (m * r) by A28, EUCLID: 8, XCMPLX_1: 203;

          then

           A99: (( |.y.| " ) * |.z.|) <= r1 by XCMPLX_1: 87;

          r1 < r0 by A9, XREAL_1: 216;

          hence (( |.y.| " ) * |.z.|) < r0 by A99, XXREAL_0: 2;

        end;

      end;

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

      proof

        let y be Element of ( REAL m);

        assume |.(y - x).| < d0;

        (R . (y - x)) = (((f /. (x + (y - x))) - (f /. x)) - (L . (y - x))) by A6;



        hence ((L . (y - x)) + (R . (y - x))) = (((f /. (x + (y - x))) - (f /. x)) - ((L . (y - x)) - (L . (y - x)))) by RVSUM_1: 41

        .= (((f /. (x + (y - x))) - (f /. x)) - ( 0* 1)) by RVSUM_1: 37

        .= ((f /. (x + (y - x))) - (f /. x)) by RVSUM_1: 32

        .= ((f /. ((x + y) - x)) - (f /. x)) by RVSUM_1: 40

        .= ((f /. (y + (x - x))) - (f /. x)) by RVSUM_1: 40

        .= ((f /. (y + ( 0* m))) - (f /. x)) by RVSUM_1: 37

        .= ((f /. y) - (f /. x)) by RVSUM_1: 16;

      end;

      then f is_differentiable_in x & ( diff (f,x)) = L by A3, A5, A8, PDIFF_6: 24;

      hence thesis by A2;

    end;

    theorem :: PDIFF_7:48



     Th48: for m be non zero Nat, f be PartFunc of ( REAL-NS m), ( REAL-NS 1), X be Subset of ( REAL-NS m), x be Point of ( REAL-NS m) st X is open & x in X & (for i be Nat st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X) holds f is_differentiable_in x & for h be Point of ( REAL-NS m) holds ex w be FinSequence of ( REAL 1) st ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = (( partdiff (f,x,i)) . <*(( proj (i,m)) . h)*>)) & (( diff (f,x)) . h) = ( Sum w)

    proof

      let m be non zero Nat, f be PartFunc of ( REAL-NS m), ( REAL-NS 1), X be Subset of ( REAL-NS m), x be Point of ( REAL-NS m);

      assume

       A1: X is open & x in X & (for i be Nat st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X);



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

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

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

      reconsider f0 = f as PartFunc of ( REAL m), ( REAL 1) by A2;

      reconsider X0 = X as Subset of ( REAL m) by REAL_NS1:def 4;

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



       A3: X0 is open by A1;

       A4:

      now

        let i be Nat;

        assume

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

        then

         A6: f is_partial_differentiable_on (X,i) by A1;

        hence

         A7: f0 is_partial_differentiable_on (X0,i) by Th33;



         A8: (f `partial| (X,i)) is_continuous_on X by A1, A5;



         A9: ( dom (f0 `partial| (X0,i))) = X0 & for x0 be Element of ( REAL m) st x0 in X0 holds ((f0 `partial| (X0,i)) /. x0) = ( partdiff (f0,x0,i)) by Def5, A7;



         A10: for z be Element of ( REAL m) st z in X0 holds ex y be Point of ( REAL-NS m) st z = y & ((f0 `partial| (X0,i)) /. z) = (( partdiff (f,y,i)) . One)

        proof

          let z be Element of ( REAL m);

          assume

           A11: z in X0;

          then f0 is_partial_differentiable_in (z,i) by A7, A5, A3, Th34;

          then

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

           A12: f0 = g & z = y & ( partdiff (f0,z,i)) = (( partdiff (g,y,i)) . <*1*>) by PDIFF_1:def 14;

          take y;

          thus z = y by A12;

          thus ((f0 `partial| (X0,i)) /. z) = (( partdiff (f,y,i)) . One) by A12, A11, Def5, A7;

        end;

        for z0 be Element of ( REAL m), r be Real st z0 in X0 & 0 < r holds ex s be Real st 0 < s & for z1 be Element of ( REAL m) st z1 in X & |.(z1 - z0).| < s holds |.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r

        proof

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

          assume

           A13: z0 in X0 & 0 < r;

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

          consider s be Real such that

           A14: 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by A8, A13, NFCONT_1: 19;

          reconsider s as Real;

          take s;

          thus 0 < s by A14;

          thus for z1 be Element of ( REAL m) st z1 in X & |.(z1 - z0).| < s holds |.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r

          proof

            let z1 be Element of ( REAL m);

            assume

             A15: z1 in X & |.(z1 - z0).| < s;

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

             |.(z1 - z0).| = ||.(y1 - y0).|| by REAL_NS1: 1, REAL_NS1: 5;

            then

             A16: ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by A15, A14;

            ((f `partial| (X,i)) /. y1) = ( partdiff (f,y1,i)) by A6, A15, PDIFF_1:def 20;

            then

             A17: ||.(( partdiff (f,y1,i)) - ( partdiff (f,y0,i))).|| < r by A16, A6, A13, PDIFF_1:def 20;



             A18: ex y1 be Point of ( REAL-NS m) st z1 = y1 & ((f0 `partial| (X0,i)) /. z1) = (( partdiff (f,y1,i)) . One) by A10, A15;



             A19: ex y0 be Point of ( REAL-NS m) st z0 = y0 & ((f0 `partial| (X0,i)) /. z0) = (( partdiff (f,y0,i)) . One) by A10, A13;

            reconsider PDP = (( partdiff (f,y1,i)) - ( partdiff (f,y0,i))) as Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1) by LOPBAN_1:def 9;

            ((( partdiff (f,y1,i)) . One) - (( partdiff (f,y0,i)) . One)) = (PDP . One) by LOPBAN_1: 40;

            then

             A20: ||.((( partdiff (f,y1,i)) . One) - (( partdiff (f,y0,i)) . One)).|| <= ( ||.(( partdiff (f,y1,i)) - ( partdiff (f,y0,i))).|| * ||.One.||) by LOPBAN_1: 32;

             ||.One.|| = |.One0.| by REAL_NS1: 1

            .= |.1.| by TOPREALC: 18

            .= 1 by ABSVALUE:def 1;

            then ||.((( partdiff (f,y1,i)) . One) - (( partdiff (f,y0,i)) . One)).|| < r by A20, A17, XXREAL_0: 2;

            hence |.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r by A18, A19, REAL_NS1: 1, REAL_NS1: 5;

          end;

        end;

        hence (f0 `partial| (X0,i)) is_continuous_on X0 by A9, Th38;

      end;

      then

       A21: f0 is_differentiable_in x0 & for h0 be Element of ( REAL m) holds ex w be FinSequence of ( REAL 1) st ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . h0) * ( partdiff (f0,x0,i)))) & (( diff (f0,x0)) . h0) = ( Sum w) by Th47, A3, A1;

      then ex g be PartFunc of ( REAL-NS m), ( REAL-NS 1), y be Point of ( REAL-NS m) st f0 = g & x0 = y & g is_differentiable_in y;

      hence f is_differentiable_in x;



       A22: ex g be PartFunc of ( REAL-NS m), ( REAL-NS 1), y be Point of ( REAL-NS m) st f0 = g & x0 = y & ( diff (f0,x0)) = ( diff (g,y)) by A21, PDIFF_1:def 8;

      now

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

        reconsider h0 = h as Element of ( REAL m) by REAL_NS1:def 4;

        consider w be FinSequence of ( REAL 1) such that

         A23: ( dom w) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w . i) = ((( proj (i,m)) . h0) * ( partdiff (f0,x0,i)))) & (( diff (f0,x0)) . h0) = ( Sum w) by Th47, A3, A1, A4;

        take w;

        thus ( dom w) = ( Seg m) by A23;

        thus for i be Nat st i in ( Seg m) holds (w . i) = (( partdiff (f,x,i)) . <*(( proj (i,m)) . h)*>)

        proof

          let i be Nat;

          assume

           A24: i in ( Seg m);

          then

           A25: 1 <= i & i <= m by FINSEQ_1: 1;

          then f0 is_partial_differentiable_on (X0,i) by A4;

          then f0 is_partial_differentiable_in (x0,i) by A1, A3, A25, Th34;

          then

           A26: ex g be PartFunc of ( REAL-NS m), ( REAL-NS 1), y be Point of ( REAL-NS m) st f0 = g & x0 = y & ( partdiff (f0,x0,i)) = (( partdiff (g,y,i)) . <*1*>) by PDIFF_1:def 14;



           A27: ((( proj (i,m)) . h) * One) = ((( proj (i,m)) . h0) * One0) by REAL_NS1: 3

          .= <*((( proj (i,m)) . h0) * 1)*> by RVSUM_1: 47

          .= <*(( proj (i,m)) . h)*>;

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

          ((( proj (i,m)) . h0) * ( partdiff (f0,x0,i))) = ((( proj (i,m)) . h0) * (PDP . One)) by A26, REAL_NS1: 3

          .= (( partdiff (f,x,i)) . <*(( proj (i,m)) . h)*>) by A27, LOPBAN_1:def 5;

          hence (w . i) = (( partdiff (f,x,i)) . <*(( proj (i,m)) . h)*>) by A24, A23;

        end;

        thus (( diff (f,x)) . h) = ( Sum w) by A23, A22;

      end;

      hence thesis;

    end;

    theorem :: PDIFF_7:49

    for m be non zero Nat, f be PartFunc of ( REAL-NS m), ( REAL-NS 1), X be Subset of ( REAL-NS m) st X is open holds (for i be Nat st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X) iff f is_differentiable_on X & (f `| X) is_continuous_on X

    proof

      let m be non zero Nat, f be PartFunc of ( REAL-NS m), ( REAL-NS 1), X be Subset of ( REAL-NS m);

      assume

       A1: X is open;

      hereby

        assume

         A2: for i be Nat st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X;

         A3:

        now

          let i be Nat;

          assume 1 <= i & i <= m;

          then (f `partial| (X,i)) is_continuous_on X by A2;

          hence X c= ( dom (f `partial| (X,i))) & for y0 be Point of ( REAL-NS m), r be Real st y0 in X & 0 < r holds ex s be Real st 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by NFCONT_1: 19;

        end;

        1 <= m by NAT_1: 14;

        then f is_partial_differentiable_on (X,m) by A2;

        then

         A4: X c= ( dom f);

        for x be Point of ( REAL-NS m) st x in X holds f is_differentiable_in x by A1, A2, Th48;

        hence

         A5: f is_differentiable_on X by A1, A4, NDIFF_1: 31;

        then

         A6: ( dom (f `| X)) = X by NDIFF_1:def 9;

        for y0 be Point of ( REAL-NS m), r be Real st y0 in X & 0 < r holds ex s be Real st 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r

        proof

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

          assume

           A7: y0 in X & 0 < r;

          defpred P[ Nat, Real] means for i be Nat st i = $1 holds ( 0 < $2 & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < $2 holds ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < (r / (2 * m)));

           A8:

          now

            let i be Nat;

            reconsider j = i as Nat;

            assume i in ( Seg m);

            then 1 <= j & j <= m by FINSEQ_1: 1;

            then

            consider s be Real such that

             A9: 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.(((f `partial| (X,j)) /. y1) - ((f `partial| (X,j)) /. y0)).|| < (r / (2 * m)) by A7, A3;

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

            take s;

            thus P[i, s] by A9;

          end;

          consider S be FinSequence of REAL such that

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

          take s = ( min S);

          reconsider mm = m as Element of NAT by ORDINAL1:def 12;



           A11: ( len S) = mm by A10, FINSEQ_1:def 3;

          then s = (S . ( min_p S)) & ( min_p S) in ( dom S) by RFINSEQ2:def 2, RFINSEQ2:def 4;

          hence s > 0 by A10;

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

          assume

           A12: y1 in X & ||.(y1 - y0).|| < s;

          reconsider DD = (( diff (f,y1)) - ( diff (f,y0))) as Lipschitzian LinearOperator of ( REAL-NS m), ( REAL-NS 1) by LOPBAN_1:def 9;



           A13: ( upper_bound ( PreNorms DD)) = ||.(( diff (f,y1)) - ( diff (f,y0))).|| by LOPBAN_1: 30;

          now

            let mt be Real;

            assume mt in ( PreNorms DD);

            then

            consider t be VECTOR of ( REAL-NS m) such that

             A14: mt = ||.(DD . t).|| & ||.t.|| <= 1;

            reconsider tt = t as Element of ( REAL m) by REAL_NS1:def 4;

            consider w0 be FinSequence of ( REAL 1) such that

             A15: ( dom w0) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w0 . i) = (( partdiff (f,y0,i)) . <*(( proj (i,m)) . t)*>)) & (( diff (f,y0)) . t) = ( Sum w0) by A1, A2, Th48, A7;

            reconsider Sw0 = ( Sum w0) as Point of ( REAL-NS 1) by A15;

            consider w1 be FinSequence of ( REAL 1) such that

             A16: ( dom w1) = ( Seg m) & (for i be Nat st i in ( Seg m) holds (w1 . i) = (( partdiff (f,y1,i)) . <*(( proj (i,m)) . t)*>)) & (( diff (f,y1)) . t) = ( Sum w1) by A1, A2, Th48, A12;

            reconsider Sw1 = ( Sum w1) as Point of ( REAL-NS 1) by A16;

            deffunc F( set) = ((w1 /. $1) - (w0 /. $1));

            consider w2 be FinSequence of ( REAL 1) such that

             A17: ( len w2) = m & for i be Nat st i in ( dom w2) holds (w2 . i) = F(i) from FINSEQ_2:sch 1;

            reconsider mm = m as Element of NAT by ORDINAL1:def 12;



             A18: ( len w1) = mm & ( len w0) = mm by A15, A16, FINSEQ_1:def 3;

            now

              let i be Nat;

              assume

               A19: i in ( dom w2);

              then (w2 . i) = F(i) by A17;

              hence (w2 /. i) = F(i) by A19, PARTFUN1:def 6;

            end;

            then

             A20: ( Sum w2) = (( Sum w1) - ( Sum w0)) by A17, Th27, A18;

            (DD . t) = (Sw1 - Sw0) by A16, A15, LOPBAN_1: 40

            .= ( Sum w2) by A20, REAL_NS1: 5;

            then

             A21: mt = |.( Sum w2).| by A14, REAL_NS1: 1;

            deffunc F( Nat) = ( In ( |.(w2 /. $1) qua Element of ( REAL 1).|, REAL ));

            consider ys be FinSequence of REAL such that

             A22: ( len ys) = m & for j be Nat st j in ( dom ys) holds (ys . j) = F(j) from FINSEQ_2:sch 1;

             A23:

            now

              let i be Nat;

              assume

               A24: i in ( dom w2);

              reconsider v = (w2 /. i) as Element of ( REAL 1);

              take v;

              thus v = (w2 . i) by A24, PARTFUN1:def 6;

              i in ( Seg m) by A17, A24, FINSEQ_1:def 3;

              then i in ( dom ys) by A22, FINSEQ_1:def 3;

              then (ys . i) = F(i) by A22;

              hence (ys . i) = |.v.|;

            end;

            then

             A25: |.( Sum w2).| <= ( Sum ys) by A17, A22, PDIFF_6: 17;

            reconsider rm = (r / (2 * m)) as Element of REAL by XREAL_0:def 1;

            deffunc F( Nat) = rm;

            consider rs be FinSequence of REAL such that

             A26: ( len rs) = m & for j be Nat st j in ( dom rs) holds (rs . j) = F(j) from FINSEQ_2:sch 1;



             A27: ( dom rs) = ( Seg m) by A26, FINSEQ_1:def 3;

            ( rng rs) = {rm}

            proof

              thus ( rng rs) c= {rm}

              proof

                let a be object;

                assume a in ( rng rs);

                then

                consider b be object such that

                 A28: b in ( dom rs) & a = (rs . b) by FUNCT_1:def 3;

                reconsider b as Nat by A28;

                (rs . b) = rm by A28, A26;

                hence a in {rm} by A28, TARSKI:def 1;

              end;

              let a be object;

              assume a in {rm};

              then

               A29: a = rm by TARSKI:def 1;

              1 <= m by NAT_1: 14;

              then

               A30: 1 in ( dom rs) by A27;

              then a = (rs . 1) by A29, A26;

              hence a in ( rng rs) by A30, FUNCT_1: 3;

            end;

            then rs = (m |-> (r / (2 * m))) by A27, FUNCOP_1: 9;



            then

             A31: ( Sum rs) = (m * (r / (2 * m))) by RVSUM_1: 80

            .= (m * ((r / 2) / m)) by XCMPLX_1: 78

            .= (r / 2) by XCMPLX_1: 87;

            now

              let i be Element of NAT ;

              assume i in ( dom ys);

              then

               A32: i in ( Seg m) by A22, FINSEQ_1:def 3;

              then

               A33: i in ( dom w2) & i in ( dom w1) & i in ( dom w0) by A15, A16, A17, FINSEQ_1:def 3;

              then

              consider v be Element of ( REAL 1) such that

               A34: v = (w2 . i) & (ys . i) = |.v.| by A23;



               A35: i in ( dom rs) by A26, A32, FINSEQ_1:def 3;

              reconsider p1 = ( partdiff (f,y1,i)), p0 = ( partdiff (f,y0,i)) as Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1) by LOPBAN_1:def 9;



               A36: ( dom p1) = the carrier of ( REAL-NS 1) & ( rng p1) c= the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

              (( proj (i,m)) . t) in REAL by XREAL_0:def 1;

              then <*(( proj (i,m)) . t)*> in ( REAL 1) by FINSEQ_2: 98;

              then <*(( proj (i,m)) . t)*> in the carrier of ( REAL-NS 1) by REAL_NS1:def 4;

              then (p1 . <*(( proj (i,m)) . t)*>) in ( rng p1) by A36, FUNCT_1: 3;

              then

              reconsider P1 = (p1 . <*(( proj (i,m)) . t)*>) as VECTOR of ( REAL-NS 1);



               A37: ( dom p0) = the carrier of ( REAL-NS 1) & ( rng p0) c= the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

              (( proj (i,m)) . t) in REAL by XREAL_0:def 1;

              then <*(( proj (i,m)) . t)*> in ( REAL 1) by FINSEQ_2: 98;

              then <*(( proj (i,m)) . t)*> in the carrier of ( REAL-NS 1) by REAL_NS1:def 4;

              then (p0 . <*(( proj (i,m)) . t)*>) in ( rng p0) by A37, FUNCT_1: 3;

              then

              reconsider P0 = (p0 . <*(( proj (i,m)) . t)*>) as VECTOR of ( REAL-NS 1);



               A38: (w1 /. i) = (w1 . i) by A32, A16, PARTFUN1:def 6

              .= P1 by A16, A32;



               A39: (w0 /. i) = (w0 . i) by A32, A15, PARTFUN1:def 6

              .= P0 by A15, A32;



               A40: (w2 . i) = ((w1 /. i) - (w0 /. i)) by A33, A17

              .= (P1 - P0) by A39, A38, REAL_NS1: 5;

              1 <= i & i <= ( len S) by A11, A32, FINSEQ_1: 1;

              then

               A41: s <= (S . i) & f is_partial_differentiable_on (X,i) by A11, A2, RFINSEQ2: 2;

              then ||.(y1 - y0).|| < (S . i) by A12, XXREAL_0: 2;

              then ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < (r / (2 * m)) by A10, A32, A12;

              then ||.(( partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < (r / (2 * m)) by A12, A41, PDIFF_1:def 20;

              then

               A42: ||.(( partdiff (f,y1,i)) - ( partdiff (f,y0,i))).|| < (r / (2 * m)) by A7, A41, PDIFF_1:def 20;

              reconsider PP = (( partdiff (f,y1,i)) - ( partdiff (f,y0,i))) as Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1) by LOPBAN_1:def 9;



               A43: ( upper_bound ( PreNorms PP)) = ||.(( partdiff (f,y1,i)) - ( partdiff (f,y0,i))).|| by LOPBAN_1: 30;

              (( proj (i,m)) . t) in REAL by XREAL_0:def 1;

              then <*(( proj (i,m)) . t)*> in ( REAL 1) by FINSEQ_2: 98;

              then

              reconsider pt = <*(( proj (i,m)) . t)*> as VECTOR of ( REAL-NS 1) by REAL_NS1:def 4;



               A44: (PP . pt) = (P1 - P0) by LOPBAN_1: 40;

              (( proj (i,m)) . t) in REAL by XREAL_0:def 1;

              then

              reconsider pt1 = <*(( proj (i,m)) . t)*> as Element of ( REAL 1) by FINSEQ_2: 98;

              reconsider p2 = ((( proj (i,m)) . t) ^2 ) as Real;



               A45: ||.pt.|| = |.pt1.| by REAL_NS1: 1

              .= ( sqrt ( Sum <*p2*>)) by RVSUM_1: 55

              .= ( sqrt ((( proj (i,m)) . t) ^2 )) by RVSUM_1: 73;



               A46: ((( proj (i,m)) . t) ^2 ) >= 0

              proof

                per cases ;

                  suppose (( proj (i,m)) . t) = 0 ;

                  hence thesis;

                end;

                  suppose (( proj (i,m)) . t) <> 0 ;

                  hence thesis by SQUARE_1: 12;

                end;

              end;

              now

                assume ||.pt.|| > 1;

                then ((( proj (i,m)) . t) ^2 ) > 1 by A45, A46, SQUARE_1: 18, SQUARE_1: 26;

                then

                 A47: ((tt . i) ^2 ) > 1 by PDIFF_1:def 1;

                 |.tt.| <= 1 by A14, REAL_NS1: 1;

                then

                 A48: ( Sum ( sqr tt)) <= 1 by SQUARE_1: 18, SQUARE_1: 27;

                ( len tt) = m by CARD_1:def 7;

                then i in ( dom tt) by A32, FINSEQ_1:def 3;

                then

                 A49: i in ( dom ( sqr tt)) by RVSUM_1: 143;

                now

                  let k be Element of NAT ;

                  assume k in ( dom ( sqr tt));



                   A50: (( sqr tt) . k) = ((tt . k) ^2 ) by VALUED_1: 11;

                  per cases ;

                    suppose (tt . k) = 0 ;

                    hence (( sqr tt) . k) >= 0 by A50;

                  end;

                    suppose (tt . k) <> 0 ;

                    hence (( sqr tt) . k) >= 0 by A50, SQUARE_1: 12;

                  end;

                end;

                then ( Sum ( sqr tt)) >= (( sqr tt) . i) by A49, POLYNOM5: 4;

                then ( Sum ( sqr tt)) >= ((tt . i) ^2 ) by VALUED_1: 11;

                hence contradiction by A47, A48, XXREAL_0: 2;

              end;

              then ||.(PP . pt).|| in ( PreNorms PP) & ( PreNorms PP) is non empty bounded_above by LOPBAN_1: 27;

              then ||.(PP . pt).|| <= ( upper_bound ( PreNorms PP)) by SEQ_4:def 1;

              then ||.(P1 - P0).|| <= (r / (2 * m)) by A44, A42, A43, XXREAL_0: 2;

              then |.v.| <= (r / (2 * m)) by A34, A40, REAL_NS1: 1;

              hence (ys . i) <= (rs . i) by A34, A26, A35;

            end;

            then ( Sum ys) <= (r / 2) by A31, A26, A22, INTEGRA5: 3;

            hence mt <= (r / 2) by A21, A25, XXREAL_0: 2;

          end;

          then

           A51: ||.(( diff (f,y1)) - ( diff (f,y0))).|| <= (r / 2) & (r / 2) < r by A13, A7, SEQ_4: 45, XREAL_1: 216;

           ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| = ||.(( diff (f,y1)) - ((f `| X) /. y0)).|| by A5, A12, NDIFF_1:def 9

          .= ||.(( diff (f,y1)) - ( diff (f,y0))).|| by A5, A7, NDIFF_1:def 9;

          hence ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A51, XXREAL_0: 2;

        end;

        hence (f `| X) is_continuous_on X by A6, NFCONT_1: 19;

      end;

      assume

       A52: f is_differentiable_on X & (f `| X) is_continuous_on X;

      then

       A53: X c= ( dom f) & for x be Point of ( REAL-NS m) st x in X holds f is_differentiable_in x by A1, NDIFF_1: 31;

      thus for i be Nat st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X

      proof

        let i be Nat;

        assume

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

        now

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

          assume x in X;

          then f is_differentiable_in x by A52, A1, NDIFF_1: 31;

          hence f is_partial_differentiable_in (x,i) & ( partdiff (f,x,i)) = (( diff (f,x)) * ( reproj (i,( 0. ( REAL-NS m))))) by A54, Th21;

        end;

        then for x be Point of ( REAL-NS m) st x in X holds f is_partial_differentiable_in (x,i);

        hence

         A55: f is_partial_differentiable_on (X,i) by A1, A54, Th8, A53;

        then

         A56: ( dom (f `partial| (X,i))) = X by PDIFF_1:def 20;

        for y0 be Point of ( REAL-NS m), r be Real st y0 in X & 0 < r holds ex s be Real st 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r

        proof

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

          assume

           A57: y0 in X & 0 < r;

          then

          consider s be Real such that

           A58: 0 < s & for y1 be Point of ( REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A52, NFCONT_1: 19;

          take s;

          thus 0 < s by A58;

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

          assume

           A59: y1 in X & ||.(y1 - y0).|| < s;

          then ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A58;

          then ||.(( diff (f,y1)) - ((f `| X) /. y0)).|| < r by A59, A52, NDIFF_1:def 9;

          then

           A60: ||.(( diff (f,y1)) - ( diff (f,y0))).|| < r by A57, A52, NDIFF_1:def 9;

          f is_differentiable_in y1 & f is_differentiable_in y0 by A52, A1, A59, A57, NDIFF_1: 31;

          then

           A61: ( partdiff (f,y1,i)) = (( diff (f,y1)) * ( reproj (i,( 0. ( REAL-NS m))))) & ( partdiff (f,y0,i)) = (( diff (f,y0)) * ( reproj (i,( 0. ( REAL-NS m))))) by Th21, A54;

          reconsider PP = (( partdiff (f,y1,i)) - ( partdiff (f,y0,i))) as Lipschitzian LinearOperator of ( REAL-NS 1), ( REAL-NS 1) by LOPBAN_1:def 9;

          reconsider DD = (( diff (f,y1)) - ( diff (f,y0))) as Lipschitzian LinearOperator of ( REAL-NS m), ( REAL-NS 1) by LOPBAN_1:def 9;



           A62: ( upper_bound ( PreNorms PP)) = ||.(( partdiff (f,y1,i)) - ( partdiff (f,y0,i))).|| by LOPBAN_1: 30;



           A63: ( upper_bound ( PreNorms DD)) = ||.(( diff (f,y1)) - ( diff (f,y0))).|| by LOPBAN_1: 30;



           A64: ( PreNorms PP) is bounded_above & ( PreNorms DD) is bounded_above by LOPBAN_1: 28;

          ( PreNorms PP) c= ( PreNorms DD)

          proof

            let a be object;

            assume a in ( PreNorms PP);

            then

            consider t be VECTOR of ( REAL-NS 1) such that

             A65: a = ||.(PP . t).|| & ||.t.|| <= 1;



             A66: ( dom ( reproj (i,( 0. ( REAL-NS m))))) = the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

            set tm = (( reproj (i,( 0. ( REAL-NS m)))) . t);



             A67: ||.tm.|| <= 1 by A65, Th5, A54;



             A68: (( partdiff (f,y1,i)) . t) = (( diff (f,y1)) . tm) by A66, A61, FUNCT_1: 13;

            (( partdiff (f,y0,i)) . t) = (( diff (f,y0)) . tm) by A66, A61, FUNCT_1: 13;



            then ||.(PP . t).|| = ||.((( diff (f,y1)) . tm) - (( diff (f,y0)) . tm)).|| by A68, LOPBAN_1: 40

            .= ||.(DD . tm).|| by LOPBAN_1: 40;

            hence a in ( PreNorms DD) by A65, A67;

          end;

          then ||.(( partdiff (f,y1,i)) - ( partdiff (f,y0,i))).|| <= ||.(( diff (f,y1)) - ( diff (f,y0))).|| by A64, A62, A63, SEQ_4: 48;

          then ||.(( partdiff (f,y1,i)) - ( partdiff (f,y0,i))).|| < r by A60, XXREAL_0: 2;

          then ||.(( partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r by A57, A55, PDIFF_1:def 20;

          hence ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by A59, A55, PDIFF_1:def 20;

        end;

        hence (f `partial| (X,i)) is_continuous_on X by A56, NFCONT_1: 19;

      end;

    end;