:: Differentiable Functions on Normed Linear Spaces
::  by Yasunari Shidama
::
:: Received June 2, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
      FUNCT_4, NAT_1, FDIFF_1, SUBSET_1, SEQ_4, RELAT_1, GLIB_000, LOPBAN_1,
      ORDINAL4, RFINSEQ, RCOMP_1, TARSKI, SEQ_1, ARYTM_3, VALUED_1, FUNCT_2,
      ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, COMPLEX1, STRUCT_0, CARD_1,
      VALUED_0, XXREAL_0, GROUP_2, FUNCOP_1, XREAL_0, ORDINAL1, MEMBERED,
      FINSEQ_5, XXREAL_2, XBOOLE_0, CARD_3, FINSEQ_1, FINSEQ_2, AFINSQ_1,
      RLVECT_1, SQUARE_1, RVSUM_1, XXREAL_1, PDIFF_1, PRVECT_1, PRVECT_2,
      ALGSTR_0, EUCLID, CFCONT_1, RFINSEQ2, NORMSP_0, NFCONT_1, MONOID_0,
      RLTOPSP1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
      PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, NUMBERS, XXREAL_0, XREAL_0,
      REAL_1, SQUARE_1, NAT_1, MEMBERED, VALUED_0, COMPLEX1, NAT_D, BINOP_2,
      XXREAL_2, CARD_3, FINSEQ_1, VALUED_1, FINSEQ_2, SEQ_1, SEQ_2, RVSUM_1,
      RFINSEQ, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, FINSEQ_5, FINSEQ_7, RFINSEQ2,
      STRUCT_0, MONOID_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1,
      VFUNCT_1, EUCLID, LOPBAN_1, PRVECT_1, NFCONT_1, NDIFF_1, PRVECT_2,
      NFCONT_3, NDIFF_3, RLTOPSP1, FUNCT_7;
 constructors REAL_1, SQUARE_1, SEQ_2, FDIFF_1, NFCONT_1, RSSPACE, VFUNCT_1,
      NDIFF_1, SEQ_1, RELSET_1, FINSEQ_7, FINSEQ_5, RVSUM_1, BINOP_2, PRVECT_2,
      RLVECT_2, NAT_D, FINSEQOP, RFINSEQ, RFINSEQ2, SEQ_4, FCONT_1, NFCONT_3,
      NDIFF_3, MONOID_0, RLTOPSP1, FUNCT_7, COMSEQ_2, FUNCT_4;
 registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, FUNCT_1,
      NDIFF_1, FUNCT_2, NUMBERS, XBOOLE_0, VALUED_0, PRVECT_2, FINSEQ_2,
      FINSEQ_1, CARD_3, NORMSP_0, NORMSP_1, RELAT_1, XXREAL_0, LOPBAN_1,
      LOPBAN_2, PRVECT_3, FUNCOP_1, NAT_1, FINSEQ_5, XXREAL_2, RCOMP_1,
      VALUED_1, FDIFF_1, NFCONT_3, FINSET_1, XCMPLX_0, PARTFUN1, CARD_1,
      MONOID_0, EUCLID, FUNCT_4;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, FUNCT_2, RLVECT_1, LOPBAN_1, EUCLID, RFINSEQ2, FINSEQ_1,
      FINSEQ_2, STRUCT_0, MONOID_0, ALGSTR_0, NORMSP_0, RCOMP_1, XCMPLX_0,
      PRVECT_2;
 theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1,
      ZFMISC_1, SEQ_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2,
      FUNCT_3, FINSEQ_4, RLVECT_2, FINSEQ_3, ORDINAL1, FINSEQ_1, CARD_3,
      FUNCT_4, SEQ_4, NORMSP_1, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1,
      FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1,
      VALUED_0, VECTSP_1, NORMSP_0, XREAL_0, RCOMP_1, FINSEQ_2, FINSEQ_7,
      RVSUM_1, SQUARE_1, PRVECT_1, PRVECT_2, PDIFF_7, EUCLID, TOPREAL7,
      XXREAL_2, FINSEQ_5, NAT_D, RFINSEQ2, INTEGRA5, FCONT_1, NAT_2, NFCONT_3,
      NDIFF_2, NDIFF_3, CARD_1, ROLLE, XXREAL_1, RLTOPSP1, FUNCT_7;
 schemes FUNCT_2, SEQ_1, FINSEQ_1, NAT_1, FINSEQ_2;

begin :: Preliminaries

 reserve j for set;
 reserve p,r for Real;
 reserve S,T,F for non trivial RealNormSpace;
 reserve x0 for Point of S;
 reserve g for PartFunc of S,T;
 reserve c for constant sequence of S;
 reserve R for RestFunc of S,T;
 reserve G for RealNormSpace-Sequence;
 reserve i for Element of dom G;
 reserve f for PartFunc of product G,F;
 reserve x for Element of product G;

theorem Th1:
for R be Function of REAL,S
  holds R is RestFunc-like
   iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
         st z <> 0 & |. z .| < d holds |.z.|"* ||. R/.z .|| < r
proof
   let R be Function of REAL,S;
A1:dom R = REAL by PARTFUN1:def 2;
A2:now assume
A3:  R is RestFunc-like;
    assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
       st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r); then
    consider r be Real such that
A4:  r > 0 and
A5:  for d be Real st d > 0 holds ex z be Real st z <> 0 & |. z .| < d
       & not |. z .|"* ||. R/.z .|| < r;
    defpred P[Element of NAT,Real] means
      $2 <> 0 & |. $2 .| < (1/($1+1)) & not |. $2 .|"* ||. R/.$2 .|| < r;
A6: for n be Element of NAT ex z be Real st P[n,z]
    proof
     let n be Element of NAT;
     1/(n + 1) is Real by XREAL_0:def 1;
     hence thesis by A5;
    end;
    consider s be Real_Sequence such that
A7:  for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6);
A8: now let p be real number;
     assume A9: 0<p;
     consider n be Element of NAT such that
A10:  p"<n by SEQ_4:3;
     reconsider q0=0, q1=1 as real number;
     p" + q0 < n + q1 by A10,XREAL_1:8; then
A11: 1/(n+1) < 1/p" by A9,XREAL_1:76;
     take n;
     let m be Element of NAT;
     assume n<=m; then
     n + 1 <= m + 1 by XREAL_1:6; then
     1/(m+1) <= 1/(n+1) by XREAL_1:118; then
     |. s.m - 0 .| < 1/(n+1) by A7,XXREAL_0:2;
     hence |. s.m - 0 .| <p by A11,XXREAL_0:2;
    end; then
A12:s is convergent by SEQ_2:def 6; then
A13:lim s = 0 by A8,SEQ_2:def 7;
    s is non-zero by A7,SEQ_1:5; then
    reconsider s as 0-convergent non-zero Real_Sequence
    by A12,A13,FDIFF_1:def 1;
    (s")(#)(R/*s) is convergent & lim( (s")(#)(R/*s) ) = 0.S
        by A3,NDIFF_3:def 1; then
    consider n0 be Element of NAT such that
A14:  for m be Element of NAT st n0 <=m
       holds ||. ((s")(#)(R/*s)).m - 0.S .|| < r by A4,NORMSP_1:def 7;
A15: ||. ((s")(#)(R/*s)).n0- 0.S .|| < r by A14;
A16: ||.(s.n0)"*(R/.(s.n0)).||
         = abs((s.n0)") * ||. R/.(s.n0) .|| by NORMSP_1:def 1
        .=|. s.n0 .|" * ||. R/.(s.n0) .|| by COMPLEX1:66;
A17:rng s c= dom R by A1;
    ||. ((s")(#)(R/*s)).n0 - 0.S .||
      = ||. ((s")(#)(R/*s)).n0 .|| by RLVECT_1:13
     .= ||. (s".n0)*((R/*s).n0) .|| by NDIFF_1:def 2
     .= ||. (s.n0)"*((R/*s).n0) .|| by VALUED_1:10
     .= ||. (s.n0)"*(R/.(s.n0)) .|| by A17,FUNCT_2:109;
    hence
     for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st
       z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r by A7,A15,A16;
   end;
   now assume
A18:for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
     st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r;
    now let s be 0-convergent non-zero Real_Sequence;
A19: s is convergent & lim s = 0;
A20: now let r be Real;
      assume r > 0; then
      consider d be Real such that
A21:   d > 0 and
A22:   for z be Real st z <> 0 & |.z.| < d
          holds |.z.|"* ||. R/.z .|| < r by A18;
      consider n0 be Element of NAT such that
A23:   for m be Element of NAT st n0 <=m
             holds |. s.m-0 .| < d by A19,A21,SEQ_2:def 7;
      take n0;
      thus for m be Element of NAT st n0 <=m
           holds ||. ((s")(#)(R/*s)).m- 0.S .|| < r
      proof
A24:   rng s c= dom R by A1;
       let m be Element of NAT;
       assume n0 <=m; then
A25:   |. s.m-0 .| < d by A23;
A26:   s.m <> 0 by SEQ_1:5;
       |. s.m .|" * ||. R/.(s.m) .||
         = abs((s.m)") * ||. R/.(s.m) .|| by COMPLEX1:66
        .= ||. (s.m)"*(R/.(s.m)) .|| by NORMSP_1:def 1
        .= ||. (s.m)"*((R/*s).m) .|| by A24,FUNCT_2:109
        .= ||. (s".m)*((R/*s).m) .|| by VALUED_1:10
        .= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2
        .= ||. ((s")(#)(R/*s)).m- 0.S .|| by RLVECT_1:13;
       hence thesis by A22,A25,A26;
      end;
     end;
     hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6;
     hence lim ((s")(#)(R/*s)) = 0.S by A20,NORMSP_1:def 7;
    end;
    hence R is RestFunc-like by NDIFF_3:def 1;
   end;
   hence thesis by A2;
end;

theorem Th2:
  for R be RestFunc of S st R/.0=0.S
  for e be Real st e > 0 ex d be Real st
    d > 0 & for h be Real st |.h.| < d holds ||.R/.h.|| <= e*|.h.|
proof
   let R be RestFunc of S such that
A1:  R/.0=0.S;
   let e be Real such that
A2:  e > 0;
   R is total by NDIFF_3:def 1; then
   consider d be Real such that
A3:  d > 0 and
A4:  for z be Real st z <> 0 & |.z.| < d
       holds |.z.|"* ||. R/.z .|| < e by A2,Th1;
   take d;
   now let h be Real such that
A5: |.h.| < d;
A6: 0 <= |.h.| by COMPLEX1:46;
    per cases;
    suppose A7: h <> 0; then
     |.h.|"*||. R/.h .|| <= e by A4,A5; then
     |.h.|*(|.h.|"*||. R/.h .||) <= |.h.|*e by A6,XREAL_1:64; then
A8:  |.h.|*|.h.|"*||. R/.h .|| <= e * |.h.|;
     |.h.| <> 0 by A7,COMPLEX1:45; then
     1*||. R/.h .|| <= e * |.h.| by A8,XCMPLX_0:def 7;
     hence ||. R/.h .|| <= e* |.h.|;
    end;
    suppose A9: h = 0;
     reconsider p0=0 as Real;
     p0* |.h.| <= e* |.h.| by A2,A6;
     hence ||. R/.h .|| <= e* |.h.| by A1,A9;
    end;
   end;
   hence thesis by A3;
end;

theorem Th3:
  for R be RestFunc of S
  for L be Lipschitzian LinearOperator of S,T holds
    L*R is RestFunc of T
proof
   let R be RestFunc of S;
   let L be Lipschitzian LinearOperator of S,T;
   consider K be Real such that
A1:  0 <= K and
A2:  for z be Point of S holds ||. L.z .|| <= K * ||.z.|| by LOPBAN_1:def 8;
   dom L = the carrier of S by FUNCT_2:def 1; then
A3:rng R c= dom L;
A4:R is total by NDIFF_3:def 1; then
A5:dom R = REAL by PARTFUN1:def 2;
   now let e be Real such that
A6:  e > 0;
     set e1 = e/2/(1 + K);
     consider d be Real such that
A7:   0 < d and
A8:   for h be Real st h <> 0 & |.h.| < d holds |.h.|"* ||. R/.h .|| < e1
         by A1,A4,A6,Th1;
A9: e/2 < e by A6,XREAL_1:216;
     now let h be Real;
       assume A10: h <> 0 & |.h.| < d; then
       |.h.|"* ||.(R/.h).|| < e1 by A8; then
       (K +1)*(|.h.|"* ||.R/.h.||) <= (K +1)*e1 by A1,XREAL_1:64; then
A11:   (K +1)*(|.h.|"* ||.R/.h.||) <= e/2 by A1,XCMPLX_1:87;
       |.h.| <> 0 by A10,COMPLEX1:45; then
A12:   |.h.| > 0 by COMPLEX1:46;
       reconsider p0=0, p1=1 as Real;
       p0 + K < p1 + K by XREAL_1:8; then
A13:   K * ||.R/.h.|| <= (K +1) * ||.R/.h.|| by XREAL_1:64;
       ||.L.(R/.h).|| <= K * ||.R/.h.|| by A2; then
       ||.L.(R/.h).|| <= (K +1) * ||.R/.h.|| by A13,XXREAL_0:2; then
       |.h.|"* ||.L.(R/.h).|| <= |.h.|"*((K +1)*||. R/.h .||) by A12,XREAL_1:64
; then
A14:   |.h.|"* ||.L.(R/.h).|| <= e/2 by A11,XXREAL_0:2;
       L.(R/.h) = L/.(R/.h); then
       L.(R/.h) =(L*R)/.h by A5,A3,PARTFUN2:5;
       hence |.h.|"* ||.(L*R)/.h.|| < e by A9,A14,XXREAL_0:2;
     end;
     hence ex d be Real st d > 0 & for h be Real st h <> 0 & |.h.| < d
       holds |.h.|"* ||.(L*R)/.h.|| < e by A7;
   end;
   hence thesis by A4,Th1;
end;

theorem Th4:
  for R1 be RestFunc of S st R1/.0 = 0.S
  for R2 be RestFunc of S,T st R2/.(0.S) = 0.T
  for L be LinearFunc of S holds
    R2*(L+R1) is RestFunc of T
proof
   let R1 be RestFunc of S;
   assume R1/.0 = 0.S; then
   consider d0 be Real such that
A1:  0 < d0 and
A2:  for h be Real st |.h.| < d0 holds ||.R1/.h.|| <= 1* |.h.| by Th2;
   let R2 be RestFunc of S,T such that
A3:R2/.(0.S) = 0.T;
   let L be LinearFunc of S;
   consider r be Point of S such that
A4:  for h be Real holds L.h = h*r by NDIFF_3:def 2;
   reconsider K = ||.r.|| as Real;
   R2 is total by NDIFF_1:def 5; then
   dom R2 = the carrier of S by PARTFUN1:def 2; then
A5:rng(L+R1) c= dom R2;
   R1 is total by NDIFF_3:def 1; then
   L+R1 is total by VFUNCT_1:32; then
A6:dom(L+R1) = REAL by PARTFUN1:def 2; then
   dom(R2*(L+R1)) = REAL by A5,RELAT_1:27; then
A7:R2*(L+R1) is total by PARTFUN1:def 2;
   now let e be Real such that
A8: e > 0;
A9: e/2 < e by A8,XREAL_1:216;
     set e1 = e/2/(1 + K);
     consider d be Real such that
A10:   0 < d and
A11:   for z be Point of S st ||.z.|| < d
         holds ||.R2/.z.|| <= e1*||.z.|| by A3,A8,NDIFF_2:7;
     set d1 = d/(1 + K);
     set dd1 = min(d0,d1);
A12: dd1 <= d1 & dd1 <= d0 by XXREAL_0:17;
A13: now let h be Real such that
A14:   h <> 0 and
A15:   |.h.| < dd1;
       |.h.| < d0 by A12,A15,XXREAL_0:2; then
A16:   ||.R1/.h.|| <=1* |.h.| by A2;
       reconsider p0=0 as Real;
       L.h = h*r by A4; then
       ||. L.h .|| - K * |.h.| + K * |.h.| <= p0 + K * |.h.|
           by NORMSP_1:def 1; then
       ||.L.h+R1/.h.|| <= ||.L.h.|| + ||.R1/.h.||
        & ||.L.h.|| + ||. R1/.h .|| <= K * |.h.| + 1 * |.h.|
           by A16,NORMSP_1:def 1,XREAL_1:7; then
A17:   ||.L.h+R1/.h.|| <= ( K +1) * |.h.| by XXREAL_0:2; then
A18:   e1 * ||. L.h+R1/.h .|| <= e1*((K +1)*|.h.|) by A8,XREAL_1:64;
       |.h.| < d1 by A12,A15,XXREAL_0:2; then
       (K +1) * |.h.| < (K +1) * d1 by XREAL_1:68; then
       ||. L.h+R1/.h .|| < (K +1) * d1 by A17,XXREAL_0:2; then
       ||. L.h+R1/.h.|| < d by XCMPLX_1:87; then
       ||. R2/.(L.h+R1/.h) .|| <= e1 * ||. L.h+R1/.h .|| by A11; then
A19:   ||. R2/.(L.h+R1/.h) .|| <= e1*((K +1)*|.h.|) by A18,XXREAL_0:2;
A20:   R2/.(L.h+R1/.h) = R2/.(L/.h+R1/.h)
        .=R2/.((L+R1)/.h) by A6,VFUNCT_1:def 1
        .=(R2*(L+R1))/.h by A6,A5,PARTFUN2:5;
A21:   |.h.| <> 0 by A14,COMPLEX1:45; then
       |.h.| > 0 by COMPLEX1:46; then
       |.h.|"* ||.(R2*(L+R1))/.h.|| <= |.h.|"* (e1* (K +1) * |.h.|)
          by A20,A19,XREAL_1:64; then
       |.h.|"* ||. (R2*(L+R1))/.h .|| <= |.h.|*|.h.|"*e1*(K +1); then
       |.h.|"* ||. (R2*(L+R1))/.h .|| <= 1 * e1 * (K +1)
          by A21,XCMPLX_0:def 7; then
       |.h.|"* ||. (R2*(L+R1))/.h .|| <= e/2 by XCMPLX_1:87;
       hence |.h.|"* ||.(R2*(L+R1))/.h.|| < e by A9,XXREAL_0:2;
     end;
     0 < dd1 by A1,A10,XXREAL_0:15;
     hence
       ex dd1 be Real st dd1 > 0 & for h be Real st h <> 0 & |.h.| < dd1
         holds |.h.|"* ||. (R2*(L+R1))/.h .|| < e by A13;
   end;
   hence thesis by A7,Th1;
end;

theorem Th5:
  for R1 be RestFunc of S st R1/.0=0.S
  for R2 be RestFunc of S,T st R2/.(0.S)=0.T
  for L1 be LinearFunc of S
  for L2 be Lipschitzian LinearOperator of S,T holds
    L2*R1 + R2*(L1+R1) is RestFunc of T
proof
   let R1 be RestFunc of S such that
A1:  R1/.0=0.S;
   let R2 be RestFunc of S,T such that
A2:  R2/.(0.S)=0.T;
   let L1 be LinearFunc of S;
   let L2 be Lipschitzian LinearOperator of S,T;
   L2*R1 is RestFunc of T & R2*(L1+R1) is RestFunc of T
   by A1,A2,Th4,Th3;
   hence thesis by NDIFF_3:7;
end;

theorem Th6:
  for x0 be Element of REAL
  for g be PartFunc of REAL,the carrier of S st
    g is_differentiable_in x0
  for f be PartFunc of the carrier of S,the carrier of T st
    f is_differentiable_in (g/.x0) holds
  f*g is_differentiable_in x0 & diff(f*g,x0) = diff(f,g/.x0).diff(g,x0)
proof
   let x0 be Element of REAL;
   let g be PartFunc of REAL,the carrier of S such that
A1:  g is_differentiable_in x0;
   consider N1 being Neighbourhood of x0 such that
A2:  N1 c= dom g and
A3:  ex L1 be LinearFunc of S,R1 be RestFunc of S st
       diff(g,x0) = L1.1
     & for x be Real st x in N1 holds g/.x-g/.x0 = L1.(x-x0) + R1/.(x-x0)
         by A1,NDIFF_3:def 4;
   let f be PartFunc of the carrier of S,the carrier of T;
   assume f is_differentiable_in g/.x0; then
   consider N2 being Neighbourhood of g/.x0 such that
A4:  N2 c= dom f and
A5:  ex R2 be RestFunc of S,T
      st R2/.(0.S) = 0.T
       & R2 is_continuous_in 0.S
       & for y be Point of S st y in N2
           holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0)
       by NDIFF_1:47;
   consider R2 be RestFunc of S,T such that
A6:  R2/.0.S=0.T and
A7:  for y be Point of S st y in N2
       holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by A5;
   reconsider L2 = diff(f,g/.x0) as Lipschitzian LinearOperator of S,T
                                    by LOPBAN_1:def 9;
   consider L1 be LinearFunc of S,R1 be RestFunc of S such that
A8:  diff(g,x0) = L1.1
   & for x be Real st x in N1 holds g/.x-g/.x0 = L1.(x-x0) + R1/.(x-x0) by A3;
   consider r be Point of S such that
A9:  for p be Real holds L1.p = p*r by NDIFF_3:def 2;
   reconsider p0=0 as Element of REAL;
   g/.x0-g/.x0 = L1.(x0-x0) + R1/.(x0-x0) by A8,RCOMP_1:16; then
   0.S = L1.0 + R1/.0 by RLVECT_1:15; then
   0.S = p0*r + R1/.0 by A9; then
   0.S = 0.S + R1/.0 by RLVECT_1:10; then
   R1/.0 = 0.S by RLVECT_1:4; then
   reconsider R0=L2*R1+R2*(L1+R1) as RestFunc of T by A6,Th5;
A10: dom(L2*L1) = REAL by FUNCT_2:def 1;
   reconsider q = L2.r as Point of T;
   now let p be Real;
     L2.(L1.p) = L2.(p*r) by A9; then
     L2.(L1.p) = p*q by LOPBAN_1:def 5;
     hence (L2*L1).p = p*q by A10,FUNCT_1:12;
   end; then
   reconsider L0=L2*L1 as LinearFunc of T by NDIFF_3:def 2;

   g is_continuous_in x0 by A1,NDIFF_3:22; then
   consider N3 be Neighbourhood of x0 such that
A11: g.:N3 c= N2 by NFCONT_3:10;
   consider N be Neighbourhood of x0 such that
A12: N c= N1 and
A13: N c= N3 by RCOMP_1:17;

   now let x be set;
     assume
A14: x in N; then
     reconsider x9 = x as Real;
A15: x in N1 by A12,A14; then
     g.x9 in g.:N3 by A2,A13,A14,FUNCT_1:def 6; then
     g.x9 in N2 by A11;
     hence x in dom(f*g) by A2,A4,A15,FUNCT_1:11;
   end; then
A16: N c= dom(f*g) by TARSKI:def 3;

A17: now let x be Real such that
A18: x in N;
A19: g/.x-g/.x0 = L1.(x-x0) + R1/.(x-x0) by A8,A12,A18;
A20: x in N1 by A12,A18; then
     g.x in g.:N3 by A2,A13,A18,FUNCT_1:def 6; then
     g.x in N2 by A11; then
A21: g/.x in N2 by A2,A20,PARTFUN1:def 6;

A22: x0 in N by RCOMP_1:16;
A23: R1 is total by NDIFF_3:def 1; then
A24: dom R1 = REAL by PARTFUN1:def 2;
     dom L2 = the carrier of S by FUNCT_2:def 1; then
A25: rng R1 c= dom L2;

A26: dom(L2*R1) = REAL by A23,PARTFUN1:def 2;

     L1+R1 is total by A23,VFUNCT_1:32; then
A27: dom(L1+R1)=REAL by PARTFUN1:def 2;

     R2 is total by NDIFF_1:def 5; then
     dom R2 = the carrier of S by PARTFUN1:def 2; then
A28: rng (L1+R1) c= dom R2; then
     dom (R2*(L1+R1)) = dom(L1+R1) by RELAT_1:27; then
A29: dom (L2*R1+R2*(L1+R1)) = REAL /\ REAL by A26,A27,VFUNCT_1:def 1;

     L2.(R1/.(x-x0)) = L2/.(R1/.(x-x0)); then
A30: L2.(R1/.(x-x0)) =(L2*R1)/.(x-x0) by A24,A25,PARTFUN2:5;

A31: R2/.(L1.(x-x0)+R1/.(x-x0)) = R2/.(L1/.(x-x0)+R1/.(x-x0))
      .=R2/.((L1+R1)/.(x-x0)) by A27,VFUNCT_1:def 1
      .=(R2*(L1+R1))/.(x-x0) by A27,A28,PARTFUN2:5;

A32: (L2*L1).(x-x0) = L2.(L1.(x-x0)) by A10,FUNCT_1:12;

     thus (f*g)/.x-(f*g)/.x0 =f/.(g/.x) -(f*g)/.x0 by A16,A18,PARTFUN2:3
      .=f/.(g/.x) -f/.(g/.x0) by A16,A22,PARTFUN2:3
      .=diff(f,g/.x0).(g/.x-g/.x0) + R2/.(g/.x-g/.x0) by A7,A21
      .=L2.(L1.(x-x0)) + L2.(R1/.(x-x0)) + (R2*(L1+R1))/.(x-x0) by A19,A31,
VECTSP_1:def 20
      .=L2.(L1.(x-x0)) + ((L2*R1)/.(x-x0) + (R2*(L1+R1))/.(x-x0)) by A30,
RLVECT_1:def 3
      .=L0.(x-x0) + R0/.(x-x0) by A32,A29,VFUNCT_1:def 1;
   end;
   hence A33: f*g is_differentiable_in x0 by A16,NDIFF_3:def 3;
   (L2*L1).1 = diff(f,g/.x0).diff(g,x0) by A8,A10,FUNCT_1:12;
   hence thesis by A33,A16,A17,NDIFF_3:def 4;
end;

theorem Th7:
for S be RealNormSpace,
    xseq be FinSequence of S,
    yseq be FinSequence of REAL st
 len xseq = len yseq &
 ( for i be Element of NAT st i in dom xseq holds
    yseq.i = ||. xseq/.i .|| )
  holds ||.Sum xseq.|| <= Sum yseq
proof
   let S be RealNormSpace,
    xseq be FinSequence of S,
    yseq be FinSequence of REAL;
   assume that
A1: len xseq = len yseq and
A2: for i be Element of NAT st
      i in dom xseq holds yseq.i = ||. xseq/.i .||;

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

A3:P[0]
   proof
    let xseq be FinSequence of S, yseq be FinSequence of REAL;
    assume
A4:  0 = len xseq & len xseq = len yseq
   & ( for i be Element of NAT st i in dom xseq holds
        yseq.i = ||. xseq/.i .|| );
    consider Sx be Function of NAT,the carrier of S such that
A5:  Sum xseq = Sx.(len xseq)
   & Sx.0 = 0.S
   & for j be Element of NAT, v be Element of S st
        j < len xseq & v = xseq.(j+1) holds Sx.(j+1) = Sx.j + v
          by RLVECT_1:def 12;
    yseq = {} by A4;
    hence thesis by A4,A5,RVSUM_1:72;
   end;

A6:now let i be Element of NAT;
    assume A7: P[i];
    now let xseq be FinSequence of S, yseq be FinSequence of REAL;
     set xseq0=xseq|i, yseq0=yseq|i;
     assume
A8:   i+1=len xseq & len xseq = len yseq &
      ( for i be Element of NAT st i in dom xseq holds
          yseq.i = ||. xseq/.i .|| );

A9:  for k be Element of NAT st k in dom xseq0 holds yseq0.k = ||. xseq0/.k .||
     proof
      let k be Element of NAT;
      assume
A10:     k in dom xseq0; then
A11:   k in Seg i & k in dom xseq by RELAT_1:57; then
A12:   yseq.k = ||. xseq/.k .|| by A8;
      xseq/.k = xseq.k by A11,PARTFUN1:def 6; then
      xseq/.k = xseq0.k by A11,FUNCT_1:49; then
      xseq/.k = xseq0/.k by A10,PARTFUN1:def 6;
      hence thesis by A11,A12,FUNCT_1:49;
     end;

A13:  dom xseq = Seg(i+1) by A8,FINSEQ_1:def 3; then
A14:  yseq.(i+1) = ||. xseq/.(i+1) .|| by A8,FINSEQ_1:4;
A15: 1 <= i + 1 by NAT_1:11;
     yseq = (yseq|i)^<*yseq/.(i+1) *> by A8,FINSEQ_5:21; then
     yseq = yseq0 ^<*(yseq.(i+1))*> by A8,A15,FINSEQ_4:15; then
A16: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74;

A17:  len xseq in dom xseq by A13,A8,FINSEQ_1:4; then
     reconsider v = xseq.(len xseq) as Element of S by PARTFUN1:4;

A18:  v = xseq/.(i+1) by A8,A17,PARTFUN1:def 6;

A19: i=len xseq0 by A8,FINSEQ_1:59,NAT_1:11; then
     xseq0 = xseq| (dom xseq0) by FINSEQ_1:def 3; then
A20: Sum xseq = Sum xseq0 + v by A8,A19,RLVECT_1:38;

A21: ||. Sum xseq0 + v.|| <= ||.Sum xseq0 .|| + ||. v .|| by NORMSP_1:def 1;
     len xseq0 = len yseq0 by A8,A19,FINSEQ_1:59,NAT_1:11; then
     ||. Sum xseq0 .|| <= Sum yseq0 by A7,A9,A19; then
     ||. Sum xseq0 .|| + ||.v.|| <= Sum yseq0 + yseq.(i+1) by A14,A18,XREAL_1:6
;
     hence ||. Sum xseq .|| <= Sum yseq by A16,A20,A21,XXREAL_0:2;
    end;
    hence P[i+1];
   end;
   for i be Element of NAT holds P[i] from NAT_1:sch 1(A3,A6);
   hence thesis by A1,A2;
end;

theorem Th8:
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 is Point of S: ||.y-x .|| < g} c= N by NFCONT_1:def 1;
   {y where y is Point of S: ||.y-x .|| < g} c= N1 /\ N2 by A2,A4,XBOOLE_1:1;
   hence thesis by A3,NFCONT_1:def 1;
end;

theorem Th9:
for X be non-empty FinSequence,
    x be set st x in product X holds x is FinSequence
proof
   let X be non-empty FinSequence, x be set;
   assume x in product X; then
   consider g be Function such that
A1: x = g & dom g = dom X
  & for i be set st i in dom X holds g.i in X.i by CARD_3:def 5;
   dom g = Seg len X by A1,FINSEQ_1:def 3;
   hence x is FinSequence by A1,FINSEQ_1:def 2;
end;

registration
  let G be RealNormSpace-Sequence;
  cluster product G -> constituted-FinSeqs;
  coherence
  proof
    let a be Element of product G;
    product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
    productnorm G #) by PRVECT_2:6;
    hence thesis by Th9;
  end;
end;

Lm1: now let G be RealLinearSpace-Sequence;
  len carr G = len G by PRVECT_2:def 4;
  hence dom carr G = Seg len G by FINSEQ_1:def 3
             .= dom G by FINSEQ_1:def 3;
end;

definition
  let G be RealLinearSpace-Sequence;
  let z be Element of product carr G;
  let j be Element of dom G;
  redefine func z.j -> Element of G.j;
correctness
proof
   reconsider zz=z as FinSequence by Th9;
   dom carr G = dom G by Lm1; then
   zz.j in carr G.j by CARD_3:9;
   hence thesis by PRVECT_2:def 4;
end;
end;

theorem Th10:
  the carrier of product G = product carr G
proof
  product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
  productnorm G #) by PRVECT_2:6;
  hence thesis;
 end;

theorem Th11:
for i be Element of dom G, r be set, x be Function
  st r in the carrier of (G.i) & x in product carr G
holds x +* (i,r) in the carrier of product G
proof
   let i be Element of dom G, r be set, x be Function;
   assume A1: r in the carrier of (G.i) & x in product carr G; then
   consider g be Function such that
A2:   x = g & dom g = dom carr G
    & for i be set st i in dom carr G holds g.i in (carr G).i
        by CARD_3:def 5;
   set h = x +* (i,r);
   set s = i .--> r;
   s = {i} --> r by FUNCOP_1:def 9; then
A3:dom s = {i} by FUNCOP_1:13;
A4:dom h = dom carr G by A2,FUNCT_7:30;
   for j be set st j in dom carr G holds h.j in (carr G).j
   proof
    let j be set;
    assume A5: j in dom carr G;
    per cases;
    suppose not j in dom s; then
     j <> i by A3,TARSKI:def 1; then
     h.j = x.j by FUNCT_7:32;
     hence h.j in (carr G).j by A2,A5;
    end;
    suppose j in dom s; then
A6:  j = i by TARSKI:def 1; then
     h.j = r by A5,A2,FUNCT_7:31;
     hence h.j in (carr G).j by A1,A6,PRVECT_2:def 4;
    end;
   end; then
   x +* (i,r) in product carr G by A4,CARD_3:def 5;
   hence thesis by Th10;
end;

definition
  let G be RealNormSpace-Sequence;
  attr G is non-trivial means :Def1:
  for j be Element of dom G holds G.j is non trivial;
end;

registration
  cluster non-trivial for RealNormSpace-Sequence;
correctness
proof
  take G = <* the non trivial RealNormSpace *>;
  let j be Element of dom G;
  dom G = Seg 1 by FINSEQ_1:38; then
  j = 1 by FINSEQ_1:2,TARSKI:def 1;
  hence thesis by FINSEQ_1:40;
end;
end;

registration
  let G be non-trivial RealNormSpace-Sequence;
  let i be Element of dom G;
  cluster G.i -> non trivial for RealNormSpace;
  correctness by Def1;
end;

registration
  let G be non-trivial RealNormSpace-Sequence;
  cluster product G -> non trivial;
correctness
proof
A1:the carrier of product G = product carr G by Th10;
   not
    for x,y be set st x in product carr G & y in product carr G holds x = y
   proof
    assume
A2:  for x,y be set st x in product carr G & y in product carr G holds x = y;
    consider z be set such that
A3:  z in product carr G by XBOOLE_0:def 1;
    consider g be Function such that
A4:  z = g & dom g = dom carr G
   & for i be set st i in dom carr G holds g.i in (carr G).i
        by A3,CARD_3:def 5;
    set i = the Element of dom G;
    now let r,s be set;
     assume A5: r in the carrier of (G.i) & s in the carrier of (G.i);
     g +* (i,r) in the carrier of product G &
     g +* (i,s) in the carrier of product G by Th11,A3,A4,A5; then
     g +* (i,r) in product carr G &
     g +* (i,s) in product carr G by Th10; then
A6:  g +* (i,r) = g +* (i,s) by A2;
     i in dom G; then
A7:  i in dom g by A4,Lm1; then
     (g +* (i,r)).i = r by FUNCT_7:31;
     hence r=s by A6,A7,FUNCT_7:31;
    end;
    hence contradiction by ZFMISC_1:def 10;
   end;
   hence thesis by A1,ZFMISC_1:def 10;
end;
end;

theorem Th12:
for G be RealNormSpace-Sequence, p,q be Point of product G,
    r0,p0,q0 be Element of product carr G st p=p0 & q=q0
holds p+q = r0
  iff for i be Element of dom G holds r0.i = p0.i + q0.i
proof
   let G be RealNormSpace-Sequence, p,q be Point of product G,
       r0,p0,q0 be Element of product carr G;
   assume A1: p=p0 & q=q0;
   len carr G = len G by PRVECT_2:def 4; then
A2:dom carr G = Seg len G by FINSEQ_1:def 3
             .= dom G by FINSEQ_1:def 3;
A3: product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
    productnorm G #) by PRVECT_2:6;
   hereby assume A4: p+q = r0;
    hereby let i be Element of dom G;
     reconsider i0=i as Element of dom carr G by A2;
     (addop G).i0 = the addF of (G.i0) by PRVECT_2:def 5;
     hence r0.i = p0.i + q0.i by A1,A4,A3,PRVECT_1:def 8;
    end;
   end;
   assume A5: for i be Element of dom G holds r0.i = p0.i + q0.i;
   reconsider pq=p+q as Element of product carr G by Th10;
A6:ex g be Function st
     pq = g & dom g = dom carr G
   & for i be set st i in dom carr G holds g.i in (carr G).i
         by CARD_3:def 5;
A7:ex g be Function st
     r0 = g & dom g = dom carr G
   & for i be set st i in dom carr G holds g.i in (carr G).i
         by CARD_3:def 5;
   now let i0 be set;
    assume A8: i0 in dom pq; then
    reconsider i1=i0 as Element of dom G by A2,A6;
    reconsider i =i0 as Element of dom carr G by A8,A6;
    (addop G).i = the addF of (G.i) by PRVECT_2:def 5; then
    pq.i0 = p0.i1 + q0.i1 by A1,A3,PRVECT_1:def 8;
    hence pq.i0 = r0.i0 by A5;
   end;
   hence p+q = r0 by A6,A7,FUNCT_1:2;
end;

theorem Th13:
for G be RealNormSpace-Sequence, p be Point of product G,
    r be Real, r0,p0 be Element of product carr G
  st p=p0
holds r*p = r0
  iff for i be Element of dom G holds r0.i = r*(p0.i)
proof
   let G be RealNormSpace-Sequence, p be Point of product G,
       r be Real, r0,p0 be Element of product carr G;
   assume A1: p=p0;
   hereby assume A2: r*p = r0;
    hereby let i be Element of dom G;
     reconsider i0=i as Element of dom carr G by Lm1;
A3:  (multop G).i0 = the Mult of (G.i0) by PRVECT_2:def 8;
     product G = NORMSTR(# product carr G,zeros G,[:addop G:],
       [:multop G:], productnorm G #) by PRVECT_2:6;
     hence r0.i = r*(p0.i) by A1,A2,A3,PRVECT_2:def 2;
    end;
   end;
   assume A4: for i be Element of dom G holds r0.i = r* (p0.i);
   reconsider rp = r*p as Element of product carr G by Th10;
A5:ex g be Function st
      rp = g & dom g = dom carr G
    & for i be set st i in dom carr G holds g.i in (carr G).i
           by CARD_3:def 5;
A6:ex g be Function st
      r0 = g & dom g = dom carr G
    & for i be set st i in dom carr G holds g.i in (carr G).i
           by CARD_3:def 5;
   now let i0 be set;
    assume A7: i0 in dom rp; then
    reconsider i1=i0 as Element of dom G by Lm1,A5;
    reconsider i=i0 as Element of dom carr G by A7,A5;
A8: product G = NORMSTR(# product carr G,zeros G,[:addop G:],
        [:multop G:], productnorm G #) by PRVECT_2:6;
    (multop G).i = the Mult of (G.i) by PRVECT_2:def 8; then
    rp.i0 = r*(p0.i1) by A1,A8,PRVECT_2:def 2;
    hence rp.i0 = r0.i0 by A4;
   end;
   hence r*p = r0 by A5,A6,FUNCT_1:2;
end;

theorem Th14:
for G be RealNormSpace-Sequence, p0 be Element of product carr G
holds 0.(product G)=p0
  iff for i be Element of dom G holds p0.i = 0.(G.i)
proof
   let G be RealNormSpace-Sequence,
       p0 be Element of product carr G;
A1:dom carr G = dom G by Lm1;
A2:product G = NORMSTR(# product carr G,zeros G,[:addop G:]
               ,[:multop G:], productnorm G #) by PRVECT_2:6;
   hence 0.(product G) = p0 implies
    for i be Element of dom G holds p0.i = 0.(G.i) by A1,PRVECT_2:def 7;
   assume A3:for i be Element of dom G holds p0.i = 0.(G.i);
   now let i0 be Element of dom carr G;
    reconsider i=i0 as Element of dom G by Lm1;
    p0.i0 = 0.(G.i) by A3;
    hence p0.i0 = the ZeroF of (G.i0);
   end;
   hence 0.(product G)=p0 by A2,PRVECT_2:def 7;
end;

theorem Th15:
for G be RealNormSpace-Sequence, p,q be Point of product G,
    r0,p0,q0 be Element of product carr G
  st p=p0 & q=q0
holds p-q = r0
  iff for i be Element of dom G holds r0.i = p0.i - q0.i
proof
   let G be RealNormSpace-Sequence, p,q be Point of product G,
       r0,p0,q0 be Element of product carr G;
   assume A1: p=p0 & q=q0;
   reconsider qq0=(-1)*q as Element of product carr G by Th10;
A2:p-q = p+(-1)*q by RLVECT_1:16;
   hereby assume A3: p-q = r0;
    thus for i be Element of dom G holds r0.i = p0.i - q0.i
    proof
     let i be Element of dom G;
A4:  r0.i = p0.i + qq0.i by Th12,A3,A1,A2;
     -1 is Real by XREAL_0:def 1; then
     qq0.i = (-1)*(q0.i) by A1,Th13;
     hence thesis by A4,RLVECT_1:16;
    end;
   end;
   assume A5: for i be Element of dom G holds r0.i = p0.i - q0.i;
   now let i be Element of dom G;
    -1 is Real by XREAL_0:def 1; then
A6: qq0.i = (-1)*(q0.i) by A1,Th13;
    r0.i = p0.i - q0.i by A5;
    hence r0.i = p0.i +  qq0.i by A6,RLVECT_1:16;
   end;
   hence p-q = r0 by A2,Th12,A1;
end;

begin :: Mean value theorem for vector-valued functions

definition
  let S be RealLinearSpace;
  let p,q be Point of S;
  func ]. p,q .[ -> Subset of S equals
    { p+t*(q-p) where t is Real : 0 < t & t < 1};
correctness
proof
   now let x be set;
    assume x in { p+t*(q-p) where t is Real : 0 < t & t < 1}; then
    ex t be Real st x=p+t*(q-p) & 0 < t & t < 1;
    hence x in the carrier of S;
   end;
   hence thesis by TARSKI:def 3;
end;
end;

notation
  let S be RealLinearSpace;
  let p,q be Point of S;
  synonym [.p,q.] for LSeg(p,q);
end;

Lm2: now let S be RealLinearSpace; let p,q be Point of S; let z1 be Real;
  thus p+z1*(q-p) = p+(z1*q + (z1*(-p))) by RLVECT_1:def 5
     .= p+(z1*q+- z1*p) by RLVECT_1:25
     .= p+-z1*p+z1*q by RLVECT_1:def 3
     .= 1*p-z1*p + z1*q by RLVECT_1:def 8
     .= (1-z1)*p + z1*q by RLVECT_1:35;
  end;

theorem Th16:
for S be RealLinearSpace, p,q be Point of S
  holds ].p,q.[ c= [. p,q .]
proof
   let S be RealLinearSpace, p,q be Point of S;
   now let z be set;
    assume z in ].p,q.[; then
    consider z1 be Real such that
A1: z=p+z1*(q-p) & 0 < z1 & z1 < 1;
    z = (1-z1)*p + z1*q by A1,Lm2; then
    z in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1 } by A1;
    hence z in [. p,q .] by RLTOPSP1:def 2;
   end;
   hence ].p,q.[ c= [. p,q .] by TARSKI:def 3;
end;

Lm3:
 for x be Real st for e be Real st 0 < e holds x <= e holds x <= 0
proof
   let x be Real;
   assume A1: for e be Real st 0 < e holds x <= e;
   assume A2: not x <= 0; then
   x <= x/2 by A1; then
   x - (x/2) <= (x/2) - (x/2) by XREAL_1:9;
   hence contradiction by A2;
end;

theorem Th17:
  for T be non trivial RealNormSpace, R be PartFunc of REAL,T
   st R is total holds
     R is RestFunc-like
  iff for r be Real st r > 0
      ex d be Real st d > 0 & for z be Real
        st z <> 0 & abs z < d holds ( ||. R/.z .||/ abs z ) < r
proof
   let T be non trivial RealNormSpace, R be PartFunc of REAL,T;
   assume A1: R is total;
A2:now assume A3: R is RestFunc-like;
    assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
    st z <> 0 & abs z < d holds ( ||. R/.z .||/ abs z) < r ); then
    consider r be Real such that
A4:  r > 0 and
A5:  for d be Real st d > 0 holds ex z be Real st z <> 0 & abs z < d
      & not (  ||. R/.z .||/ abs z ) < r;
    defpred P[Element of NAT,Element of REAL]
      means $2 <> 0 & abs($2) < (1/($1+1))
     & not ( (||. R/.$2 .||/abs($2) ) < r );
A6: now let n be Element of NAT;
     1/(n + 1) is Real by XREAL_0:def 1;
     hence ex z be Element of REAL st P[n,z] by A5;
    end;
    consider s be Real_Sequence such that
A7:   for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6);
A8: now let p be real number;
     assume A9: 0<p;
     consider n be Element of NAT such that
A10:  p"<n by SEQ_4:3;
     p" + (0 qua Real) < n + 1 by A10,XREAL_1:8; then
A11: 1/(n+1) < 1/p" by A9,XREAL_1:76;
     take n;
     let m be Element of NAT;
     assume n<=m; then
     n + 1 <= m + 1 by XREAL_1:6; then
     1/(m+1) <= 1/(n+1) by XREAL_1:118; then
     abs(s.m - 0) < 1/(n+1) by A7,XXREAL_0:2;
     hence abs(s.m - 0) <p by A11,XXREAL_0:2;
    end; then
A12:s is convergent by SEQ_2:def 6; then
A13:lim s = 0 by A8,SEQ_2:def 7;
    s is non-zero by A7,SEQ_1:5; then
    reconsider s as 0-convergent non-zero Real_Sequence
    by A12,A13,FDIFF_1:def 1;
    (s")(#)(R/*s) is convergent & lim ((s")(#)(R/*s)) = 0.T
      by A3,NDIFF_3:def 1; then
    consider n be Element of NAT such that
A14: for m be Element of NAT st n <=m
       holds ||. ((s")(#)(R/*s)).m - 0.T .|| < r by A4,NORMSP_1:def 7;
A15: ||. ((s")(#)(R/*s)).n- 0.T.|| < r by A14;
A16: ||.(s.n)"*(R/.(s.n)).||
       = abs((s.n)") * ||. R/.(s.n) .|| by NORMSP_1:def 1
      .= ||. R/.(s.n) .||/abs(s.n) by COMPLEX1:66;
    dom R = REAL by A1,PARTFUN1:def 2; then
A17:rng s c= dom R;
    ||. ((s")(#)(R/*s)).n- 0.T.||
       = ||. ((s")(#)(R/*s)).n .|| by RLVECT_1:13
      .= ||. (s".n)*((R/*s).n) .|| by NDIFF_1:def 2
      .= ||. (s.n)"*((R/*s).n) .|| by VALUED_1:10
      .= ||. (s.n)"*(R/.(s.n)) .|| by A17,FUNCT_2:109;
    hence
      for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st
         z <> 0 & abs z < d holds ( ||. R/.z .||/abs z ) < r by A7,A15,A16;
   end;

   now assume
A18: for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
    st z <> 0 & abs(z) < d holds ( ||. R/.z .||/abs z) < r;
    now let s be 0-convergent non-zero Real_Sequence;
A19: s is convergent & lim s = 0;
A20: now let r be Real;
      assume r > 0; then
      consider d be Real such that
A21:   d > 0 and
A22:   for z be Real st z <> 0 & abs z < d holds
          ( ||. R/.z .||/abs z) < r by A18;
      consider n be Element of NAT such that
A23:   for m be Element of NAT st n <=m holds abs(s.m-0) < d
         by A19,A21,SEQ_2:def 7;
      take n;
      thus for m be Element of NAT st n <=m
        holds ||. ((s")(#)(R/*s)).m- 0.T.|| < r
      proof
       dom R = REAL by A1,PARTFUN1:def 2; then
A24:   rng s c= dom R;
       let m be Element of NAT;
       assume n <=m; then
A25:   abs(s.m-0) < d by A23;
A26:   s.m <> 0 by SEQ_1:5;
       ||.(R/.(s.m)).|| / abs(s.m)
          = abs((s.m)") * ||.(R/.(s.m)).|| by COMPLEX1:66
         .= ||.(s.m)"*(R/.(s.m)).|| by NORMSP_1:def 1
         .= ||.(s.m)"*((R/*s).m).|| by A24,FUNCT_2:109
         .= ||.(s".m)*((R/*s).m).|| by VALUED_1:10
         .= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2
         .= ||. ((s")(#)(R/*s)).m- 0.T.|| by RLVECT_1:13;
       hence thesis by A22,A25,A26;
      end;
     end;
     hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6;
     hence lim ((s")(#)(R/*s)) = 0.T by A20,NORMSP_1:def 7;
    end;
    hence R is RestFunc-like by A1,NDIFF_3:def 1;
   end;
   hence thesis by A2;
end;

theorem Th18:
  for R be Function of REAL,REAL holds R is RestFunc-like iff
  for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
     st z <> 0 & abs(z) < d holds (abs(R.z)/ abs(z)) < r
proof
  let R be Function of REAL,REAL;
A1:now assume
A2: R is RestFunc-like;
    assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
    st z <> 0 & abs z < d holds ( abs(R.z)/ abs z ) < r); then
    consider r be Real such that
A3:  r > 0 and
A4:  for d be Real st d > 0 holds ex z be Real st z <> 0 & abs z < d
    & not ( abs(R.z)/abs z) < r;
    defpred P[Element of NAT,Element of REAL]
     means $2 <> 0 & abs $2 < 1/($1+1) & not (abs(R.$2)/abs $2) < r;

A5: now let n be Element of NAT;
     1/(n + 1) is Real by XREAL_0:def 1;
     hence ex z be Element of REAL st P[n,z] by A4;
    end;
    consider s be Real_Sequence such that
A6:  for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A5);
A7: now let p be real number;
     assume
A8:   0<p;
     consider n be Element of NAT such that
A9:  p"<n by SEQ_4:3;
     p" + (0 qua Real) < n + 1 by A9,XREAL_1:8; then
A10: 1/(n+1) < 1/p" by A8,XREAL_1:76;
     take n;
     let m be Element of NAT;
     assume n<=m; then
     n + 1 <= m + 1 by XREAL_1:6; then
     1/(m+1) <= 1/(n+1) by XREAL_1:118; then
     abs(s.m - 0) < 1/(n+1) by A6,XXREAL_0:2;
     hence abs(s.m - 0) < p by A10,XXREAL_0:2;
    end; then
A11:s is convergent by SEQ_2:def 6; then
A12:lim s = 0 by A7,SEQ_2:def 7;
    s is non-zero by A6,SEQ_1:5; then
    reconsider s as 0-convergent non-zero Real_Sequence
    by A11,A12,FDIFF_1:def 1;
    (s")(#)(R/*s) is convergent & lim ((s")(#)(R/*s)) = 0
      by A2,FDIFF_1:def 2; then
    consider n be Element of NAT such that
A13: for m be Element of NAT st n <=m holds abs( ((s")(#)(R/*s)).m- 0 ) < r
      by A3,SEQ_2:def 7;
A14:abs( ((s")(#)(R/*s)).n - 0 ) < r by A13;
A15:abs( (s.n)"*(R.(s.n)) ) = abs((s.n)") * abs(R.(s.n)) by COMPLEX1:65
      .= abs(R.(s.n))/abs(s.n) by COMPLEX1:66;
    abs( ((s")(#)(R/*s)).n- 0 )
      = abs( (s".n)*((R/*s).n) ) by SEQ_1:8
      .= abs( (s.n)"*((R/*s).n) ) by VALUED_1:10
      .= abs( (s.n)"*(R.(s.n)) ) by FUNCT_2:115;
    hence
     for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st
      z <> 0 & abs z < d holds ( abs(R.z)/abs z ) < r by A6,A14,A15;
   end;
   now assume
A16: for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
    st z <> 0 & abs z < d holds ( abs(R.z)/abs z ) < r;
    now let s be 0-convergent non-zero Real_Sequence;
A17: s is convergent & lim s = 0;
A18: now let r be real number;
      assume A19: r > 0;
      r is Real by XREAL_0:def 1; then
      consider d be Real such that
A20:   d > 0 and
A21:   for z be Real st z <> 0 & abs z < d holds abs(R.z)/abs z < r by A19,A16;
      consider n be Element of NAT such that
A22:   for m be Element of NAT st n <= m holds abs(s.m-0) < d
         by A17,A20,SEQ_2:def 7;
      take n;
      hereby let m be Element of NAT;
       assume n <=m; then
A23:   abs(s.m-0) < d by A22;
A24:   s.m <> 0 by SEQ_1:5;
       abs(R.(s.m)) / abs(s.m)
         = abs((s.m)") * abs(R.(s.m)) by COMPLEX1:66
        .= abs((s.m)" * R.(s.m)) by COMPLEX1:65
        .= abs((s.m)" * (R/*s).m) by FUNCT_2:115
        .= abs(s".m * (R/*s).m) by VALUED_1:10
        .= abs((s"(#)(R/*s)).m - 0) by SEQ_1:8;
       hence abs( ((s")(#)(R/*s)).m- 0) < r by A21,A23,A24;
      end;
     end;
     hence (s")(#)(R/*s) is convergent by SEQ_2:def 6;
     hence lim((s")(#)(R/*s)) = 0 by A18,SEQ_2:def 7;
    end;
    hence R is RestFunc-like by FDIFF_1:def 2;
   end;
   hence thesis by A1;
end;

Lm4:
for T be non trivial RealNormSpace,
f be PartFunc of REAL,T,
g be PartFunc of REAL,REAL
  st dom f = [.0,1.] & dom g = [.0,1.]
     & f| [.0,1.] is continuous
     & g| [.0,1.] is continuous
     & f is_differentiable_on ].0,1.[
     & g is_differentiable_on ].0,1.[
     & (for x be real number st x in ].0,1.[ holds
        ||. diff(f,x) .|| <= diff(g,x))
holds
  ||. f/.1 -f/.0 .|| <= g/.1 - g/.0
proof
   let T be non trivial RealNormSpace,
       f be PartFunc of REAL,T,
       g be PartFunc of REAL,REAL;
   assume A1: dom f = [.0,1.] & dom g = [.0,1.]
     & f| [.0,1.] is continuous
     & g| [.0,1.] is continuous
     & f is_differentiable_on ].0,1.[
     & g is_differentiable_on ].0,1.[
     & (for x be real number st x in ].0,1.[ holds
        ||. diff(f,x) .|| <= diff(g,x));
   now let e be Real;
    assume A2: 0 < e;
    set e1=e/2;
    set B = {x where x is Real : x in [.0,1.]
               & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0};
    now let z be set;
     assume z in B; then
     ex x be Real st z=x & x in [.0,1.]
          & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0;
     hence z in REAL;
    end; then
    reconsider B as Subset of REAL by TARSKI:def 3;
    now let r be real number;
     assume r in B; then
     ex x be Real st r = x & x in [.0,1.]
       & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; then
A3: ex t be Real st r = t & 0<=t & t<=1; then
     abs r = r by ABSVALUE:def 1;
     hence abs r < 2 by A3,XXREAL_0:2;
    end; then
A4: B is real-bounded by SEQ_4:4;

    set s = upper_bound B;

A5: ex d be real number st 0 < d & d in B
    proof
     0 in [.0,1.]; then
     consider d1 be real number such that
A6:  0 < d1 & for x1 be real number st x1 in [.0,1.] & abs(x1-0) < d1
             holds ||. f/.x1 - f/.0 .|| < e1 by A2,A1,NFCONT_3:17;
     set d2=d1/2;
A7: d2 < d1 by A6,XREAL_1:216;
     take d = min(d2,1);
     thus A8: 0 < d by A6,XXREAL_0:21;
A9: d <= 1 by XXREAL_0:17; then
A10: d in [.0,1.] by A8;
A11: d <= d2 by XXREAL_0:17;
     abs(d-0) = d by A8,ABSVALUE:def 1; then
     abs(d-0) < d1 by A11,A7,XXREAL_0:2; then
A12: ||. f/.d - f/.0 .|| < e1 by A6,A10;

A13: [.0,d.] c= dom g by A1,A9,XXREAL_1:34;

A14: g| [.0,d.] is continuous by A1,A9,FCONT_1:16,XXREAL_1:34;

A15: ].0,d.[ c=].0,1.[ by A9,XXREAL_1:46; then
     consider x0 be Real such that
A16:  x0 in ].0,d.[
     & diff(g,x0) =(g.d-g.0)/(d-0) by A1,A8,A13,A14,FDIFF_1:26,ROLLE:3;

     ||. diff(f,x0) .|| <= diff(g,x0) by A1,A16,A15; then
     0 <= g.d-g.0 by A8,A16; then
     (0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1
       by A12,XREAL_1:7; then
     (0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1+ e1*d
       by A8,A2,XREAL_1:7; then
     ||. f/.d - f/.0 .|| -( (g.d - g.0) + e1+ e1*d ) <= 0 by XREAL_1:47; then
     ||. f/.d -f/.0 .|| - (g.d - g.0) - e1*d - e1 <= 0;
     hence d in B by A10;
    end; then
A17: 0 < s by A4,SEQ_4:def 1;
    now let r be real number;
     assume r in B; then
     ex x be Real st r = x & x in [.0,1.]
       & ||. f/.x -f/.0 .|| - (g.x - g.0 ) - e1*x - e1 <= 0; then
     ex t be Real st r=t & 0<=t & t<=1;
     hence r<=1;
    end; then
A18: s <= 1 by A5,SEQ_4:45;

    defpred P[Element of NAT,Element of REAL]
      means $2 in B & abs(s-$2) <= 1/($1+1);

A19:now let x be Element of NAT;
     reconsider t = 1/(1+x) as real number;
     consider r be real number such that
A20:  r in B & s-t < r by A4,A5,SEQ_4:def 1;
     reconsider r as Element of REAL by XREAL_0:def 1;
     take r;
     s-t + t < r + t by A20,XREAL_1:8; then
A21: s -r < t+r -r by XREAL_1:14;
     r <= s by A4,A20,SEQ_4:def 1; then
     0 <= s - r by XREAL_1:48;
     hence P[x,r] by A20,A21,SEQ_2:1;
    end;
    consider sq be Function of NAT,REAL such that
A22: for x being Element of NAT holds P[x, sq.x] from FUNCT_2:sch 3(A19);
    reconsider sq as Real_Sequence;
A23: now let p1 be real number;
     assume A24: 0 < p1;
     set p = p1/2;
     consider n be Element of NAT such that
A25:  1/p < n by SEQ_4:3;

     1/p + (0 qua Real) < n+1 by A25,XREAL_1:8; then
A26:  1/(n+1) <= 1/(1/p) by A24,XREAL_1:118;
     take n;
     thus for m be Element of NAT st n<=m holds abs (sq.m-s) < p1
     proof
      let m be Element of NAT;
      assume n<=m; then
      0 < n+1 & n+1 <= m+1 by XREAL_1:6; then
      1/(m+1) <= 1/(n+1) by XREAL_1:118; then
A27:   1/(m+1) <= p by A26,XXREAL_0:2;

      sq.m in B & abs(s-sq.m) <= 1/(m+1) by A22; then
      abs(sq.m-s) <= 1/(1+m) by COMPLEX1:60; then
A28:   abs(sq.m-s) <= p by A27,XXREAL_0:2;
      p < p1 by A24,XREAL_1:216;
      hence thesis by A28,XXREAL_0:2;
     end;
    end; then
A29:sq is convergent by SEQ_2:def 6; then
A30:lim sq = s by A23,SEQ_2:def 7;
    deffunc F(Real) = ||. f/.$1 -f/.0 .|| - (g.$1 - g.0) - e1*$1 - e1;
A31:for x being Element of REAL holds F(x) in REAL;
    consider Lg0 be Function of REAL,REAL such that
A32: for x being Element of REAL holds Lg0.x = F(x) from FUNCT_2:sch 8(A31);

    set Lg = Lg0| [.0,1.];
A33: dom Lg0 = REAL by FUNCT_2:def 1; then
A34:
    dom Lg = [.0,1.] by RELAT_1:62;

    now let y be set;
     assume y in rng sq; then
     ex x be set st x in NAT & sq.x = y by FUNCT_2:11; then
     y in B by A22; then
     ex x be Real st y=x & x in [.0,1.]
       & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0;
     hence y in [.0,1.];
    end; then
A35:
    rng sq c= dom Lg by A34,TARSKI:def 3;

A36:s in [.0,1.] by A18,A17;

    now let r be real number;
     set r3=r/3;
     assume A37: 0<r; then
     consider t1 be real number such that
A38:  0 < t1 & for x1 be real number st x1 in [.0,1.] & abs(x1-s) < t1
             holds ||. f/.x1 - f/.s .|| < r3 by A1,A36,NFCONT_3:17;
     consider t2 be real number such that
A39:  0 < t2 & for x1 be real number st x1 in [.0,1.] & abs(x1-s) < t2
             holds abs(g.x1 - g.s) < r3
         by A37,A36,A1,FCONT_1:14;
     set t30 = r3/e1;
     set t3 = t30/2;
     0 < t3 & t3 < t30 by A2,A37,XREAL_1:216; then
     e1*t3 < (r3/e1)*e1 by A2,XREAL_1:97; then
A40: e1*t3 < r3 by A2,XCMPLX_1:87;
     take t = min(min(t1,t2),t3);
A41:  min(t1,t2) <= t1 & min(t1,t2) <= t2 & 0 < min(t1,t2)
       by A38,A39,XXREAL_0:17,21;
     hence 0 < t by A2,A37,XXREAL_0:21;

A42: t <= t3 by XXREAL_0:17;
A43:  t <= min(t1,t2) by XXREAL_0:17; then
A44:  t <= t1 by A41,XXREAL_0:2;
A45: t <= t2 by A41,A43,XXREAL_0:2;

     thus for x1 be real number st x1 in dom Lg & abs(x1-s) < t
             holds abs(Lg.x1 - Lg.s) < r
     proof
      let x1 be real number;
A46:   x1 is Element of REAL by XREAL_0:def 1;

      assume that
A47: x1 in dom Lg and
A48: abs(x1-s) < t;
      x1 in [.0,1.] by A33,A47,RELAT_1:62; then
A49: Lg.x1 = Lg0.x1 by FUNCT_1:49
           .= ||. f/.x1 -f/.0 .|| - (g.x1 - g.0) - e1*x1 - e1 by A32,A46;
      Lg.s = Lg0.s by A36,FUNCT_1:49; then
      Lg.s = ||. f/.s -f/.0 .|| - (g.s - g.0) - e1*s - e1 by A32; then
      (Lg.x1 - Lg.s)
        = ||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .|| - (g.x1 - g.s) -e1*(x1-s)
         by A49; then
A50: abs(Lg.x1 - Lg.s)
       <= abs(||. f/.x1 -f/.0 .|| - ||. f/.s -f/.0 .|| - (g.x1 - g.s))
          +abs(e1*(x1-s)) by COMPLEX1:57;
      abs(||. f/.x1 -f/.0 .|| - ||. f/.s -f/.0 .|| - (g.x1 - g.s))
       <= abs(||. f/.x1 -f/.0 .|| - ||. f/.s -f/.0 .||) + abs(g.x1 - g.s)
         by COMPLEX1:57; then
      abs(||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .|| - (g.x1 - g.s))
        + abs(e1*(x1-s))
       <= abs(||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||) +abs(g.x1 - g.s)
        + abs(e1*(x1-s)) by XREAL_1:6; then
A51: abs(Lg.x1 - Lg.s)
       <= abs(||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||) +abs(g.x1 - g.s)
        + abs(e1*(x1-s)) by A50,XXREAL_0:2;
A52: abs(||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||)
        <= ||. (f/.x1 -f/.0)- (f/.s -f/.0) .|| by NORMSP_1:9;
      (f/.x1 -f/.0)- (f/.s -f/.0)
        = f/.x1 -(f/.0 -(-(f/.s -f/.0))) by RLVECT_1:29
       .= f/.x1 -(f/.0 + (f/.s -f/.0)) by RLVECT_1:17
       .= f/.x1 -(f/.s- (f/.0 -f/.0)) by RLVECT_1:29
       .= f/.x1 -(f/.s- 0.T) by RLVECT_1:5
       .= f/.x1 -f/.s by RLVECT_1:13; then
      abs(||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||) +abs(g.x1 - g.s)
       <= ||. f/.x1 -f/.s .|| + abs(g.x1 - g.s) by A52,XREAL_1:6; then
      abs(||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||) +abs(g.x1 - g.s)
         + abs(e1*(x1-s))
       <= ||. f/.x1 -f/.s .|| + abs(g.x1 - g.s) + abs(e1*(x1-s))
          by XREAL_1:6; then
A53: abs(Lg.x1 - Lg.s)
       <= ||. f/.x1 -f/.s .|| + abs(g.x1 - g.s) + abs(e1*(x1-s))
          by A51,XXREAL_0:2;
      abs(x1-s) < t2 by A48,A45,XXREAL_0:2; then
      abs(g.x1 -g.s) < r3 by A47,A34,A39; then
A54: ||. f/.x1 -f/.s .|| + abs(g.x1 - g.s)
        < ||. f/.x1 -f/.s .|| + r3 by XREAL_1:8;

      abs(x1-s) < t3 by A48,A42,XXREAL_0:2; then
      abs(x1-s)*e1 <= t3*e1 by A2,XREAL_1:64; then
      abs(x1-s)*abs(e1) <= t3*e1 by A2,ABSVALUE:def 1; then
      abs(e1*(x1-s)) <= t3*e1 by COMPLEX1:65; then
A55: abs(e1*(x1-s)) < r3 by A40,XXREAL_0:2;
      abs(x1-s) < t1 by A48,A44,XXREAL_0:2; then
      ||. f/.x1 -f/.s .|| < r3 by A47,A34,A38; then
      ||. f/.x1 -f/.s .|| + r3 < r3 + r3 by XREAL_1:8; then
      ||. f/.x1 -f/.s .|| + abs(g.x1 - g.s) < r3 + r3 by A54,XXREAL_0:2; then
      ||. f/.x1 -f/.s .|| + abs(g.x1 - g.s)+ abs(e1*(x1-s))
         < r3 + r3 + r3 by A55,XREAL_1:8;
      hence abs(Lg.x1 - Lg.s) < r by A53,XXREAL_0:2;
     end;
    end; then
    Lg is_continuous_in s by FCONT_1:3; then
A56:Lg/*sq is convergent & Lg.s = lim (Lg/*sq) by A29,A30,A35,FCONT_1:def 1;

A57:for n be Element of NAT holds 0 <= (-(Lg/*sq)).n
    proof
     let n be Element of NAT;
     (-(Lg/*sq)).n = - (Lg/*sq).n by SEQ_1:10; then
A58:  (-(Lg/*sq)).n = - Lg.(sq.n) by A35,FUNCT_2:108;

     P[n, sq.n] by A22; then
A59: ex x be Real st sq.n=x & x in [.0,1.]
      & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; then
     Lg0.(sq.n) <=0 by A32; then
     Lg.(sq.n) <=0 by A59,FUNCT_1:49;
     hence 0 <= (-(Lg/*sq)).n by A58;
    end;

    -(Lg/*sq) is convergent by A56,SEQ_2:9; then
    0 <= lim -(Lg/*sq) by A57,SEQ_2:17; then
    0 <= - lim (Lg/*sq) by A56,SEQ_2:10; then
    Lg.s <= 0 by A56; then
    Lg0.s <= 0 by A36,FUNCT_1:49; then
A60: ||. f/.s -f/.0 .|| - (g.s - g.0) - e1*s -  e1 <= 0 by A32;
A61: s = 1
    proof
     assume s <> 1; then
     s < 1 by A18,XXREAL_0:1; then
A62:  s in ].0,1.[ by A17; then
     f is_differentiable_in s by A1,NDIFF_3:10; then
     consider N1 being Neighbourhood of s such that
A63:   N1 c= dom f & ex L1 be LinearFunc of T,R1 be RestFunc of T
        st diff(f,s)=L1.1
       & for x be Real st x in N1 holds f/.x-f/.s = L1.(x-s) + R1/.(x-s)
        by NDIFF_3:def 4;
     consider L1 be LinearFunc of T,R1 be RestFunc of T such that
A64:  diff(f,s)=L1.1
      & for x be Real st x in N1 holds
          f/.x-f/.s = L1.(x-s) + R1/.(x-s) by A63;

     g is_differentiable_in s by A1,A62,FDIFF_1:9; then
     consider N2 being Neighbourhood of s such that
A65:  N2 c= dom g & ex L2 be LinearFunc,R2 be RestFunc
       st diff(g,s)=L2.1
        & for x be Real st x in N2 holds
            g.x-g.s = L2.(x-s) + R2.(x-s) by FDIFF_1:def 5;
     consider L2 be LinearFunc,R2 be RestFunc such that
A66:  diff(g,s)=L2.1
      & for x be Real st x in N2 holds
          g.x-g.s = L2.(x-s) + R2.(x-s) by A65;
     consider NN3 being Neighbourhood of s such that
A67: NN3 c= N1 & NN3 c= N2 by RCOMP_1:17;
     consider g0 be real number such that
A68: 0 < g0 & ].s-g0,s+g0.[ c= ].0,1.[ by A62,RCOMP_1:19;
     reconsider NN4 = ].s-g0,s+g0.[ as Neighbourhood of s
       by A68,RCOMP_1:def 6;
     consider N3 being Neighbourhood of s such that
A69: N3 c= NN3 & N3 c= NN4 by RCOMP_1:17;

A70: N3 c= N1 & N3 c= N2 & N3 c= ].0,1.[ by A69,A67,A68,XBOOLE_1:1;

     consider d1 be real number such that
A71:  0<d1 & N3 = ]. s-d1,s+d1.[ by RCOMP_1:def 6;

     set e2=e1/2;
     R1 is total & R1 is RestFunc-like by NDIFF_3:def 1; then
     consider d2 be Real such that
A72:  0<d2 & for t be Real st t <> 0 & abs t < d2
        holds ||. (R1/.t) .|| / abs t < e2 by A2,Th17;

     R2 is total & R2 is RestFunc-like by FDIFF_1:def 2; then
     consider d3 be Real such that
A73:  0<d3 & for t be Real st t <> 0 & abs t < d3
        holds abs(R2.t)/abs t < e2 by A2,Th18;

A74:  min(d1,d2) <= d1 & min(d1,d2) <= d2 & 0 < min(d1,d2)
       by A71,A72,XXREAL_0:17,21;

     set d40= min(min(d1,d2),d3);
A75:  d40 <= min(d1,d2) & d40 <= d3 & 0 < d40 by A73,A74,XXREAL_0:17,21;

     set d4=d40/2;
A76:  d40 <= d1 & d40 <= d2 by A74,A75,XXREAL_0:2;

     d4 < d40 by A75,XREAL_1:216; then
A77: 0 < d4 & d4 < d1 & d4 < d2 & d4 < d3 by A75,A76,XXREAL_0:2; then
     s-d1< s+d4 & s+d4< s+d1 by XREAL_1:8; then
A78: s+d4 in N3 by A71; then
A79: f/.(s+d4)-f/.s = L1.((s+d4)-s) + R1/.((s+d4)-s) by A64,A70;
A80: g.(s+d4)-g.s = L2.((s+d4)-s) + R2.((s+d4)-s) by A70,A78,A66;

     consider df1 be Point of T such that
A81:   for p be Real holds L1.p = p*df1 by NDIFF_3:def 2;

     L1.1 = 1*df1 by A81; then
     L1.1 = df1 by RLVECT_1:def 8; then
A82: L1.d4 = d4*diff(f,s) by A64,A81;
     consider df2 be Real such that
A83:   for p be Real holds L2.p = df2*p by FDIFF_1:def 3;

     L2.1 = df2*1 by A83; then
A84: L2.d4 = d4*diff(g,s) by A66,A83;

A85: ||. f/.(s+d4)-f/.s .|| <= ||. L1.d4 .|| + ||. R1/. d4 .||
        by A79,NORMSP_1:def 1;

A86: ||. L1.d4 .|| = (abs d4)*||. diff(f,s) .|| by A82,NORMSP_1:def 1
         .= ||. diff(f,s) .||*d4 by A75,ABSVALUE:def 1;

A87:  0 < abs d4 by A75,ABSVALUE:def 1;

     abs d4 < d2 by A77,ABSVALUE:def 1; then
     ||. R1/.d4 .|| / (abs d4) < e2 by A72,A75; then
     ||. R1/.d4 .|| <= e2 * (abs d4) by A87,XREAL_1:81; then
     ||. R1/.d4 .|| <= e2 * d4 by A75,ABSVALUE:def 1; then
     ||. L1.d4 .|| + ||. R1/.d4 .||
        <= ||. diff(f,s) .|| * d4 + e2 * d4 by A86,XREAL_1:6; then
A88:  ||. f/.(s+d4)-f/.s .||
        <= ||. diff(f,s) .|| * d4 + e2 * d4 by A85,XXREAL_0:2;

     ||. diff(f,s) .||*d4 <=diff(g,s)*d4 by A62,A1,A77,XREAL_1:64; then
     ||. diff(f,s) .||*d4 + e2*d4 <= diff(g,s)*d4 + e2*d4 by XREAL_1:6; then
A89: ||. f/.(s+d4)-f/.s .|| <= diff(g,s)*d4 + e2*d4 by A88,XXREAL_0:2;

     abs d4 < d3 by A77,ABSVALUE:def 1; then
     abs(R2.d4)/ (abs d4) < e2 by A73,A75; then
     abs(R2.d4) <= e2* (abs d4) by A87,XREAL_1:81; then
     abs(R2.d4) <= e2* d4 by A75,ABSVALUE:def 1; then
       -(e2*d4) <= R2.d4 by ABSVALUE:5; then
     d4*diff(g,s) -(e2*d4) <= g.(s+d4)-g.s by A80,A84,XREAL_1:6; then
     d4*diff(g,s) <= g.(s+d4)-g.s + e2*d4 by XREAL_1:20; then
     diff(g,s)*d4 + e2*d4
      <= (g.(s+d4)-g.s + e2*d4) + e2*d4 by XREAL_1:6; then
     ||. f/.(s+d4)-f/.s .|| <= g.(s+d4)-g.s + e1*d4 by A89,XXREAL_0:2; then
     ||. f/.(s+d4)-f/.s .|| - (g.(s+d4)-g.s + e1*d4) <= 0 by XREAL_1:47; then
A90: ||. f/.(s+d4)-f/.s .|| - g.(s+d4)+g.s - e1*d4
       + (||. f/.s -f/.0 .|| - (g.s - g.0 ) - e1*s -  e1)
       <= (0 qua Real)+ (0 qua Real) by A60;

     ||. f/.(s+d4)-f/.0 .||
       <= ||. f/.(s+d4)-f/.s .|| + ||. f/.s -f/.0 .|| by NORMSP_1:10; then
     ||. f/.(s+d4)-f/.0 .|| - (g.(s+d4) -g.0 + e1*(d4+s) + e1)
       <= ||. f/.(s+d4)-f/.s .|| + ||. f/.s -f/.0 .||
         - (g.(s+d4) -g.0 + e1*(d4+s) + e1) by XREAL_1:9; then
A91: ||. f/.(s+d4)-f/.0 .|| - (g.(s+d4) -g.0) - e1*(s+d4) -e1 <= 0 by A90;

     abs((0 qua real number)+1-2*(s+d4))< 1 -(0 qua real number)
        by A78,A70,RCOMP_1:3; then
     s + d4 in [.0,1.] by RCOMP_1:2; then
A92: s+d4 in B by A91;

     s +(0 qua Real) < s + d4 by A75,XREAL_1:8;
     hence contradiction by A92,A4,SEQ_4:def 1;
    end;
    0 in dom g & 1 in dom g by A1; then
    g/.1 = g.1 & g/.0 = g.0 by PARTFUN1:def 6; then
    ||. f/.1 -f/.0 .|| - (g/.1 - g/.0 ) - e + e <= (0 qua Real) + e
     by A61,A60,XREAL_1:6;
    hence ||. f/.1 -f/.0 .|| - (g/.1 - g/.0) <= e;
   end; then
   ||. f/.1 -f/.0 .|| - (g/.1 - g/.0) <= 0 by Lm3; then
   ||. f/.1 -f/.0 .|| - (g/.1 - g/.0) + (g/.1 - g/.0)
      <= (0 qua Real) + (g/.1 - g/.0) by XREAL_1:6;
   hence thesis;
end;

theorem Th19:
for S,T be non trivial RealNormSpace,
    f be PartFunc of S,T, p,q be Point of S, M be Real
  st [.p,q.] c= dom f
   & (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
   & (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
   & (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) .|| <= M)
holds ||. f/.q - f/.p .|| <= M*||. q-p .||
proof
   let S,T be non trivial RealNormSpace,
       f be PartFunc of S,T, p,q be Point of S, M be Real;
   assume A1: [.p,q.] c= dom f
    & (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
    & (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
    & (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) .|| <= M);

   deffunc PP(Element of REAL) = $1*(q-p)+p;

   consider pt0 be Function of REAL,the carrier of S such that
A2: for t being Element of REAL holds pt0.t = PP(t) from FUNCT_2:sch 4;

   set pt=pt0 | ([.0,1.]);
A3:dom pt0 = REAL by FUNCT_2:def 1; then
A4:dom pt = [.0,1.] by RELAT_1:62;

   now let t be real number;
    assume t in [.0,1.];

A5:t is Element of REAL by XREAL_0:def 1; then
    pt0/.t = pt0.t by A3,PARTFUN1:def 6;
    hence pt0/.t = t*(q-p)+p by A2,A5;
   end; then
A6:pt is continuous by NFCONT_3:33;

A7: ].0,1.[ c= [.0,1.] by XXREAL_1:25;

A8:now let t be Real;
    assume t in ].0,1.[;
    hence pt/.t = pt0/.t by A4,A7,PARTFUN2:15
               .= t*(q-p)+p by A2;
   end; then
A9:pt is_differentiable_on ].0,1.[
    & for t be Real st t in ].0,1.[ holds (pt`|].0,1.[ ).t = (q-p)
         by A4,A7,NDIFF_3:21;

   reconsider phi = f*pt as PartFunc of REAL,T;

A10:rng pt c= [.p,q.]
   proof
    let y be set;
    assume y in rng pt; then
    consider x be set such that
A11:  x in dom pt & y = pt.x by FUNCT_1:def 3;
A12: y = pt0.x by A11,FUNCT_1:47;
    reconsider x as Element of REAL by A11;

    consider r be Real such that
A13: x=r & 0<=r & r<=1 by A11,A4;

    y = p+ x*(q-p) by A2,A12 .= (1-x)*p + x*q by Lm2; then
    y in {(1-r1)*p + r1*q where r1 is Real : 0 <= r1 & r1 <= 1 } by A13;
    hence y in [. p,q .] by RLTOPSP1:def 2;
   end; then
   rng pt c= dom f by A1,XBOOLE_1:1; then
A14:
   dom phi = [.0,1.] by A4,RELAT_1:27;

A15:
   for t be real number st t in [.0,1.] holds phi/.t = f/.(p+t*(q-p))
   proof
    let t be real number;
    assume A16: t in [.0,1.]; then
A17: phi/.t =phi.t by A14,PARTFUN1:def 6
          .= f.(pt.t) by A16,A14,FUNCT_1:12;
    pt.t in rng pt by A16,A4,FUNCT_1:def 3; then
A18: pt.t in [.p,q.] by A10;

    pt.t = pt0.t by A16,A4,FUNCT_1:47
        .= p+t*(q-p) by A2,A16;
    hence thesis by A17,A18,A1,PARTFUN1:def 6;
   end;

   now let x0 be real number;
    assume A19: x0 in dom phi; then
A20: pt is_continuous_in x0 by A4,A6,A14,NFCONT_3:def 2;
    pt.x0 in rng pt by A4,A19,A14,FUNCT_1:def 3; then
    pt.x0 in [.p,q.] by A10; then
    pt/.x0 in [.p,q.] by A19,A14,A4,PARTFUN1:def 6;
    hence phi is_continuous_in x0 by A1,A19,A20,NFCONT_3:15;
   end; then
   phi is continuous by NFCONT_3:def 2; then
A21:phi| [.0,1.] is continuous;

A22:
   now let x be Real;
    assume A23: x in ].0,1.[; then
A24: pt is_differentiable_in x by A9,NDIFF_3:10;
    (pt`|].0,1.[ ).x = (q-p) by A23,A8,A4,A7,NDIFF_3:21; then
A25: diff(pt,x) = (q-p) by A9,A23,NDIFF_3:def 6;
A26: pt.x = pt/.x by A23,A7,A4,PARTFUN1:def 6;

A27: ex r be Real st x=r & 0<r & r<1 by A23;
A28: pt.x= pt0.x by A23,A7,A4,FUNCT_1:47;

A29: pt0.x = p+ x*(q-p) by A2; then
    pt.x in ].p,q.[ by A27,A28; then
A30: f is_differentiable_in pt/.x by A26,A1;
    hence phi is_differentiable_in x by A24,Th6;
    thus diff(phi,x) = diff(f,p+ x*(q-p)).(q-p)
      by A25,A26,A28,A29,A30,A24,Th6;
   end; then
   ].0,1.[ c= dom phi & for x be Real st x in ].0,1.[ holds
   phi is_differentiable_in x by A14,XXREAL_1:25; then
A31:phi is_differentiable_on ].0,1.[ by NDIFF_3:10;

   deffunc GG(Element of REAL) = M*||. q-p .||*$1;

   consider g0 be Function of REAL,REAL such that
A32: for t being Element of REAL holds g0.t = GG(t) from FUNCT_2:sch 4;

   set g=g0 | ([.0,1.]);
   for t be real number st t in [.0,1.] holds
     g0.t = (M*||. q-p .||)*t + (0 qua real number) by A32; then
A33:g is continuous by FCONT_1:41;

   dom g0 = REAL by FUNCT_2:def 1; then
A34:dom g = [.0,1.] by RELAT_1:62;
A35:g| [.0,1.] is continuous by A33;

A36:now let t be Real;
    assume t in ].0,1.[;
    hence g.t =g0.t by A34,A7,FUNCT_1:47
             .= M*||. q-p .||*t + (0 qua Real) by A32;
   end; then
A37:g is_differentiable_on ].0,1.[
    & for t be Real st t in ].0,1.[ holds (g`|].0,1.[ ).t = M*||. q-p .||
       by A34,A7,FDIFF_1:23;
   for t be real number st t in ].0,1.[ holds ||. diff(phi,t) .|| <= diff(g,t)
   proof
    let t be real number;
    assume A38: t in ].0,1.[; then
A39: ||.diff(phi,t).|| = ||. diff(f,p+ t*(q-p)).(q-p) .|| by A22;
    reconsider L= diff(f,p+ t*(q-p)) as Lipschitzian LinearOperator of S,T
        by LOPBAN_1:def 9;
A40: ||.L.(q-p).|| <= ||.diff(f,p+ t*(q-p)).|| * ||.(q-p).|| by LOPBAN_1:32;
    ex r be Real st t=r & 0<r & r<1 by A38; then
    p+ t*(q-p) in ].p,q.[; then
A41: ||. diff(f,p+ t*(q-p)).|| * ||.q-p.|| <= M * ||.q-p.|| by A1,XREAL_1:64;

    diff(g,t) = (g`|].0,1.[ ).t by A38,A37,FDIFF_1:def 7; then
    diff(g,t) = M*||. q-p .|| by A38,A36,A34,A7,FDIFF_1:23;
    hence thesis by A41,A40,A39,XXREAL_0:2;
   end; then
A42:
   ||. phi/.1 -phi/.0 .|| <= g/.1 - g/.0 by Lm4,A14,A21,A31,A34,A35,A37;
A43:
   1 in [.0,1.] & 0 in [.0,1.]; then
A44:g/.1 =g.1 by A34,PARTFUN1:def 6
       .=g0.1 by A34,A43,FUNCT_1:47
       .= M*||. q-p .||*1 by A32;

A45:g/.0 = g.0 by A34,A43,PARTFUN1:def 6
       .=g0.0 by A34,A43,FUNCT_1:47
       .= M*||. q-p .|| * ( 0 qua Real) by A32;

A46:phi/.1 = f/.(p+1*(q-p)) by A15,A43
         .= f/.(p+(q-p)) by RLVECT_1:def 8
         .= f/.(q-(p-p)) by RLVECT_1:29
         .= f/.(q-0.S) by RLVECT_1:15
         .= f/.q by RLVECT_1:13;

   phi/.0 = f/.(p+( 0 qua Real ) * (q-p)) by A15,A43
         .= f/.(p+0.S) by RLVECT_1:10
         .= f/.p by RLVECT_1:4;
   hence thesis by A42,A44,A45,A46;
end;

theorem Th20:
for S,T be non trivial RealNormSpace, f be PartFunc of S,T,
    p,q be Point of S, M be Real,
    L be Point of R_NormSpace_of_BoundedLinearOperators(S,T)
  st [.p,q.] c= dom f
   & (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
   & (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
   & (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) - L .|| <= M)
holds ||. f/.q - f/.p -L.(q-p).|| <= M*||. q-p .||
proof
   let S,T be non trivial RealNormSpace,
       f be PartFunc of S,T,
       p,q be Point of S,
       M be Real,
       L be Point of R_NormSpace_of_BoundedLinearOperators(S,T);

   assume that
A1: [.p,q.] c= dom f and
A2: (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
  & (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
  & (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) - L .|| <= M);

   reconsider LP=L as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;

   deffunc LL(Point of S) = L.($1-p);

   consider L0 be Function of the carrier of S,the carrier of T such that
A3: for t being Element of the carrier of S
      holds L0.t = LL(t)  from FUNCT_2:sch 4;

A4:dom L0 = the carrier of S by FUNCT_2:def 1;

   now let x1,x2 be Point of S;
    assume x1 in dom L0 & x2 in dom L0;

A5: -1 is Real by XREAL_0:def 1;

    L0/.x1=L.(x1-p) & L0/.x2=L.(x2-p) by A3; then
    ||.L0/.x1-L0/.x2 .||
      = ||.LP.(x1-p)+(-1)*LP.(x2-p) .|| by RLVECT_1:16
     .= ||.LP.(x1-p)+LP.((-1)*(x2-p)) .|| by A5,LOPBAN_1:def 5
     .= ||.LP.((x1-p)+(-1)*(x2-p)) .|| by VECTSP_1:def 20
     .= ||.LP.((x1-p)-(x2-p)) .|| by RLVECT_1:16
     .= ||. LP.(x1-((x2-p)+p)) .|| by RLVECT_1:27
     .= ||. LP.(x1-(x2-(p-p))) .|| by RLVECT_1:29
     .= ||. LP.(x1-(x2-0.S)) .|| by RLVECT_1:15
     .= ||. LP.(x1-x2) .|| by RLVECT_1:13; then
A6: ||.L0/.x1-L0/.x2 .|| <= ||.L.|| * ||.x1-x2.|| by LOPBAN_1:32;

    (0 qua Real) + ||.L.|| < (1 qua Real) + ||.L.|| by XREAL_1:8; then
    ||.L.|| * ||.x1-x2.|| <= (||.L.||+1) * ||.x1-x2.|| by XREAL_1:64;
    hence
      ||.L0/.x1-L0/.x2 .|| <= (||.L.||+1) * ||.x1-x2.|| by A6,XXREAL_0:2;
   end; then
   L0 is_Lipschitzian_on (dom L0) by NFCONT_1:def 9; then
A7:L0 is_continuous_on (dom L0) by NFCONT_1:45;

   reconsider R = (the carrier of S) --> 0.T as PartFunc of S,T;

A8:dom R = the carrier of S by FUNCOP_1:13;
   now let h be (0.S)-convergent non-zero sequence of S;
A9: now let n be Nat;
A10:  R/.(h.n) =R.(h.n) by A8,PARTFUN1:def 6
             .=0.T by FUNCOP_1:7;
A11:  rng h c= dom R by A8;
A12: n in NAT by ORDINAL1:def 12;
     hence ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n)
           by NDIFF_1:def 2
        .=(||.h.||".n)*(R/.(h.n)) by A12,A11,FUNCT_2:109
        .=0.T by A10,RLVECT_1:10;
    end; then
A13: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
    hence (||.h.||")(#)(R/*h) is convergent by NDIFF_1:18;
    ((||.h.||")(#)(R/*h)).0 = 0.T by A9;
    hence lim ((||.h.||")(#)(R/*h)) = 0.T by A13,NDIFF_1:18;
   end; then
   reconsider R as RestFunc of S,T by NDIFF_1:def 5;
A14:
   now let x0 be Point of S;
    set N = the Neighbourhood of x0;
A15:for x be Point of S st x in N holds L0/.x-L0/.x0=L.(x-x0)+R/.(x-x0)
    proof
     let x be Point of S;
A16: R/.(x-x0) =R.(x-x0) by A8,PARTFUN1:def 6
       .=0.T by FUNCOP_1:7;
A17: -1 is Real by XREAL_0:def 1;
     assume x in N;
     thus L0/.x-L0/.x0 = L.(x-p)-L0.x0 by A3
       .= L.(x-p)-L.(x0-p) by A3
       .= LP.(x-p)+(-1)*LP.(x0-p) by RLVECT_1:16
       .= LP.(x-p)+LP.((-1)*(x0-p)) by A17,LOPBAN_1:def 5
       .= LP.((x-p)+(-1)*(x0-p)) by VECTSP_1:def 20
       .= LP.((x-p)-(x0-p)) by RLVECT_1:16
       .= LP.(x-((x0-p)+p)) by RLVECT_1:27
       .= LP.(x-(x0-(p-p))) by RLVECT_1:29
       .= LP.(x-(x0-0.S)) by RLVECT_1:15
       .= LP.(x-x0) by RLVECT_1:13
       .= L.(x-x0) + R/.(x-x0) by A16,RLVECT_1:4;
    end;
    hence L0 is_differentiable_in x0 by A4,NDIFF_1:def 6;
    hence diff(L0,x0) = L by A4,A15,NDIFF_1:def 7;
   end;

   set g= f - L0;

A18:dom g = dom f /\ dom L0 by VFUNCT_1:def 2
        .= dom f by A4,XBOOLE_1:28;

A19:for x be Point of S st x in dom g holds g/.x= f/.x - L.(x-p)
   proof
    let x be Point of S;
    assume x in dom g;
    hence g/.x= f/.x - L0/.x by VFUNCT_1:def 2
             .=f/.x - L.(x-p) by A3;
   end;

A20:for x be Point of S st x in [.p,q.] holds g is_continuous_in x
   proof
    let x be Point of S;
    assume x in [.p,q.]; then
A21:f is_continuous_in x by A2;
    L0 | (dom L0) is_continuous_in x by A4,A7,NFCONT_1:def 7; then
    L0 is_continuous_in x;
    hence thesis by A21,NFCONT_1:15;
   end;

A22:for x be Point of S st x in ].p,q.[ holds g is_differentiable_in x
   proof
    let x be Point of S;
    assume x in ].p,q.[; then
    f is_differentiable_in x & L0 is_differentiable_in x by A2,A14;
    hence g is_differentiable_in x by NDIFF_1:36;
   end;

   for x be Point of S st x in ].p,q.[ holds ||. diff(g,x) .|| <= M
   proof
    let x be Point of S;
    assume A23: x in ].p,q.[; then
A24: f is_differentiable_in x by A2;
    L0 is_differentiable_in x & diff(L0,x) = L by A14; then
    diff(g,x) = diff(f,x) - L by A24,NDIFF_1:36;
    hence ||. diff(g,x) .|| <= M by A2,A23;
   end; then
A25:
   ||. g/.q - g/.p .|| <= M*||. q-p .|| by Th19,A1,A18,A20,A22;
   p in [.p,q.] by RLTOPSP1:68; then
   g/.p= f/.p - L.(p-p) by A1,A18,A19; then
A26:g/.p = f/.p - LP.(0.S) by RLVECT_1:15
       .=f/.p - LP.( 0 *p ) by RLVECT_1:10
       .=f/.p - 0 * LP.p by LOPBAN_1:def 5
       .=f/.p - 0.T by RLVECT_1:10
       .=f/.p by RLVECT_1:13;
   q in [.p,q.] by RLTOPSP1:68; then
   g/.q= f/.q - L.(q-p) by A1,A18,A19; then
   f/.q - (L.(q-p) +f/.p ) = g/.q - g/.p by A26,RLVECT_1:27;
   hence thesis by A25,RLVECT_1:27;
end;

begin :: Partial derivative of a function of several variables.

definition
  let G be RealNormSpace-Sequence;
  let i be Element of dom G;
  func proj i -> Function of product G,G.i means  :Def3:
 for x be Element of product carr G holds it.x = x.i;
existence
proof
   deffunc F(Element of product carr G) = $1.i;
   consider f being Function of product carr G,G.i such that
A1: for x being Element of product carr G holds f.x = F(x) from FUNCT_2:sch 4;
   product G = NORMSTR(# product carr G,zeros G,[:addop G:]
          ,[:multop G:], productnorm G #) by PRVECT_2:6; then
   reconsider f as Function of product G,G.i;
   take f;
   thus thesis by A1;
end;
uniqueness
proof
   let f,g be Function of the carrier of (product G),the carrier of (G.i);
   assume that
A2: for x being Element of product carr G holds f.x = x.i and
A3: for x being Element of product carr G holds g.x = x.i;
A4:product G = NORMSTR(# product carr G,zeros G,[:addop G:]
               ,[:multop G:], productnorm G #) by PRVECT_2:6;
   now let x1 be Element of the carrier of product G;
    reconsider x=x1 as Element of product carr G by A4;
    f.x1 =x.i by A2;
    hence f.x1 = g.x1 by A3;
   end;
   hence thesis by FUNCT_2:63;
end;
end;

definition
  let G be RealNormSpace-Sequence;
  let i be Element of dom G;
  let x be Element of product G;
  func reproj(i,x) -> Function of G.i,product G means :Def4:
  for r be Element of G.i holds it.r = x +* (i,r);
existence
proof
   reconsider x1 = x as Element of product carr G by Th10;
   defpred P[Element of G.i,
             Element of the carrier of product G] means
      $2 = x1 +* (i,$1);
A1:for r being Element of G.i
    ex y be Element of the carrier of product G st P[r,y]
   proof
    let r be Element of G.i;
    x1 +* (i,r) is Element of the carrier of product G by Th11;
    hence thesis;
   end;
   ex f being Function of the carrier of (G.i),the carrier of product G st
    for r be Element of G.i
      holds P[r,f.r] from FUNCT_2:sch 3(A1);
   hence thesis;
end;
uniqueness
proof
   let f,g be Function of the carrier of (G.i),the carrier of product G;
   assume that
A2:for r be Element of G.i holds f.r = x +* (i,r) and
A3:for r be Element of G.i holds g.r = x +* (i,r);
    let r be Element of G.i;
    f.r = x +* (i,r) by A2;
    hence f.r = g.r by A3;
end;
end;

definition
  let G be non-trivial RealNormSpace-Sequence;
  let j be set;
  assume A1: j in dom G;
  func modetrans(G,j) -> Element of dom G equals :Def5:
   j;
  correctness by A1;
end;

definition
  let G be non-trivial RealNormSpace-Sequence;
  let F be non trivial RealNormSpace;
  let i be set;
  let f be PartFunc of product G,F;
  let x being Element of product G;
  pred f is_partial_differentiable_in x,i means :Def6:
  f*reproj(modetrans(G,i),x) is_differentiable_in proj(modetrans(G,i)).x;
end;

definition
  let G be non-trivial RealNormSpace-Sequence;
  let F be non trivial RealNormSpace;
  let i be set;
  let f be PartFunc of product G,F;
  let x be Point of product G;
 func partdiff(f,x,i)
       -> Point of R_NormSpace_of_BoundedLinearOperators(G.modetrans(G,i),F)
    equals
 diff(f*reproj(modetrans(G,i),x),proj(modetrans(G,i)).x);
coherence;
end;

begin :: Linearity of Partial Differential Operator

reserve G for non-trivial RealNormSpace-Sequence;
reserve F for non trivial RealNormSpace;
reserve i for Element of dom G;
reserve f,f1,f2 for PartFunc of product G, F;
reserve x for Point of product G;
reserve X for set;

definition
  let G be non-trivial RealNormSpace-Sequence;
  let F be non trivial RealNormSpace;
  let i be set;
  let f be PartFunc of product G,F;
  let X be set;
  pred f is_partial_differentiable_on X,i means :Def8:
  X c= dom f & for x be Point of product G st x in X
    holds f|X is_partial_differentiable_in x,i;
end;

theorem Th21:
for xi be Element of G.i
  holds ||. reproj(i,0.(product G)).xi .|| = ||.xi.||
proof
   let xi be Element of G.i;
   set j = len G;
   reconsider i0 = i as Element of NAT;
   Seg len G = dom G by FINSEQ_1:def 3; then
A1:1 <= i0 & i0 <= j by FINSEQ_1:1;
   set z = 0.(product G);
A2: reproj(i,z).xi = z +* (i,xi) by Def4;
A3: the carrier of (product G) = product carr G by Th10;
   then reconsider w = z +* (i0,xi) as Element of product carr G by Th11;
A4: ||. reproj(i,z).xi .|| = |. normsequence(G,w) .|
         by A2,PRVECT_2:7;
   set q = ||.xi.||;
   set q1 = <*q*>;
   set y = 0*j;
A5:len normsequence(G,w) = j by PRVECT_2:def 11;
A6:len y = j by CARD_1:def 7; then
A7:(y| (i0-'1))^<*q*>^(y /^ i0) = Replace(y,i0,q) by A1,FINSEQ_7:def 1; then
A8:len ((y| (i0-'1))^<*q*>^(y /^ i0)) = len y by FINSEQ_7:5;
A9:len y = len Replace(y,i0,q) by FINSEQ_7:5;
   for k be Nat st 1 <= k & k <= len normsequence(G,w) holds
    normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k
   proof
    let k be Nat;
    assume A10: 1 <= k & k <= len normsequence(G,w); then
    reconsider k1 = k as Element of dom G by A5,FINSEQ_3:25;
A11: k1 in dom G;
    z in the carrier of product G; then
    z in product carr G by Th10; then
    consider g being Function such that
A12: z = g & dom g = dom carr G &
      for y being set st y in dom carr G holds g.y in (carr G).y
        by CARD_3:def 5;
A13: k in dom z by A11,A12,Lm1;
A14: (normsequence(G,w)).k
      = (the normF of (G.k1)).(w.k1) by PRVECT_2:def 11;
    per cases;
    suppose A15: k = i0; then
A16:  (normsequence(G,w)).k = ||. xi .|| by A14,A13,FUNCT_7:31;
     Replace(y,i0,q)/.k = q by A15,A10,A5,A6,FINSEQ_7:8;
     hence normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k
        by A16,A7,A10,A5,A6,A9,FINSEQ_4:15;
    end;
    suppose A17: k <> i0; then
     w.k1 = z.k1 by FUNCT_7:32; then
A18:  (normsequence(G,w)).k = ||. 0.(G.k1) .|| by A14,Th14,A3;
     Replace(y,i0,q)/.k = y/.k by A17,A10,A5,A6,FINSEQ_7:10; then
     Replace(y,i0,q).k = y/.k by A10,A5,A6,A9,FINSEQ_4:15; then
     Replace(y,i0,q).k = y.k by A10,A5,A6,FINSEQ_4:15;
     hence normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k
       by A18,A7;
    end;
   end; then
A19:normsequence(G,w) = (y| (i0-'1))^<*q*>^(y /^ i0)
     by A5,A6,A8,FINSEQ_1:14;
   sqrt Sum sqr(y| (i0-'1)) = |. 0*(i0-'1) .| by A1,PDIFF_7:2; then
   sqrt Sum sqr(y| (i0-'1)) = 0 by EUCLID:7; then
A20:Sum sqr(y| (i0-'1)) = 0 by RVSUM_1:86,SQUARE_1:24;
   sqrt Sum sqr(y/^i0) = |. 0*(j-'i0) .| by PDIFF_7:3; then
A21:sqrt Sum sqr(y/^i0) = 0 by EUCLID:7;
   sqr((y| (i0-'1))^<*q*>^(y/^i0))
     = sqr((y| (i0-'1))^<*q*>)^sqr(y/^i0) by RVSUM_1:144
    .= sqr(y| (i0-'1))^sqr<*q*>^sqr(y/^i0) by RVSUM_1:144
    .= sqr(y| (i0-'1))^<*q^2*>^sqr(y/^i0) by RVSUM_1:55; then
   Sum sqr((y| (i0-'1))^<*q*>^(y/^i0))
     = Sum(sqr(y| (i0-'1))^<*q^2*>) + Sum sqr(y/^i0) by RVSUM_1:75
    .= Sum sqr(y| (i0-'1)) + q^2 + Sum sqr(y/^i0) by RVSUM_1:74
    .= q^2 by A20,A21,RVSUM_1:86,SQUARE_1:24; then
   ||. reproj(i,z).xi .|| = |. q .| by A19,A4,COMPLEX1:72;
   hence thesis by COMPLEX1:43;
end;

theorem Th22:
for G be non-trivial RealNormSpace-Sequence,
    i be Element of dom G,
    x be Point of product G,
    r be Point of G.i holds
  reproj(i,x).r - x = reproj(i,0.(product G)).(r - proj(i).x) &
  x - reproj(i,x).r = reproj(i,0.(product G)).(proj(i).x - r)
proof
   let G be non-trivial RealNormSpace-Sequence,
       i be Element of dom G,
       x be Point of product G,
       r be Point of G.i;
    set m=len G;
   reconsider xf=x as Element of product carr G by Th10;
A1:dom carr G = dom G by Lm1;
   reconsider Zr = 0.(product G) as Element of product carr G by Th10;
   reconsider ixr = reproj(i,x).r as Element of product carr G by Th10;
   reconsider p = reproj(i,x).r - x as Element of product carr G by Th10;
A2:dom p = dom (carr G) by CARD_3:9;
   reconsider q = reproj(i,0.(product G)).(r - proj(i).x)
                    as Element of product carr G by Th10;
A3:dom q = dom (carr G) by CARD_3:9;
   reconsider s = x - reproj(i,x).r as Element of product carr G by Th10;
A4:dom s = dom (carr G) by CARD_3:9;
   reconsider t = reproj(i,0.(product G)).(proj(i).x - r)
                   as Element of product carr G by Th10;
A5:dom t = dom carr G by CARD_3:9;
A6: reproj(i,x).r = x +* (i,r) by Def4;
   reconsider xfi =xf.i as Point of G.i;
   reproj(i,0.(product G)).(r - proj(i).x)
              = 0.(product G) +* (i,(r - proj(i).x)) by Def4; then
A7:
   q = Zr +* (i,(r- xfi)) by Def3;
   reproj(i,0.(product G)).(proj(i).x -r)
            = 0.(product G) +* (i,(proj(i).x - r)) by Def4; then
A8:
   t = Zr +* (i,(xfi -r)) by Def3;
   set ir= i .--> r;
   set irx1= (i .--> (r- xfi));
   set irx2= (i .--> (xfi - r));
    x in the carrier of product G; then
A9: x in product carr G by Th10;
    consider g1 be Function such that
A10:  x = g1 & dom g1 = dom carr G
    & for i be set st i in dom carr G holds g1.i in (carr G).i
        by A9,CARD_3:def 5;
   for k be set st k in dom p holds p.k = q.k
   proof
    let k be set;
    assume A11: k in dom p; then
    reconsider k0=k as Element of dom G by A1,CARD_3:9;
    consider g be Function such that
A12:  Zr = g & dom g = dom carr G
    & for i be set st i in dom carr G holds g.i in (carr G).i
        by CARD_3:def 5;
A13: k in dom Zr by A12,A11,CARD_3:9;
A14: k in dom x by A10,A11,CARD_3:9;
    per cases;
    suppose not k in {i}; then
A15:   k <> i by TARSKI:def 1; then
A16: q.k0 = Zr.k0 by A7,FUNCT_7:32;
     p.k = ixr.k0 -xf.k0 by Th15
        .= xf.k0 -xf.k0 by A15,A6,FUNCT_7:32; then
     p.k =0.(G.k0) by RLVECT_1:15;
     hence p.k = q.k by A16,Th14;
    end;
    suppose k in {i}; then
A17: k=i by TARSKI:def 1; then
A18: q.k0 = r- xfi by A7,A13,FUNCT_7:31;
     p.k=ixr.k0 -xf.k0 by Th15;
     hence p.k = q.k by A18,A6,A17,A14,FUNCT_7:31;
    end;
   end;
   hence reproj(i,x).r - x = reproj(i,0.(product G)).(r - proj(i).x)
     by A2,A3,FUNCT_1:2;
   for k be set st k in dom s holds s.k = t.k
   proof
    let k be set;
    assume A19: k in dom s; then
    reconsider k0=k as Element of dom G by A1,CARD_3:9;
    consider g be Function such that
A20:   Zr = g & dom g = dom carr G
    & for i be set st i in dom carr G holds g.i in (carr G).i
        by CARD_3:def 5;
A21: k in dom Zr by A20,A19,CARD_3:9;
A22: k in dom x by A10,A19,CARD_3:9;
    per cases;
    suppose not k in {i}; then
A23:   k <> i by TARSKI:def 1; then
A24: t.k0 = Zr.k0 by A8,FUNCT_7:32;
     s.k= xf.k0 - ixr.k0 by Th15
       .=xf.k0 -xf.k0 by A6,A23,FUNCT_7:32; then
     s.k =0.(G.k0) by RLVECT_1:15;
     hence s.k = t.k by A24,Th14;
    end;
    suppose k in {i}; then
A25: k=i by TARSKI:def 1; then
A26: t.k0 = xfi-r by A8,A21,FUNCT_7:31;
     s.k=xf.k0 - ixr.k0 by Th15;
     hence s.k = t.k by A26,A6,A25,A22,FUNCT_7:31;
    end;
   end;
   hence thesis by A4,A5,FUNCT_1:2;
end;

theorem Th23:
for G be non-trivial RealNormSpace-Sequence,
    i be Element of dom G,
    x be Point of product G,
    Z be Subset of product G
      st Z is open & x in Z holds
ex N be Neighbourhood of proj(i).x st
  for z be Point of G.i st z in N holds (reproj(i,x)).z in Z
proof
   let G be non-trivial RealNormSpace-Sequence,
       i be Element of dom G,
       x be Point of product G,
       Z be Subset of product G;
   assume Z is open & x in Z; then
   consider r be Real such that
A1: 0 < r & {y where y is Point of product G : ||. y - x .|| < r} c= Z
      by NDIFF_1:3;
   set N = {y where y is Point of G.i : ||. y - proj(i).x .|| < r};
   reconsider N as Neighbourhood of proj(i).x by A1,NFCONT_1:3;
   take N;
   thus for z be Point of G.i st z in N holds (reproj(i,x)).z in Z
   proof
    let z be Point of G.i;
    assume z in N; then
A2: ex y be Point of G.i st y = z & ||. y - proj(i).x .|| < r;
    ||. (reproj(i,x)).z - x .||
      = ||. reproj(i,0.(product G)).(z - proj(i).x) .|| by Th22
     .= ||. z - proj(i).x .|| by Th21; then
    (reproj(i,x)).z
     in {y where y is Point of product G : ||. y - x .|| < r} by A2;
    hence thesis by A1;
   end;
end;

theorem Th24:
 for G be non-trivial RealNormSpace-Sequence,
     T be non trivial RealNormSpace,
     i be set,
     f be PartFunc of product G, T,
     Z be Subset of product G
       st Z is open holds
   f is_partial_differentiable_on Z,i
iff
   Z c=dom f &
   for x be Point of product G st x in Z holds
     f is_partial_differentiable_in x,i
proof
   let G be non-trivial RealNormSpace-Sequence,
       T be non trivial RealNormSpace,
       i be set,
       f be PartFunc of product G, T,
       Z be Subset of (product G);
   assume
A1: Z is open;

   set i0=modetrans(G,i);
   set S=G.i0;
   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 product G st x in Z holds
           f is_partial_differentiable_in x,i
   proof
    assume A2: f is_partial_differentiable_on Z,i;
    hence A3: Z c=dom f by Def8;
    let nx0 be Point of product G;
    reconsider x0=proj(i0).nx0 as Point of S;
    assume A4: nx0 in Z; then
    f|Z is_partial_differentiable_in nx0,i by A2,Def8; then
    (f|Z)*reproj(i0,nx0) is_differentiable_in x0 by Def6; then
    consider N0 being Neighbourhood of x0 such that
A5:  N0 c= dom((f|Z)*reproj(i0,nx0)) and
A6:  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(i0,nx0))/.x-((f|Z)*reproj(i0,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
A7:  for x be Point of S st x in N0 holds
      ((f|Z)*reproj(i0,nx0))/.x - ((f|Z)*reproj(i0,nx0))/.x0
        = L.(x-x0) + R/.(x-x0) by A6;
    consider N1 being Neighbourhood of x0 such that
A8:  for x be Point of S st x in N1 holds
      (reproj(i0,nx0)).x in Z by A1,A4,Th23;
A9:now let x be Point of S;
     assume x in N1; then
     (reproj(i0,nx0)).x in Z by A8; then
     (reproj(i0,nx0)).x in (dom f) /\ Z by A3,XBOOLE_0:def 4;
     hence (reproj(i0,nx0)).x in dom(f|Z) by RELAT_1:61;
    end;
    reconsider N = N0 /\ N1 as Neighbourhood of x0 by Th8;
    (f|Z)*reproj(i0,nx0) c= f*reproj(i0,nx0) by RELAT_1:29,59; then
A10:dom((f|Z)*reproj(i0,nx0)) c= dom(f*reproj(i0,nx0)) by RELAT_1:11;
    N c= N0 by XBOOLE_1:17; then
    N c= dom((f|Z)*reproj(i0,nx0)) by A5,XBOOLE_1:1; then
A11:N c= dom(f*reproj(i0,nx0)) by A10,XBOOLE_1:1;
    now let x be Point of S;
     assume A12: x in N; then
A13: x in N0 by XBOOLE_0:def 4;
A14: dom(reproj(i0,nx0)) = the carrier of G.i0 by FUNCT_2:def 1;

     x in N1 by A12,XBOOLE_0:def 4; then
A15: (reproj(i0,nx0)).x in dom(f|Z) by A9; then
A16: (reproj(i0,nx0)).x in dom f &
      (reproj(i0,nx0)).x in Z by RELAT_1:57;
A17: (reproj(i0,nx0)).x0 in dom(f|Z) by A9,NFCONT_1:4; then
A18: (reproj(i0,nx0)).x0 in dom f &
      (reproj(i0,nx0)).x0 in Z by RELAT_1:57;

A19: ((f|Z)*reproj(i0,nx0))/.x
       =(f|Z)/.(reproj(i0,nx0)/.x) by A15,A14,PARTFUN2:4
      .= f/. (reproj(i0,nx0)/.x) by A16,PARTFUN2:17
      .= (f*reproj(i0,nx0))/.x by A14,A16,PARTFUN2:4;
     ((f|Z)*reproj(i0,nx0))/.x0
       =(f|Z)/. (reproj(i0,nx0)/.x0 ) by A14,A17,PARTFUN2:4
      .= f/. (reproj(i0,nx0)/.x0) by A18,PARTFUN2:17
      .= (f*reproj(i0,nx0))/.x0 by A14,A18,PARTFUN2:4;
     hence (f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0 =L.(x-x0)+R/.(x-x0)
       by A7,A13,A19;
    end; then
    f*reproj(i0,nx0) is_differentiable_in x0 by A11,NDIFF_1:def 6;
    hence f is_partial_differentiable_in nx0,i by Def6;
   end;
   assume that
A20:Z c=dom f and
A21:for nx be Point of product G st nx in Z holds
     f is_partial_differentiable_in nx,i;
    now let nx0 be Point of product G;
    assume A22: nx0 in Z; then
A23:f is_partial_differentiable_in nx0,i by A21;
    reconsider x0=proj(i0).nx0 as Point of S;

    f*reproj(i0,nx0) is_differentiable_in x0 by A23,Def6; then
    consider N0 being Neighbourhood of x0 such that
     N0 c= dom (f*reproj(i0,nx0)) and
A24: 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(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0
         = L.(x-x0)+R  /.(x-x0) by NDIFF_1:def 6;

    consider N1 being Neighbourhood of x0 such that
A25: for x be Point of S st x in N1 holds
       (reproj(i0,nx0)).x in Z by A1,A22,Th23;

A26:now let x be Point of S;
     assume x in N1; then
     (reproj(i0,nx0)).x in Z by A25; then
     (reproj(i0,nx0)).x in (dom f) /\ Z by A20,XBOOLE_0:def 4;
     hence (reproj(i0,nx0)).x in dom(f|Z) by RELAT_1:61;
    end;

A27:N1 c= dom((f|Z)*reproj(i0,nx0))
    proof
     let z be set;
     assume A28:z in N1; then
A29: z in the carrier of S;
     reconsider x=z as Point of S by A28;
A30: (reproj(i0,nx0)).x in dom(f|Z) by A28,A26;
     z in dom (reproj(i0,nx0)) by A29,FUNCT_2:def 1;
     hence z in dom((f|Z)*reproj(i0,nx0)) by A30,FUNCT_1:11;
    end;
    reconsider N=N0 /\ N1 as Neighbourhood of x0 by Th8;
    N c= N1 by XBOOLE_1:17; then
A31:N c= dom((f|Z)*reproj(i0,nx0)) by A27,XBOOLE_1:1;

    consider L be Point of RNS,R be RestFunc of S,T such that
A32: for x be Point of S st x in N0 holds
      (f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0=L.(x-x0)+R/.(x-x0) by A24;
    now let x be Point of S;
     assume A33: x in N; then
A34: x in N0 by XBOOLE_0:def 4;
A35: dom (reproj(i0,nx0)) = the carrier of G.i0 by FUNCT_2:def 1;
     x in N1 by A33,XBOOLE_0:def 4; then
A36: (reproj(i0,nx0)).x in dom(f|Z) by A26; then
A37: (reproj(i0,nx0)).x in dom f /\ Z by RELAT_1:61; then
A38: (reproj(i0,nx0)).x in dom f by XBOOLE_0:def 4;

A39: (reproj(i0,nx0)).x0 in dom(f|Z) by A26,NFCONT_1:4; then
A40: (reproj(i0,nx0)).x0 in dom f /\ Z by RELAT_1:61; then
A41: (reproj(i0,nx0)).x0 in dom f by XBOOLE_0:def 4;

A42: ((f|Z)*reproj(i0,nx0))/.x
       = (f|Z)/.(reproj(i0,nx0)/.x) by A36,A35,PARTFUN2:4
      .= f/.(reproj(i0,nx0)/.x) by A37,PARTFUN2:16
      .= (f*reproj(i0,nx0))/.x by A35,A38,PARTFUN2:4;
     ((f|Z)*reproj(i0,nx0))/.x0
       = (f|Z)/. (reproj(i0,nx0)/.x0 ) by A35,A39,PARTFUN2:4
      .= f/. (reproj(i0,nx0)/.x0) by A40,PARTFUN2:16
      .= (f*reproj(i0,nx0))/.x0 by A35,A41,PARTFUN2:4;
     hence ((f|Z)*reproj(i0,nx0))/.x -((f|Z)*reproj(i0,nx0))/.x0
             = L.(x-x0)+R/.(x-x0) by A42,A34,A32;
    end; then
    (f|Z)*reproj(i0,nx0) is_differentiable_in x0 by A31,NDIFF_1:def 6;
    hence (f|Z) is_partial_differentiable_in nx0,i by Def6;
   end;
   hence thesis by A20,Def8;
end;

theorem Th25:
for i be set st i in dom G & f is_partial_differentiable_on X,i
  holds X is Subset of product G
proof
   let i be set;
   assume i in dom G & f is_partial_differentiable_on X,i; then
   X c=dom f by Def8;
   hence thesis by XBOOLE_1:1;
end;

definition
  let G be non-trivial RealNormSpace-Sequence;
  let S be non trivial RealNormSpace;
  let i be set;
  assume A1: i in dom G;
  let f be PartFunc of product G, S;
  let X be set;
  assume A2: f is_partial_differentiable_on X,i;
 func f `partial|(X,i) -> PartFunc of product G,
  R_NormSpace_of_BoundedLinearOperators(G.modetrans(G,i),S) means
:Def9:
  dom it = X &
  for x be Point of product G st x in X holds it/.x = partdiff(f,x,i);
existence
proof
   deffunc F(Element of product G) = partdiff(f,$1,i);
   defpred P[Element of product G] means $1 in X;
   consider F being PartFunc of product G,
    R_NormSpace_of_BoundedLinearOperators(G.modetrans(G,i),S) such that
A3: (for x be Point of product G holds x in dom F iff P[x]) & for x be
    Point of product G st x in dom F holds F.x = F(x) from SEQ_1:sch 3;
   take F;
   now
A4: X is Subset of product G by A2,A1,Th25;
    let y be set;
    assume y in X;
    hence y in dom F by A3,A4;
   end; then
A5:X c= dom F by TARSKI:def 3;

   for y be set st y in dom F holds y in X by A3; then
   dom F c= X by TARSKI:def 3;
   hence dom F = X by A5,XBOOLE_0:def 10;
   hereby let x be Point of product G;
    assume x in X; then
A6: x in dom F by A3; then
    F.x = partdiff(f,x,i) by A3;
    hence F/.x = partdiff(f,x,i) by A6,PARTFUN1:def 6;
   end;
end;
uniqueness
proof
   let F,H be PartFunc of product G,
            R_NormSpace_of_BoundedLinearOperators(G.modetrans(G,i),S);
   assume that
A7: dom F = X and
A8: for x be Point of product G st x in X holds F/.x = partdiff(f,x,i) and
A9: dom H = X and
A10: for x be Point of product G st x in X holds H/.x = partdiff(f,x,i);
   now let x be Point of product G;
    assume A11: x in dom F; then
    F/.x = partdiff(f,x,i) by A7,A8;
    hence F/.x=H/.x by A7,A10,A11;
   end;
   hence thesis by A7,A9,PARTFUN2:1;
end;
end;

theorem Th26:
for i be set st i in dom G holds
  (f1+f2)*reproj(modetrans(G,i),x) = f1*reproj(modetrans(G,i),x)
                                    +f2*reproj(modetrans(G,i),x)
& (f1-f2)*reproj(modetrans(G,i),x) = f1*reproj(modetrans(G,i),x)
                            -f2*reproj(modetrans(G,i),x)
proof
   let i0 be set;
   assume i0 in dom G;
   set i=modetrans(G,i0);

A1:dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1;
A2:dom(f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
   for s be Element of G.i holds s in dom((f1+f2)*reproj(i,x))
    iff s in dom(f1*reproj(i,x)+f2*reproj(i,x))
   proof
    let s be Element of G.i;
    s in dom((f1+f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2
      by A2,A1,FUNCT_1:11; then
    s in dom((f1+f2)*reproj(i,x))
     iff reproj(i,x).s in dom f1 & reproj(i,x).s in dom f2
       by XBOOLE_0:def 4; then
    s in dom((f1+f2)*reproj(i,x))
     iff s in dom(f1*reproj(i,x)) & s in dom(f2*reproj(i,x))
       by A1,FUNCT_1:11; then
    s in dom((f1+f2)*reproj(i,x))
     iff s in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by XBOOLE_0:def 4;
    hence thesis by VFUNCT_1:def 1;
   end; then
   for s be set holds s in dom((f1+f2)*reproj(i,x))
     iff s in dom(f1*reproj(i,x) + f2*reproj(i,x)); then
A3:dom((f1+f2)*reproj(i,x)) = dom(f1*reproj(i,x)+f2*reproj(i,x)) by TARSKI:1;
A4:for z being Element of G.i st z in dom((f1+f2)*reproj(i,x)) holds
    ((f1+f2)*reproj(i,x)).z = (f1*reproj(i,x)+f2*reproj(i,x)).z
   proof
    let z be Element of G.i;
    assume A5: z in dom((f1+f2)*reproj(i,x)); then
A6: reproj(i,x).z in dom(f1+f2) by FUNCT_1:11;

    z in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x))
      by A3,A5,VFUNCT_1:def 1; then
A7: z in dom(f1*reproj(i,x)) & z in dom(f2*reproj(i,x)) by XBOOLE_0:def 4;

A8: reproj(i,x).z in dom f1 /\ dom f2 by A2,A5,FUNCT_1:11; then
    reproj(i,x).z in dom f1 by XBOOLE_0:def 4; then
A9:f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by PARTFUN1:def 6
      .=(f1*reproj(i,x)).z by A7,FUNCT_1:12
      .=(f1*reproj(i,x))/.z by A7,PARTFUN1:def 6;

    reproj(i,x).z in dom f2 by A8,XBOOLE_0:def 4; then
A10:f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by PARTFUN1:def 6
      .=(f2*reproj(i,x)).z by A7,FUNCT_1:12
      .=(f2*reproj(i,x))/.z by A7,PARTFUN1:def 6;

    ((f1+f2)*reproj(i,x)).z = (f1+f2).(reproj(i,x).z) by A5,FUNCT_1:12
      .=(f1+f2)/.(reproj(i,x).z) by A6,PARTFUN1:def 6
      .= f1/.(reproj(i,x).z) +f2/.(reproj(i,x).z) by A6,VFUNCT_1:def 1
      .=(f1*reproj(i,x)+ f2*reproj(i,x))/.z by A3,A5,A9,A10,VFUNCT_1:def 1;
    hence thesis by A3,A5,PARTFUN1:def 6;
   end;

A11:
   dom(f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
   for s be Element of G.i holds s in dom((f1-f2)*reproj(i,x))
     iff s in dom(f1*reproj(i,x)-f2*reproj(i,x))
   proof
    let s be Element of G.i;
    s in dom((f1-f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2
      by A11,A1,FUNCT_1:11; then
    s in dom((f1-f2)*reproj(i,x))
      iff reproj(i,x).s in dom f1 & reproj(i,x).s in dom f2
        by XBOOLE_0:def 4; then
    s in dom((f1-f2)*reproj(i,x))
      iff s in dom(f1*reproj(i,x)) & s in dom(f2*reproj(i,x))
        by A1,FUNCT_1:11; then
    s in dom((f1-f2)*reproj(i,x))
      iff s in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by XBOOLE_0:def 4;
    hence thesis by VFUNCT_1:def 2;
   end; then
   for s be set holds s in dom((f1-f2)*reproj(i,x))
     iff s in dom(f1*reproj(i,x) - f2*reproj(i,x)); then
A12:
   dom((f1-f2)*reproj(i,x)) = dom(f1*reproj(i,x)-f2*reproj(i,x)) by TARSKI:1;
   for z being Element of G.i st z in dom((f1-f2)*reproj(i,x)) holds
    ((f1-f2)*reproj(i,x)).z = (f1*reproj(i,x)-f2*reproj(i,x)).z
   proof
    let z be Element of G.i;
    assume A13: z in dom((f1-f2)*reproj(i,x)); then
A14:reproj(i,x).z in dom (f1-f2) by FUNCT_1:11;
    z in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x))
      by A12,A13,VFUNCT_1:def 2; then
A15:z in dom(f1*reproj(i,x)) & z in dom(f2*reproj(i,x)) by XBOOLE_0:def 4;
A16:reproj(i,x).z in dom f1 /\ dom f2 by A11,A13,FUNCT_1:11; then
    reproj(i,x).z in dom f1 by XBOOLE_0:def 4; then
A17:f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by PARTFUN1:def 6
      .=(f1*reproj(i,x)).z by A15,FUNCT_1:12
      .=(f1*reproj(i,x))/.z by A15,PARTFUN1:def 6;

    reproj(i,x).z in dom f2 by A16,XBOOLE_0:def 4; then
A18:f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by PARTFUN1:def 6
      .=(f2*reproj(i,x)).z by A15,FUNCT_1:12
      .=(f2*reproj(i,x))/.z by A15,PARTFUN1:def 6;
    thus ((f1-f2)*reproj(i,x)).z =(f1-f2).(reproj(i,x).z) by A13,FUNCT_1:12
      .=(f1-f2)/.(reproj(i,x).z) by A14,PARTFUN1:def 6
      .= f1/.(reproj(i,x).z) - f2/.(reproj(i,x).z) by A14,VFUNCT_1:def 2
      .=(f1*reproj(i,x)- f2*reproj(i,x))/.z by A12,A13,A17,A18,VFUNCT_1:def 2
      .=(f1*reproj(i,x)- f2*reproj(i,x)).z by A12,A13,PARTFUN1:def 6;
   end;
   hence thesis by A3,A12,A4,PARTFUN1:5;
end;

theorem Th27:
for i be set st i in dom G holds
  r(#)(f*reproj(modetrans(G,i),x)) = (r(#)f)*reproj(modetrans(G,i),x)
proof
   let i0 be set;
   assume i0 in dom G;
   set i=modetrans(G,i0);
A1:dom(r(#)f) = dom f by VFUNCT_1:def 4;
A2:dom(r(#)(f*reproj(i,x))) =dom(f*reproj(i,x)) by VFUNCT_1:def 4;
A3:dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1;
   for s be Element of G.i holds s in dom((r(#)f)*reproj(i,x))
     iff s in dom(f*reproj(i,x))
   proof
    let s be Element of G.i;
    s in dom((r(#)f)*reproj(i,x)) iff reproj(i,x).s in dom(r(#)f)
      by A3,FUNCT_1:11;
    hence thesis by A1,A3,FUNCT_1:11;
   end; then
   for s be set holds s in dom(r(#)(f*reproj(i,x)))
     iff s in dom((r(#)f)*reproj(i,x)) by A2; then
A4:dom(r(#)(f*reproj(i,x))) =dom((r(#)f)*reproj(i,x)) by TARSKI:1;
A5:for s be Element of G.i holds s in dom((r(#)f)*reproj(i,x))
     iff reproj(i,x).s in dom(r(#)f)
   proof
    let s be Element of G.i;
    dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1;
    hence thesis by FUNCT_1:11;
   end;
   for z being Element of G.i st z in dom(r(#)(f*reproj(i,x))) holds
    (r(#)(f*reproj(i,x))).z = ((r(#)f)*reproj(i,x)).z
   proof
    let z be Element of G.i;
    assume A6: z in dom(r(#)(f*reproj(i,x))); then
A7: z in dom(f*reproj(i,x)) by VFUNCT_1:def 4;

A8: reproj(i,x).z in dom f by A1,A5,A4,A6; then
A9: f/.(reproj(i,x).z) = f.(reproj(i,x).z) by PARTFUN1:def 6
      .= (f*reproj(i,x)).z by A7,FUNCT_1:12
      .= (f*reproj(i,x))/.z by A7,PARTFUN1:def 6;

A10:(r(#)(f*reproj(i,x))).z =(r(#)(f*reproj(i,x)))/.z by A6,PARTFUN1:def 6
      .= r * f/.(reproj(i,x).z) by A6,A9,VFUNCT_1:def 4;
    ((r(#)f)*reproj(i,x)).z = (r(#)f).(reproj(i,x).z) by A4,A6,FUNCT_1:12
      .= (r(#)f)/.(reproj(i,x).z) by A1,A8,PARTFUN1:def 6
      .= r * f/.(reproj(i,x).z) by A1,A8,VFUNCT_1:def 4;
    hence thesis by A10;
   end;
   hence thesis by A4,PARTFUN1:5;
end;

theorem
for i be set st i in dom G
  & f1 is_partial_differentiable_in x,i
  & f2 is_partial_differentiable_in x,i
  holds f1+f2 is_partial_differentiable_in x,i
   & partdiff(f1+f2,x,i)=partdiff(f1,x,i)+partdiff(f2,x,i)
proof
   let i0 be set;
   set i=modetrans(G,i0);
   assume A1: i0 in dom G; then
A2:(f1+f2)*reproj(i,x) = f1*reproj(i,x)+f2*reproj(i,x) by Th26;
   assume
A3: f1 is_partial_differentiable_in x,i0 &
    f2 is_partial_differentiable_in x,i0;
A4:f1*reproj(i,x) is_differentiable_in proj(i).x &
   f2*reproj(i,x) is_differentiable_in proj(i).x by A3,Def6; then
   (f1+f2)*reproj(i,x) is_differentiable_in proj(i).x by A2,NDIFF_1:35;
   hence f1+f2 is_partial_differentiable_in x,i0 by Def6;
   thus
    partdiff(f1,x,i0)+partdiff(f2,x,i0)
    = diff(f1*reproj(i,x)+f2*reproj(i,x),proj(i).x) by A4,NDIFF_1:35
    .= partdiff((f1+f2),x,i0) by A1,Th26;
end;

theorem
for i be set st i in dom G
  & f1 is_partial_differentiable_in x,i
  & f2 is_partial_differentiable_in x,i
 holds f1-f2 is_partial_differentiable_in x,i
     & partdiff(f1-f2,x,i)=partdiff(f1,x,i)-partdiff(f2,x,i)
proof
   let i0 be set;
   assume A1: i0 in dom G;
   set i=modetrans(G,i0);
   assume f1 is_partial_differentiable_in x,i0
        & f2 is_partial_differentiable_in x,i0; then
A2:f1*reproj(i,x) is_differentiable_in proj(i).x
 & f2*reproj(i,x) is_differentiable_in proj(i).x by Def6;
   (f1-f2)*reproj(i,x) = f1*reproj(i,x)-f2*reproj(i,x) by A1,Th26; then
   (f1-f2)*reproj(i,x) is_differentiable_in proj(i).x by A2,NDIFF_1:36;
   hence f1-f2 is_partial_differentiable_in x,i0 by Def6;
   thus partdiff(f1,x,i0)-partdiff(f2,x,i0)
     = diff(f1*reproj(i,x)-f2*reproj(i,x),proj(i).x) by A2,NDIFF_1:36
     .= partdiff((f1-f2),x,i0) by A1,Th26;
end;

theorem
for i be set st i in dom G
  & f is_partial_differentiable_in x,i
 holds r(#)f is_partial_differentiable_in x,i & partdiff((r(#)f),x,i)
          = r*partdiff(f,x,i)
proof
   let i0 be set;
   assume A1: i0 in dom G;
   set i=modetrans(G,i0);
   assume f is_partial_differentiable_in x,i0; then
A2:f*reproj(i,x) is_differentiable_in proj(i).x by Def6;
   r(#)(f*reproj(i,x)) = (r(#)f)*reproj(i,x) by A1,Th27; then
   (r(#)f)*reproj(i,x) is_differentiable_in proj(i).x by A2,NDIFF_1:37;
   hence r(#)f is_partial_differentiable_in x,i0 by Def6;
   thus partdiff(r(#)f,x,i0) = diff(r(#)(f*reproj(i,x)),proj(i).x) by A1,Th27
    .= r*partdiff(f,x,i0) by A2,NDIFF_1:37;
end;

begin :: Continuously differentiable and Partial derivative

theorem Th31:
 ||. proj(i).x .|| <= ||.x.||
proof
   reconsider y= x as Element of product carr G by Th10;
   proj(i).x = y.i by Def3;
   hence thesis by PRVECT_2:10;
end;

registration
  let G be non-trivial RealNormSpace-Sequence;
  cluster -> (len G)-element for Point of product G;
  coherence
  proof
    let x be Point of product G;
A1: the carrier of (product G) = product carr G by Th10;
A2: dom x = dom (carr G)
    & for i be set st i in dom (carr G) holds x.i in carr G.i by A1,CARD_3:9;
    len carr G = len G by PRVECT_2:def 4; then
    dom x= Seg len G by A2,FINSEQ_1:def 3; then
    len x = len G by FINSEQ_1:def 3;
    hence thesis by CARD_1:def 7;
  end;
end;

theorem Th32:
for G be non-trivial RealNormSpace-Sequence,
    T be non trivial RealNormSpace,
    i be set,
    Z be Subset of product G,
    f be PartFunc of product G,T
      st Z is open holds
  f is_partial_differentiable_on Z,i
      iff
  Z c=dom f &
  for x be Point of product G st x in Z holds
    f is_partial_differentiable_in x,i
proof
   let G be non-trivial RealNormSpace-Sequence,
       T be non trivial RealNormSpace,
       i0 be set,
       Z be Subset of product G,
       f be PartFunc of product G,T;
   assume
A1: Z is open;
   set i = modetrans(G,i0);
   set S=G.i;
   set RNS= R_NormSpace_of_BoundedLinearOperators(S,T);
   hereby
    assume A2: f is_partial_differentiable_on Z,i0;
    hence A3: Z c=dom f by Def8;
    let nx0 be Point of product G;
    reconsider x0=proj(i).nx0 as Point of S;
    assume A4: nx0 in Z; then
    f|Z is_partial_differentiable_in nx0,i0 by A2,Def8; then
    (f|Z)*reproj(i,nx0) is_differentiable_in x0 by Def6; then
    consider N0 being Neighbourhood of x0 such that
A5:  N0 c= dom((f|Z)*reproj(i,nx0)) and
A6:  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
A7:  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 A6;

    consider N1 being Neighbourhood of x0 such that
A8:  for x be Point of S st x in N1 holds
      (reproj(i,nx0)).x in Z by A1,A4,Th23;

A9:now let x be Point of S;
     assume x in N1; then
     (reproj(i,nx0)).x in Z by A8; then
     (reproj(i,nx0)).x in (dom f) /\ Z by A3,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 Th8;
    (f|Z)*reproj(i,nx0) c= f*reproj(i,nx0) by RELAT_1:29,59; then
A10: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 A5,XBOOLE_1:1; then
A11:N c= dom(f*reproj(i,nx0)) by A10,XBOOLE_1:1;
A12:dom(reproj(i,nx0)) = the carrier of G.i by FUNCT_2:def 1;
    now let x be Point of S;
     assume x in N; then
A13: x in N0 & x in N1 by XBOOLE_0:def 4; then
A14: (reproj(i,nx0)).x in dom(f|Z) by A9; then
A15: (reproj(i,nx0)).x in dom f & (reproj(i,nx0)).x in Z by RELAT_1:57;

A16: (reproj(i,nx0)).x0 in dom(f|Z) by A9,NFCONT_1:4; then
A17: (reproj(i,nx0)).x0 in dom f & (reproj(i,nx0)).x0 in Z by RELAT_1:57;

A18: ((f|Z)*reproj(i,nx0))/.x
       = (f|Z)/.(reproj(i,nx0)/.x) by A14,A12,PARTFUN2:4
      .= f/.(reproj(i,nx0)/.x) by A15,PARTFUN2:17
      .= (f*reproj(i,nx0))/.x by A12,A15,PARTFUN2:4;

      ((f|Z)*reproj(i,nx0))/.x0
       = (f|Z)/.(reproj(i,nx0)/.x0) by A12,A16,PARTFUN2:4
      .= f/.(reproj(i,nx0)/.x0) by A17,PARTFUN2:17
      .= (f*reproj(i,nx0))/.x0 by A12,A17,PARTFUN2:4;
     hence (f*reproj(i,nx0))/.x-(f*reproj(i,nx0))/.x0 =L.(x-x0)+R/.(x-x0)
       by A7,A13,A18;
    end; then
    f*reproj(i,nx0) is_differentiable_in x0 by A11,NDIFF_1:def 6;
    hence f is_partial_differentiable_in nx0,i0 by Def6;
   end;

   assume that
A19:Z c=dom f and
A20:for nx be Point of product G  st nx in Z holds
      f is_partial_differentiable_in nx,i0;
   now let nx0 be Point of product G;
    assume A21: nx0 in Z; then
A22:f is_partial_differentiable_in nx0,i0 by A20;
    reconsider x0=proj(i).nx0 as Point of S;

    f*reproj(i,nx0) is_differentiable_in x0 by A22,Def6; then
    consider N0 being Neighbourhood of x0 such that
     N0 c= dom (f*reproj(i,nx0)) and
A23: 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 being Neighbourhood of x0 such that
A24: for x be Point of S st x in N1 holds
      (reproj(i,nx0)).x in Z by A1,A21,Th23;

A25:now let x be Point of S;
     assume x in N1; then
     (reproj(i,nx0)).x in Z by A24; then
     (reproj(i,nx0)).x in (dom f) /\ Z by A19,XBOOLE_0:def 4;
     hence (reproj(i,nx0)).x in dom(f|Z) by RELAT_1:61;
    end;

A26:N1 c= dom((f|Z)*reproj(i,nx0))
    proof
     let z be set;
     assume A27:z in N1; then
     z in the carrier of S; then
A28: z in dom (reproj(i,nx0)) by FUNCT_2:def 1;

     reconsider x=z as Point of S by A27;
     (reproj(i,nx0)).x in dom(f|Z) by A27,A25;
     hence z in dom((f|Z)*reproj(i,nx0)) by A28,FUNCT_1:11;
    end;

    reconsider N=N0 /\ N1 as Neighbourhood of x0 by Th8;

    N c= N1 by XBOOLE_1:17; then
A29:N c= dom((f|Z)*reproj(i,nx0)) by A26,XBOOLE_1:1;

    consider L be Point of RNS,R be RestFunc of S,T such that
A30: 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 A23;

    now let x be Point of S;
     assume A31: x in N; then
A32: x in N0 by XBOOLE_0:def 4;

A33: dom (reproj(i,nx0)) = the carrier of G.i by FUNCT_2:def 1;

     x in N1 by A31,XBOOLE_0:def 4; then
A34: (reproj(i,nx0)).x in dom(f|Z) by A25; then
A35: (reproj(i,nx0)).x in dom f /\ Z by RELAT_1:61; then
A36: (reproj(i,nx0)).x in dom f by XBOOLE_0:def 4;

A37: (reproj(i,nx0)).x0 in dom(f|Z) by A25,NFCONT_1:4; then
A38: (reproj(i,nx0)).x0 in dom f /\ Z by RELAT_1:61; then
A39: (reproj(i,nx0)).x0 in dom f by XBOOLE_0:def 4;

A40: ((f|Z)*reproj(i,nx0))/.x
       = (f|Z)/. (reproj(i,nx0)/.x ) by A34,A33,PARTFUN2:4
      .= f/. (reproj(i,nx0)/.x) by A35,PARTFUN2:16
      .= (f*reproj(i,nx0))/.x by A33,A36,PARTFUN2:4;
     ((f|Z)*reproj(i,nx0))/.x0
       = (f|Z)/. (reproj(i,nx0)/.x0 ) by A33,A37,PARTFUN2:4
      .= f/. (reproj(i,nx0)/.x0) by A38,PARTFUN2:16
      .= (f*reproj(i,nx0))/.x0 by A33,A39,PARTFUN2:4;
     hence ((f|Z)*reproj(i,nx0))/.x -((f|Z)*reproj(i,nx0))/.x0
             = L.(x-x0)+R/.(x-x0) by A40,A32,A30;
    end; then
    (f|Z)*reproj(i,nx0) is_differentiable_in x0 by A29,NDIFF_1:def 6;
    hence (f|Z) is_partial_differentiable_in nx0,i0 by Def6;
   end;
   hence thesis by A19,Def8;
end;

theorem Th33:
 for i,j be Element of dom G,
     x be Point of G.i,
     z be Element of product carr G
      st z= reproj(i,0.(product G)).x
holds
  (i = j implies z.j = x) & (i <> j implies z.j = 0.(G.j))
proof
   let i,j be Element of dom G,
       x be Point of G.i,
       z be Element of product carr G;
   assume A1: z= reproj(i,0.(product G)).x;
   reconsider Zr = 0.(product G) as Element of product carr G by Th10;
   reconsider ixr = (reproj(i,0.(product G))).x
             as Element of product carr G by Th10;
A2:reproj(i,0.(product G)).x = 0.(product G) +* (i,x) by Def4;
   set ix= i .--> x;
   consider g be Function such that
A3:   Zr = g & dom g = dom carr G
    & for i be set st i in dom carr G holds g.i in (carr G).i
        by CARD_3:def 5;
A4:dom Zr = dom G by A3,Lm1;
   now assume i <> j; then
    z.j = Zr.j by A1,A2,FUNCT_7:32;
    hence z.j = 0.(G.j) by Th14;
   end;
   hence thesis by A1,A2,A4,FUNCT_7:31;
end;

theorem Th34:
for x,y be Point of G.i
 holds reproj(i,0.(product G)).(x+y)
   = reproj(i,0.(product G)).x + reproj(i,0.(product G)).y
proof
   let x,y be Point of G.i;
   reconsider v=reproj(i,0.(product G)).(x+y) as Element of product carr G
     by Th10;
   reconsider s=reproj(i,0.(product G)).x as Element of product carr G
     by Th10;
   reconsider t=reproj(i,0.(product G)).y as Element of product carr G
     by Th10;
   for j be Element of dom G holds v.j=s.j + t.j
   proof
    let j be Element of dom G;
    per cases;
    suppose A1: i= j; then
     reconsider yy=y as Point of G.j;
     v.j = x+y by Th33,A1; then
     v.j =s.j + yy by Th33,A1;
     hence v.j =s.j + t.j by Th33,A1;
    end;
    suppose A2: i <> j; then
     v.j = 0.(G.j) by Th33; then
     v.j = 0.(G.j) + 0.(G.j) by RLVECT_1:def 4; then
     v.j =s.j + 0.(G.j) by Th33,A2;
     hence v.j =s.j + t.j by Th33,A2;
    end;
   end;
   hence thesis by Th12;
end;

theorem Th35:
for x,y be Point of product G
 holds proj(i).(x+y) = proj(i).x + proj(i).y
proof
   let x,y be Point of product G;
   reconsider v=x+y as Element of product carr G by Th10;
   reconsider s=x as Element of product carr G by Th10;
   reconsider t=y as Element of product carr G by Th10;
   proj(i).(x+y)= v.i & proj(i).x = s.i & proj(i).y = t.i by Def3;
   hence thesis by Th12;
end;

theorem
for x,y be Point of G.i
 holds reproj(i,0.(product G)).(x-y)
   = reproj(i,0.(product G)).x - reproj(i,0.(product G)).y
proof
   let x,y  be Point of G.i;
   reconsider v=reproj(i,0.(product G)).(x-y) as Element of product carr G
     by Th10;
   reconsider s=reproj(i,0.(product G)).x as Element of product carr G
     by Th10;
   reconsider t=reproj(i,0.(product G)).y as Element of product carr G
     by Th10;

   for j be Element of dom G holds v.j=s.j - t.j
   proof
    let j be Element of dom G;
    per cases;
    suppose A1: i= j; then
     reconsider yy=y as Point of G.j;
     v.j = x-y by Th33,A1; then
     v.j =s.j - yy by Th33,A1;
     hence v.j =s.j - t.j by Th33,A1;
    end;
    suppose A2: i <> j; then
     v.j = 0.(G.j) by Th33; then
     v.j = 0.(G.j) - 0.(G.j) by RLVECT_1:13; then
     v.j =s.j - 0.(G.j) by Th33,A2;
     hence v.j =s.j - t.j by Th33,A2;
    end;
   end;
   hence thesis by Th15;
end;

theorem Th37:
for x,y be Point of product G
 holds proj(i).(x-y) = proj(i).x - proj(i).y
proof
   let x,y be Point of product G;
   reconsider v=x-y as Element of product carr G by Th10;
   reconsider s=x as Element of product carr G by Th10;
   reconsider t=y as Element of product carr G by Th10;
   proj(i).(x-y)= v.i & proj(i).x = s.i & proj(i).y = t.i by Def3;
   hence thesis by Th15;
end;

theorem Th38:
for x be Point of G.i st x <> 0.(G.i)
 holds reproj(i,0.(product G)).x <> 0.(product G)
proof
   let x be Point of G.i;
   assume A1: x <> 0.(G.i);
   assume A2: reproj(i,0.(product G)).x = 0.(product G);
   reconsider v=reproj(i,0.(product G)).x as Element of product carr G
     by Th10;
   x = v.i by Th33;
   hence contradiction by A1,Th14,A2;
end;

theorem Th39:
for x be Point of G.i, a be Element of REAL
 holds reproj(i,0.(product G)).(a*x)
   = a*(reproj(i,0.(product G)).x)
proof
   let x  be Point of G.i,a be Element of REAL;
   reconsider v=reproj(i,0.(product G)).(a*x) as Element of product carr G
     by Th10;
   reconsider s=reproj(i,0.(product G)).x as Element of product carr G
     by Th10;

   for j be Element of dom G holds v.j=a*(s.j)
   proof
    let j be Element of dom G;
    per cases;
    suppose A1: i= j; then
     v.j = a*x by Th33;
     hence v.j =a*(s.j) by Th33,A1;
    end;
    suppose A2: i <> j; then
     v.j = 0.(G.j) by Th33; then
     v.j = a*0.(G.j) by RLVECT_1:10;
     hence v.j =a*(s.j) by Th33,A2;
    end;
   end;
   hence thesis by Th13;
end;

theorem Th40:
for x be Point of product G,a be Element of REAL
 holds proj(i).(a*x) = a*(proj(i).x)
proof
   let x be Point of product G,a  be Element of REAL;
   reconsider v=a*x as Element of product carr G by Th10;
   reconsider s=x as Element of product carr G by Th10;
   proj(i).(a*x)= v.i & proj(i).x = s.i by Def3;
   hence thesis by Th13;
end;

theorem Th41:
 for G be non-trivial RealNormSpace-Sequence,
      S be non trivial RealNormSpace,
      f be PartFunc of product G, S,
      x be Point of product G,
      i be set
  st f is_differentiable_in x holds
    f is_partial_differentiable_in x,i
  & partdiff(f,x,i) = diff(f,x) * reproj(modetrans(G,i),0.(product G))
proof
   let G be non-trivial RealNormSpace-Sequence,
       S be non trivial RealNormSpace,
       f be PartFunc of product G, S,
       x be Point of product G,
       i0 be set;
   assume
A1: f is_differentiable_in x;
   set i=modetrans(G,i0);

   consider N being Neighbourhood of x such that
A2: N c= dom f &
    ex R be RestFunc of product G,S st
     for y be Point of product G  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 product G,S such that
A3: for y be Point of product G  st y in N holds
     f/.y-f/.x = diff(f,x).(y-x) + R/.(y-x) by A2;

   consider r0 be Real such that
A4: 0 < r0 &
    {z where z is Point of product G  : ||. z-x .|| < r0} c= N
      by NFCONT_1:def 1;

   set u = f*reproj(i,x);
   reconsider x0 = proj(i).x as Point of G.i;
   set Z=0.(product G);
   set Nx0 = {z where z is Point of G.i: ||. z-x0 .|| < r0 };
   now let s be set;
    assume s in Nx0; then
    ex z be Point of G.i st s=z & ||. z-x0 .|| < r0;
    hence s in the carrier of G.i;
   end; then
   Nx0 is Subset of G.i by TARSKI:def 3; then
   reconsider Nx0 as Neighbourhood of x0 by A4,NFCONT_1:def 1;

A5:for xi be Element of G.i st xi in Nx0 holds reproj(i,x).xi in N
   proof
    let xi be Element of G.i;
    assume xi in Nx0; then
A6: ex z be Point of G.i st xi=z & ||. z-x0 .|| < r0;
    reproj(i,x).xi-x = reproj(i,Z).(xi-x0) by Th22; then
    ||. reproj(i,x).xi-x .|| < r0 by Th21,A6; then
    reproj(i,x).xi in {z where z is Point of product G : ||. z-x .|| < r0 };
    hence thesis by A4;
   end;

A7:R is total by NDIFF_1:def 5; then
A8:dom R = the carrier of product G by PARTFUN1:def 2;
   reconsider R1 = R*reproj(i,0.(product G)) as PartFunc of G.i,S;
A9:
   dom(reproj(i,0.(product G))) = the carrier of G.i by FUNCT_2:def 1;

A10:
   dom R1 = the carrier of G.i by A7,PARTFUN1:def 2;

   for r be Real st r > 0
    ex d be Real st d > 0 &
     for z be Point of G.i st z <> 0.(G.i) & ||.z.|| < d
      holds (||.z.||"  * ||. R1/.z .||) < r
   proof
    let r be Real;
    assume r > 0; then
    consider d be Real such that
A11: d > 0 &
     for z be Point of product G  st z <> 0.(product G ) & ||.z.|| < d
      holds (||.z.||"  * ||. R/.z .||) < r by A7,NDIFF_1:23;
    take d;
    now let z be Point of G.i;
     assume A12: z <> 0.(G.i) & ||.z.|| < d;
A13: ||. reproj(i,Z).z .|| = ||.z.|| by Th21;

     R/.(reproj(i,Z).z) = R.(reproj(i,Z).z) by A8,PARTFUN1:def 6; then
     R/.(reproj(i,Z).z) =R1.z by A9,FUNCT_1:13; then
     R/.(reproj(i,Z).z) =R1/.z by A10,PARTFUN1:def 6;
     hence ||.z.||" * ||. R1/.z .|| < r by A11,A13,A12,Th38;
    end;
    hence thesis by A11;
   end; then
   reconsider R1 as RestFunc of G.i,S by A7,NDIFF_1:23;

   reconsider dfx = diff(f,x)
      as Lipschitzian LinearOperator of product G,S by LOPBAN_1:def 9;
   reconsider LD1 = dfx*reproj(i,0.(product G )) as Function of G.i,S;
A14:
   now let x,y be Element of G.i;
    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 Th34; 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 G.i, 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 Th39; 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 G.i,S
     by A14,VECTSP_1:def 20,LOPBAN_1:def 5;

   consider K0 being Real such that
A15:  0 <= K0 & for x being
   VECTOR of product G holds ||. dfx.x .|| <= K0 * ||. x .||
      by LOPBAN_1:def 8;

   now let r being  VECTOR of G.i;
    ||. dfx.(reproj(i,Z).r) .|| <= K0 * ||. reproj(i,Z).r .|| by A15; then
    ||. dfx.(reproj(i,Z).r ) .|| <= K0 * ||.r.|| by Th21;
    hence ||. LD1.r .|| <= K0 * ||.r.|| by FUNCT_2:15;
   end; then
   LD1 is Lipschitzian by A15,LOPBAN_1:def 8; then
   reconsider LD1 as Point of
     R_NormSpace_of_BoundedLinearOperators(G.i,S) by LOPBAN_1:def 9;
   now let s be set;
    assume s in (reproj(i,x)).:Nx0; then
    ex t being Element of G.i st
      t in Nx0 & s = (reproj(i,x)).t by FUNCT_2:65; then
    s in N by A5;
    hence s in dom f by A2;
   end; then
A16:
   (reproj(i,x)).:Nx0 c= dom f by TARSKI:def 3;
   dom(reproj(i,x)) = the carrier of G.i by FUNCT_2:def 1; then
A17:
   Nx0 c= dom u by A16,FUNCT_3:3;
A18:
   for y be Point of G.i st y in Nx0 holds
     u/.y-u/.x0 = LD1.(y-x0) + R1/.(y-x0)
   proof
    let y be Point of G.i;
    assume A19: y in Nx0; then
A20:reproj(i,x).y in N by A5;
A21:  reproj(i,x).x0 = x +* (i,x0) by Def4;
A22:  the carrier of (product G) = product carr G by Th10;
    x.i=x0 by Def3,A22; then
A23:x= x +* (i,x0) by FUNCT_7:35;
A24:reproj(i,x).x0 in N by A5,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,A2,PARTFUN1:def 6;
    R/.(reproj(i,Z).(y-x0)) = R.(reproj(i,Z).(y-x0))
       by A8,PARTFUN1:def 6; then
    R/.(reproj(i,Z).(y-x0)) = R1.(y-x0) by A9,FUNCT_1:13; then
A26:R/.(reproj(i,Z).(y-x0)) = R1/.(y-x0) by A10,PARTFUN1:def 6;
    x0 in Nx0 by NFCONT_1:4; then
    u/.x0 = u.x0 by A17,PARTFUN1:def 6; then
    u/.x0 = f.(reproj(i,x).x0) by FUNCT_2:15; then
    u/.y-u/.x0 = f/.(reproj(i,x).y) -f/.x
       by A25,A23,A24,A2,A21,PARTFUN1:def 6; then
    u/.y-u/.x0 = diff(f,x).(reproj(i,x).y-x) + R/.(reproj(i,x).y-x)
      by A3,A19,A5; then
    u/.y-u/.x0 = dfx.(reproj(i,Z).(y-x0)) + R/.(reproj(i,x).y-x) by Th22; then
    u/.y-u/.x0 = dfx.(reproj(i,Z).(y-x0)) + R/.(reproj(i,Z).(y-x0)) by Th22;
    hence u/.y-u/.x0 = LD1.(y-x0) +  R1/.(y-x0) by A26,FUNCT_2:15;
   end; then
A27: u is_differentiable_in x0 by A17,NDIFF_1:def 6;
   hence f is_partial_differentiable_in x,i0 by Def6;
   thus thesis by A27,A17,A18,NDIFF_1:def 7;
end;

Lm5:
for G be non-trivial RealNormSpace-Sequence,
    S be non trivial RealNormSpace,
    f be PartFunc of product G,S, x be Point of product G
 ex L be Lipschitzian LinearOperator of product G,S
    st
  for h be Element of product G
   ex w be FinSequence of S st
     dom w = Seg len G
   & (for i be Element of NAT st i in Seg len G  holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).h) )
   & L.h=Sum w
proof
   let G be non-trivial RealNormSpace-Sequence,
       S be non trivial RealNormSpace,
       f be PartFunc of product G,S,
       x be Point of product G;
   set m=len G;
   defpred LX[set,set] means
     ex w be FinSequence of S st
       dom w = Seg m
     & (for i be Element of NAT st i in Seg m holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).$1) )
     & $2=Sum w;

A1:for v being Element of product G holds
    ex y be Element of S st LX[v,y]
   proof
    let v being Element of product G;

    defpred YX[set,set] means
     ex i be Element of NAT st i=$1 &
     $2 = partdiff(f,x,i).(proj(modetrans(G,i)).v);

A2: for i be Nat st i in Seg m holds ex r being Element of S st YX[i,r]
    proof
     let i be Nat;
     assume i in Seg m;
     reconsider i0=i as Element of NAT by ORDINAL1:def 12;
     partdiff(f,x,i0).(proj(modetrans(G,i0)).v) in the carrier of S;
     hence thesis;
    end;

    consider w be FinSequence of S 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 Element of NAT;
     assume i in Seg m; then
     YX[i,w.i] by A3;
     hence w.i = partdiff(f,x,i).(proj(modetrans(G,i)).v);
    end;

    reconsider w0 = Sum w as Element of S;
    ex w be FinSequence of S st
       dom w=Seg m
     & (for i be Element of NAT st i in Seg m holds
            w.i = partdiff(f,x,i).(proj(modetrans(G,i)).v))
     & w0 = Sum w by A4,A3;
    hence ex y0 be Element of S st LX[v,y0];
   end;

   consider L being Function of product G,S such that
A5: for h being Element of product G holds LX[h,L.h] from FUNCT_2:sch 3(A1);

A6:for s,t being Element of product G holds L.(s+t) = L.s + L.t
   proof
    let s,t being Element of product G;
    consider w be FinSequence of S such that
A7:  dom w=Seg m
   & (for i be Element of NAT st i in Seg m holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).s))
   & L.s = Sum w by A5;
    consider v be FinSequence of S such that
A8:  dom v=Seg m
   & (for i be Element of NAT st i in Seg m holds
          v.i = partdiff(f,x,i).(proj(modetrans(G,i)).t ))
   & L.t = Sum v by A5;
    consider u be FinSequence of S such that
A9:  dom u=Seg m
   & (for i be Element of NAT st i in Seg m holds
          u.i = partdiff(f,x,i).(proj(modetrans(G,i)).(s+t)))
   & L.(s+t) = Sum u by A5;

A10: len w = m by A7,FINSEQ_1:def 3;
A11: len v = m by A8,FINSEQ_1:def 3;
A12: len u = m by A9,FINSEQ_1:def 3;

    now let i be Element of NAT;
     assume A13: i in dom w; then
A14: 1 <= i & i <= m by A7,FINSEQ_1:1; then
     w/.i = w.i by A10,FINSEQ_4:15; then
A15: w/.i = partdiff(f,x,i).(proj(modetrans(G,i)).s) by A7,A13;

     v/.i = v.i by A14,A11,FINSEQ_4:15; then
A16: v/.i = partdiff(f,x,i).(proj(modetrans(G,i)).t) by A7,A8,A13;

A17:  partdiff(f,x,i) is Lipschitzian LinearOperator of G.(modetrans(G,i)),S
        by LOPBAN_1:def 9;

     u.i = partdiff(f,x,i).(proj(modetrans(G,i)).(s+t)) by A7,A9,A13; then
     u.i = partdiff(f,x,i).(proj(modetrans(G,i)).s + proj(modetrans(G,i)).t)
                 by Th35;
     hence u.i = w/.i + v/.i by A15,A16,A17,VECTSP_1:def 20;
    end;
    hence L.(s+t) = L.s + L.t by A9,A7,A8,A10,A11,A12,RLVECT_2:2;
   end;

   for s being Element of product G, r being Real holds L.(r*s) = r*(L.s)
   proof
    let s being Element of product G, r being Real;

    consider w be FinSequence of S such that
A18: dom w = Seg m
   & (for i be Element of NAT st i in Seg m holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).s))
   & L.s = Sum w by A5;

    consider u be FinSequence of S such that
A19: dom u = Seg m
   & (for i be Element of NAT st i in Seg m holds
          u.i = partdiff(f,x,i).(proj(modetrans(G,i)).(r*s)) )
   & L.(r*s) = Sum u by A5;

A20: len w = m & len u = m by A18,A19,FINSEQ_1:def 3;
    now let i be Element of NAT;
     assume A21: i in dom w; then
     1 <= i & i <= m by A18,FINSEQ_1:1; then
     w/.i = w.i by A20,FINSEQ_4:15; then
A22: w/.i = partdiff(f,x,i).(proj(modetrans(G,i)).s ) by A18,A21;

A23:  partdiff(f,x,i) is Lipschitzian LinearOperator of G.(modetrans(G,i)),S
         by LOPBAN_1:def 9;

     u.i = partdiff(f,x,i).(proj(modetrans(G,i)).(r*s)) by A18,A19,A21; then
     u.i = partdiff(f,x,i).(r*proj(modetrans(G,i)).s) by Th40;
     hence u.i = r*(w/.i) by A22,A23,LOPBAN_1:def 5;
    end;
    hence L.(r*s) = r * L.s by A18,A19,A20,RLVECT_2:3;
   end; then
   reconsider L as LinearOperator of product G,S
       by A6,VECTSP_1:def 20,LOPBAN_1:def 5;

   defpred YXL[set,set] means
     ex i be Element of NAT st i=$1 & $2 = ||. partdiff(f,x,i) .||;

A24:
   for i be Nat st i in Seg m holds ex r being Element of REAL st YXL[i,r]
   proof
    let i be Nat;
    assume i in Seg m;
    reconsider i0=i as Element of NAT by ORDINAL1:def 12;
    reconsider r = ||. partdiff(f,x,i0) .|| as Element of REAL;
    YXL[i,r];
    hence thesis;
   end;

   consider Kw be FinSequence of REAL such that
A25: dom Kw=Seg m
  & for i be Nat st i in Seg m holds YXL[i,Kw.i] from FINSEQ_1:sch 5(A24);

A26:now let i be Element of NAT;
     assume i in Seg m; then
     YXL[i,Kw.i] by A25;
     hence Kw.i = ||. partdiff(f,x,i) .||;
    end;

A27:
   now let i be Nat;
    assume i in dom Kw; then
    Kw.i = ||. partdiff(f,x,i) .|| by A26,A25;
    hence 0 <= Kw.i;
   end;

   set LK= Sum Kw;
A28:
   0 <= LK by A27,RVSUM_1:84;

   for s being Element of product G holds ||. L.s .|| <= LK*||. s .||
   proof
    let s being Element of product G;
    consider w be FinSequence of S such that
A29:  dom w=Seg m
   & (for i be Element of NAT st i in Seg m holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).s))
   & L.s = Sum w by A5;

    defpred YXD[set,set] means
     ex i be Element of NAT st i=$1 & $2 = ||.partdiff(f,x,i).|| * ||.s.||;

A30:for i be Nat st i in Seg m holds ex r being Element of REAL st YXD[i,r]
    proof
     let i be Nat;
     assume i in Seg m;
     reconsider i0=i as Element of NAT by ORDINAL1:def 12;
     reconsider r = ||.partdiff(f,x,i0).|| * ||.s.|| as Element of REAL;
     YXD[i,r];
     hence thesis;
    end;

    consider Dw be FinSequence of REAL such that
A31:dom Dw=Seg m
   & for i be Nat st i in Seg m holds YXD[i,Dw.i] from FINSEQ_1:sch 5(A30);

A32:now let i be Element of NAT;
     assume i in Seg m; then
     YXD[i,Dw.i] by A31;
     hence Dw.i = ||.partdiff(f,x,i).|| * ||.s.||;
    end;

    defpred YXH[set,set] means
     ex i be Element of NAT st i=$1 & $2 = ||. w/.i .||;

A33:for i be Nat st i in Seg m holds ex r being Element of REAL st YXH[i,r]
    proof
     let i be Nat;
     assume i in Seg m;
     reconsider i0=i as Element of NAT by ORDINAL1:def 12;
     reconsider r = ||. w/.i0 .|| as Element of REAL;
     YXH[i,r];
     hence thesis;
    end;

    consider yseq be FinSequence of REAL such that
A34: dom yseq=Seg m
   & for i be Nat st i in Seg m holds YXH[i,yseq.i] from FINSEQ_1:sch 5(A33);

A35: now let i be Element of NAT;
     assume i in Seg m; then
     YXH[i,yseq.i] by A34;
     hence yseq.i = ||. w/.i .||;
    end;

    len w = len yseq by A29,A34,FINSEQ_3:29; then
A36: ||.L.s.|| <= Sum yseq by A29,A35,Th7;

    m = len yseq by A34,FINSEQ_1:def 3; then
A37: yseq is Element of m-tuples_on REAL by FINSEQ_2:92;

    len Dw = m by A31,FINSEQ_1:def 3; then
A38:Dw is Element of m-tuples_on REAL by FINSEQ_2:92;

    now let i be Nat;
     assume A39: i in Seg m; then
A40: yseq.i = ||. w/.i .|| by A35;

     w/.i = w.i by A39,A29,PARTFUN1:def 6; then
A41:  ||. w/.i .|| = ||.partdiff(f,x,i).(proj(modetrans(G,i)).s) .||
         by A29,A39;

     reconsider DF1=partdiff(f,x,i) as
       Lipschitzian LinearOperator of G.(modetrans(G,i)),S by LOPBAN_1:def 9;

A42:  ||. DF1.(proj(modetrans(G,i)).s) .||
        <= ||.partdiff(f,x,i).|| * ||.(proj(modetrans(G,i)).s) .||
            by LOPBAN_1:32;

     product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop
       G:], productnorm G #) by PRVECT_2:6; then
     reconsider ss= s as Element of product carr G;
     reconsider xi = proj(modetrans(G,i)).s  as Point of G.(modetrans(G,i));
     xi = ss.(modetrans(G,i)) by Def3; then
     ||.partdiff(f,x,i).|| * ||.(proj(modetrans(G,i)).s) .||
       <=||.partdiff(f,x,i).|| * ||.s.|| by PRVECT_2:10,XREAL_1:64; then
     ||. w/.i .|| <= ||.partdiff(f,x,i).|| * ||.s.|| by A41,A42,XXREAL_0:2;
     hence yseq.i <= Dw.i by A32,A39,A40;
    end; then
A43: Sum yseq <= Sum Dw by A37,A38,RVSUM_1:82;

    len Kw = m by A25,FINSEQ_1:def 3; then
    reconsider KKw= Kw as Element of m-tuples_on REAL by FINSEQ_2:92;
    (||.s.|| * KKw) in m-tuples_on REAL; then
    ex t be Element of REAL* st t= (||.s.|| * KKw) & len t = m; then
A44: dom Dw = dom (||.s.|| * Kw) by A31,FINSEQ_1:def 3;
    now let k be Nat;
     assume A45: k in dom Dw; then
     Dw.k = ||.partdiff(f,x,k).|| * ||.s.|| by A32,A31; then
     Dw.k = ||.s.|| * Kw.k by A26,A45,A31;
     hence Dw.k = (||.s.|| * Kw).k by RVSUM_1:45;
    end; then
    Dw = ||.s.|| * Kw by A44,FINSEQ_1:13; then
    Sum Dw = (Sum Kw)* ||.s.|| by RVSUM_1:87;
    hence thesis by A36,A43,XXREAL_0:2;
   end; then
   reconsider L as Lipschitzian LinearOperator of product G,S
   by A28,LOPBAN_1:def 8;
   take L;
   thus thesis by A5;
end;

theorem Th42:
for S be RealNormSpace, h,g be FinSequence of S
    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 S be RealNormSpace, h,g be FinSequence of S;
   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);

   consider F be Function of NAT, the carrier of S such that
A3:  Sum g = F.(len g) & F.0 = 0.S
  & for j be Element of NAT,v be Element of S
    st j < len g & v = g.(j + 1) holds F.(j + 1) = F.j + v
   by RLVECT_1:def 12;

   per cases;
   suppose len g = 0;
    hence thesis by A3,A1,RLVECT_1:15;
   end;
   suppose A4:len g > 0;
    defpred P[Nat] means $1 <= len g implies F.$1 = h/.1 - h/.($1+1);
A5: P[1]
    proof
     assume A6: 1 <= len g; then
     1 in Seg len g; then
A7:  1 in dom g by FINSEQ_1:def 3;
     reconsider zz0=0 as Element of NAT;
     g/.1 = g.( zz0 + 1 ) by A7,PARTFUN1:def 6; then
     F.(zz0 + 1) = F.0 + g/.1 by A3,A6
                .= g/.1 by A3,RLVECT_1:4;
     hence F.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 1 <= j;
     assume A9: P[j];
     assume A10:j+1 <= len g; then
A11: j < len g by NAT_1:13;
     1 <= j+1 by XREAL_1:38; then
A12: j+1 in dom g by A10,FINSEQ_3:25; then
A13: g.(j+1)=g/.(j+1) by PARTFUN1:def 6;
     j is Element of NAT by ORDINAL1:def 12; then
     F.(j+1) = F.j + g/.(j+1) by A13,A11,A3
            .=F.j + (h/.(j+1) - h/.(j+1+1)) by A2,A12
            .= h/.1 - h/.(j+1) + h/.(j+1) - h/.(j+1+1)
                  by A9,A10,NAT_1:13,RLVECT_1:28
            .= h/.1 -(h/.(j+1) - h/.(j+1)) - h/.(j+1+1) by RLVECT_1:29
            .= h/.1 -0.S - h/.(j+1+1) by RLVECT_1:15;
     hence thesis by RLVECT_1:13;
    end;
A14:1 <= len g by A4,NAT_1:14;
    for i be Nat st 1 <= i holds P[i] from NAT_1:sch 8(A5,A8);
    hence thesis by A3,A1,A14;
   end;
end;

theorem
for G be non-trivial RealNormSpace-Sequence,
    x,y be Element of product carr G, Z be set
 holds x +* (y|Z) is Element of product carr G by CARD_3:79;

theorem Th44:
for G be non-trivial RealNormSpace-Sequence,
    x,y be Point of product G,
    Z,x0 be Element of product carr G,
    X be set
  st Z=0.(product G) & x0=x & y= Z +* (x0|X)
 holds ||.y.|| <= ||.x.||
proof
   let G be non-trivial RealNormSpace-Sequence,
       x,y be Point of product G,
       Z,x0 be Element of product carr G,
       X be set;
   assume A1: Z=0.(product G) & x0=x & y= Z +* (x0|X);

   reconsider y0 = y as Element of product carr G by Th10;

A2: ||.y.|| = (productnorm G).y by PRVECT_2:def 13
           .= |. normsequence(G,y0) .| by PRVECT_2:def 12;

A3: ||.x.|| = (productnorm G).x by PRVECT_2:def 13
           .= |. normsequence(G,x0) .| by A1,PRVECT_2:def 12;

   reconsider Ny = normsequence(G,y0) as (len G)-element FinSequence of REAL;
   reconsider Nx = normsequence(G,x0) as (len G)-element FinSequence of REAL;

A4:len Nx = len G & len Ny = len G by CARD_1:def 7;

   for k be Element of NAT st k in Seg len Ny holds 0 <= Ny.k & Ny.k <= Nx.k
   proof
    let k be Element of NAT;
    assume A5: k in Seg len Ny; then
    reconsider k1 = k as Element of dom G by A4,FINSEQ_1:def 3;

    x0 is Element of the carrier of (product G) by Th10; then
    reconsider xx = x0 as (len G)-element FinSequence;
    dom xx = Seg len G by FINSEQ_1:89; then
A6: k in dom x0 by A5,CARD_1:def 7;

    reconsider yk = y0.k1, xk = x0.k1 as Element of the carrier of (G.k1);

A7: Nx.k = (the normF of G.k1).(x0.k1) by PRVECT_2:def 11;
A8: Ny.k = ||. yk .|| by PRVECT_2:def 11;
    hence 0 <= Ny.k;

A9: Nx.k = ||. xk .|| by PRVECT_2:def 11;

    per cases;
    suppose k1 in X; then
A10:  k1 in dom(x0|X) by A6,RELAT_1:57; then
     y0.k1 = (x0|X).k1 by A1,FUNCT_4:13; then
     y0.k1 = x0.k1 by A10,FUNCT_1:47;
     hence Ny.k <= Nx.k by A7,PRVECT_2:def 11;
    end;
    suppose not k1 in X; then
     not k1 in dom(x0|X); then
     y0.k1 = Z.k1 by A1,FUNCT_4:11; then
     y0.k1 = 0.(G.k1) by A1,Th14;
     hence Ny.k <= Nx.k by A8,A9;
    end;
   end;
   hence ||.y.|| <= ||.x.|| by A2,A3,A4,PRVECT_2:2;
end;

theorem Th45:
for G be non-trivial RealNormSpace-Sequence,
      S be non trivial RealNormSpace,
      f be PartFunc of product G, S,
      x,y be Point of product G
ex h be FinSequence of product G, g be FinSequence of S,
    Z,y0 be Element of product carr G st
    y0=y & Z = 0.(product G)
   & len h = len G + 1 & len g = len G  &
  (for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg (len G + 1-'i))) &
  (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 Point of product G st
    i in dom h & h/.i= hi holds ||. hi .|| <=||. y .||) &
  f /.(x+y) - f/.x = Sum g
proof
   let G be non-trivial RealNormSpace-Sequence,
       S be non trivial RealNormSpace,
       f be PartFunc of product G,S,
       x,y be Point of product G;
   set m= len G;
A1:
   the carrier of (product G) = product carr G by Th10;
   reconsider Z0 = 0.(product G) as Element of product carr G by Th10;
   reconsider y0 = y as Element of product carr G by Th10;
   reconsider y1=y as (len G)-element FinSequence;
   reconsider Z1=0.(product G) as (len G)-element FinSequence;

   len y1 = m by CARD_1:def 7; then
A2:dom y1 = dom G by FINSEQ_3:29;

   len Z1 = m by CARD_1:def 7; then
A3:dom Z1 = dom G by FINSEQ_3:29;

   defpred H[Nat,set] means $2=Z0 +* (y0| Seg (len G + 1-'$1));

A4:for k be Nat st k in Seg(m+1) ex x being Element of product G st H[k,x]
   proof
    let k be Nat;
    assume k in Seg(m+1);
    Z0 +* (y0| Seg (len G + 1-'k)) is Element of product carr G by CARD_3:79;
    hence thesis by A1;
   end;

   consider h be FinSequence of product G such that
A5: dom h = Seg(m+1) &
    for j being Nat st j in Seg(m+1) holds H[j,h.j] from FINSEQ_1:sch 5(A4);

A6:now let j being Nat;
    assume A7: j in dom h; then
    h/.j = h.j by PARTFUN1:def 6;
    hence h/.j = Z0 +* (y0| Seg (len G + 1-'j)) by A7,A5;
   end;

   deffunc Z(Nat)=f/.(x+h/.$1);
   consider z be FinSequence of S such that
A8: len z = m+1 &
    for j being Nat st j in dom z holds z.j = Z(j) from FINSEQ_2:sch 1;

A9:now let j being Nat;
    assume A10: j in dom z; then
    z/.j = z.j by PARTFUN1:def 6;
    hence z/.j = f/.(x+h/.j) by A10,A8;
   end;

   deffunc G(Nat) = z/.$1 - z/.($1+1);
   consider g be FinSequence of S such that
A11:len g = m &
    for j being Nat st j in dom g holds g.j = G(j) from FINSEQ_2:sch 1;

A12:now let j being Nat;
    assume A13: j in dom g; then
    g/.j = g.j by PARTFUN1:def 6;
    hence g/.j = z/.j - z /.(j+1) by A13,A11;
   end;

A14:m+1-'1 = m+1-1 by NAT_1:11,XREAL_1:233;

   reconsider zz0=0 as Element of NAT;
   1 <= m+1 by NAT_1:11; then
A15:1 in dom h by A5; then
   h/.1 = Z0 +* (y0| Seg (len G + 1-'1)) by A6
       .= Z0 +* (y0| dom G) by A14,FINSEQ_1:def 3
       .= Z0 +* y0 by A2,RELAT_1:69; then
A16:h/.1 = y by A2,A3,FUNCT_4:19;

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

   1 <= len z & len z <= m+1 by A8,NAT_1:14; then
A18:len z in dom h by A5; then
A19:h/.(len z) = Z0 +* (y0| Seg 0) by A6,A17,A8
             .= Z0 +* {}
             .=0.(product G);

A20:dom h= dom z by A5,A8,FINSEQ_1:def 3; then
A21:z/.1 = f/.(x+y) by A9,A16,A15;

   z/.(len z) = f/. (x+h/.(len z)) by A9,A20,A18; then
A22:z/.(len z) = f/.x by A19,RLVECT_1:def 4;

   take h,g,Z0,y0;

A23:now let i be Nat;
    assume A24: i in dom g; then
A25:i in Seg m by A11,FINSEQ_1:def 3; then
    1 <= i & i <= m by FINSEQ_1:1; then
A26:i+1 <= m+1 by XREAL_1:6;

    m <= m+1 by NAT_1:11; then
    Seg m c= Seg (m+1) by FINSEQ_1:5; then
A27:z/.i =f/.(x+h/.i) by A9,A5,A25,A20;

    1 <= i+1 by NAT_1:11; then
    i+1 in Seg (m+1) by A26; then
    i+1 in dom z by A8,FINSEQ_1:def 3; then
    z/.(i+1) =f /. (x+h/.(i+1)) by A9;
    hence g/.i = f /. (x+h/.i) - f /.(x+h/.(i+1)) by A12,A24,A27;
   end;

   now let i be Nat, hi be Element of product G;
    assume A28: i in dom h & h/.i= hi; then
    h/.i = Z0 +* (y0| Seg (len G + 1-'i)) by A6;
    hence ||. hi .|| <=||. y .|| by Th44,A28;
   end;
   hence thesis by A6,A21,A22,A23,A8,A12,Th42,A5,A11,FINSEQ_1:def 3;
end;

theorem Th46:
for G be non-trivial RealNormSpace-Sequence,
    i be Element of dom G,
    x,y be Point of product G,
    xi be Point of G.i
  st y = reproj(i,x).xi holds proj(i).y = xi
proof
   let G be non-trivial RealNormSpace-Sequence,
       i be Element of dom G, x,y be Point of product G,
       xi be Point of G.i;
   assume A1: y = reproj(i,x).xi;
A2:y = x +* (i,xi) by A1,Def4;
   x in the carrier of product G; then
   x in product carr G by Th10; then
   consider g being Function such that
A3:x = g & dom g = dom carr G &
    for y be set st y in dom carr G holds g.y in (carr G).y by CARD_3:def 5;
A4:i in dom G;
A5:i in dom x by Lm1,A4,A3;
   y is Element of product carr G by Th10; then
   proj(i).y = (x +* (i,xi)).i by A2,Def3;
   hence proj(i).y = xi by A5,FUNCT_7:31;
end;

theorem Th47:
for G be non-trivial RealNormSpace-Sequence, i be Element of dom G,
    y be Point of product G, q be Point of G.i
  st q = proj(i).y holds y = reproj(i,y).q
proof
   let G be non-trivial RealNormSpace-Sequence, i be Element of dom G,
       y be Point of product G, q be Point of G.i;
   assume A1: q = proj(i).y;
   reconsider z1 = reproj(i,y).q as (len G)-element FinSequence;
   reconsider z2 = y as (len G)-element FinSequence;
A2:dom z1 = Seg len G by FINSEQ_1:89 .= dom z2 by FINSEQ_1:89;
   for k be Nat st k in dom z1 holds z1.k = z2.k
   proof
    let k be Nat;
    assume k in dom z1;
    product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop
    G:], productnorm G #) by PRVECT_2:6; then
A3: q = y.i by A1,Def3;
    per cases;
    suppose A4: k = i; then
     (y +*(i,q)).k = q by A3,FUNCT_7:35;
     hence z1.k = z2.k by A4,A3,Def4;
    end;
    suppose k <> i; then
     (y +*(i,q)).k = y.k by FUNCT_7:32;
     hence z1.k = z2.k by Def4;
    end;
   end;
   hence thesis by A2,FINSEQ_1:13;
end;

theorem Th48:
for G be non-trivial RealNormSpace-Sequence,
    i be Element of dom G, x,y be Point of product G,
    xi be Point of G.i
  st y = reproj(i,x).xi holds reproj(i,x)=reproj(i,y)
proof
   let G be non-trivial RealNormSpace-Sequence,
       i be Element of dom G, x,y be Point of product G,
       xi be Point of G.i;
   assume A1: y = reproj(i,x).xi;
   for v be Element of G.i holds reproj(i,x).v = reproj(i,y).v
   proof
    let v be Element of G.i;
A2: reproj(i,x).v = x +* (i,v) & reproj(i,y).v = y +* (i,v) by Def4;
    reconsider xv = reproj(i,x).v, yv = reproj(i,y).v
       as (len G)-element FinSequence;
A3: dom xv = Seg len G & dom yv = Seg len G by FINSEQ_1:89; then
A4: dom xv = dom G by FINSEQ_1:def 3;

    for k be Nat st k in dom xv holds xv.k = yv.k
    proof
     let k be Nat;
     assume A5: k in dom xv;
     x in the carrier of product G & y in the carrier of product G; then
A6:  x in product carr G & y in product carr G by Th10; then
     consider g be Function such that
A7:   x = g & dom g = dom carr G
      & for i be set st i in dom carr G holds g.i in (carr G).i
        by CARD_3:def 5;
     consider g1 be Function such that
A8:   y = g1 & dom g1 = dom carr G
      & for i be set st i in dom carr G holds g1.i in (carr G).i
        by A6,CARD_3:def 5;
A9:  k in dom y & k in dom x by A7,A8,Lm1,A5,A4;
     per cases;
     suppose k = i; then
      (y +*(i,v)).k = v & (x +*(i,v)).k = v by A9,FUNCT_7:31;
      hence yv.k = xv.k by A2;
     end;
     suppose A10: k <> i;
A11:   yv.k = y.k & xv.k = x.k by A2,A10,FUNCT_7:32;
      y = x +* (i,xi) by A1,Def4;
      hence yv.k = xv.k by A11,A10,FUNCT_7:32;
      end;
     end;
     hence reproj(i,x).v = reproj(i,y).v by A3,FINSEQ_1:13;
    end;
    hence thesis by FUNCT_2:def 8;
end;

theorem Th49:
for G be non-trivial RealNormSpace-Sequence,
    i,j be Element of dom G, x,y be Point of product G,
    xi be Point of G.i
  st y = reproj(i,x).xi & i <> j holds proj(j).x = proj(j).y
proof
   let G be non-trivial RealNormSpace-Sequence,
       i,j be Element of dom G, x,y be Point of product G,
       xi be Point of G.i;
   assume A1: y = reproj(i,x).xi & i <> j;
   reconsider y1 = y as Element of product carr G by Th10;
A2:y = x +* (i,xi) by A1,Def4;
   set ix = i .--> xi;
A3:  the carrier of (product G) = product carr G by Th10;
   y1.j = x.j by A2,A1,FUNCT_7:32; then
   proj(j).y = x.j by Def3;
   hence thesis by A3,Def3;
end;

theorem
for  G be non-trivial RealNormSpace-Sequence,
     F be non trivial RealNormSpace,
     i be Element of dom G,
     x be Point of product G,
     xi be Point of G.i,
     f be PartFunc of product G,F,
     g be PartFunc of G.i,F
      st proj(i).x=xi & g=f*reproj(i,x)
 holds
    diff(g,xi) = partdiff(f,x,i)
proof
   let G be non-trivial RealNormSpace-Sequence,
       F be non trivial RealNormSpace,
       i be Element of dom G,
       x be Point of product G,
       xi be Point of G.i,
       f be PartFunc of product G,F,
       g be PartFunc of G.i,F;
   i=modetrans(G,i) by Def5;
   hence thesis;
end;

theorem Th51:
for G be non-trivial RealNormSpace-Sequence,
    F be non trivial RealNormSpace,
    f be PartFunc of product G,F,
    x be Point of product G,
    i be set,
    M be Real,
    L be Point of R_NormSpace_of_BoundedLinearOperators
             (G.(modetrans(G,i)),F),
    p,q be Point of G.(modetrans(G,i))
 st i in dom G
  & (for h be Point of G.(modetrans(G,i)) st h in ]. p,q .[ holds
       ||. partdiff(f,reproj(modetrans(G,i),x).h,i) - L  .|| <= M)
  & (for h be Point of G.(modetrans(G,i)) st h in [. p,q .] holds
       reproj(modetrans(G,i),x).h in dom f)
  & (for h be Point of G.(modetrans(G,i)) st h in [. p,q .] holds
       f is_partial_differentiable_in (reproj(modetrans(G,i),x).h),i)
holds
 ||.f/.(reproj(modetrans(G,i),x).q) - f/.(reproj(modetrans(G,i),x).p)
     - L.(q-p) .|| <= M * ||.q-p.||
proof
   let G be non-trivial RealNormSpace-Sequence,
       F be non trivial RealNormSpace,
       f be PartFunc of product G,F,
       x be Point of product G,
       i be set,
       M be Real,
       L be Point of R_NormSpace_of_BoundedLinearOperators
             (G.(modetrans(G,i)),F),
       p,q be Point of G.(modetrans(G,i));
   assume
A1: i in dom G
  & (for h be Point of G.(modetrans(G,i)) st h in ]. p,q .[ holds
       ||. partdiff(f,reproj(modetrans(G,i),x).h,i) - L .|| <= M)
  & (for h be Point of G.(modetrans(G,i)) st h in [. p,q .] holds
       reproj(modetrans(G,i),x).h in dom f )
  & (for h be Point of G.(modetrans(G,i)) st h in [. p,q .] holds
       f is_partial_differentiable_in (reproj(modetrans(G,i),x).h),i );

   set m=len G;
   set S=G.(modetrans(G,i));
   set g=f*reproj(modetrans(G,i),x);
A2:now let h be set;
    assume A3: h in [. p,q .]; then
    reconsider h1=h as Point of S;
A4: dom reproj(modetrans(G,i),x) = the carrier of S by FUNCT_2:def 1;
    reproj(modetrans(G,i),x).h1 in dom f by A1,A3;
    hence h in dom g by A4,FUNCT_1:11;
   end; then
A5:[. p,q .] c= dom g by TARSKI:def 3;
A6:now let x0 be Point of S;
    assume A7: x0 in [. p,q .];
    set y=reproj(modetrans(G,i),x).x0;
A8: proj(modetrans(G,i)).y = x0 by Th46;
    f is_partial_differentiable_in y,i by A1,A7; then
    f*reproj(modetrans(G,i),y) is_differentiable_in x0 by A8,Def6;
    hence g is_differentiable_in x0 by Th48;
   end;

   now let z be set;
    assume z in ].p,q.[; then
    consider z1 be Real such that A9: z=p+z1*(q-p) & 0 < z1 & z1 < 1;
    z = (1-z1)*p+z1*q by A9,Lm2; then
    z in {(1-r1)*p + r1*q where r1 is Real : 0 <= r1 & r1 <= 1 } by A9;
    hence z in [. p,q .] by RLTOPSP1:def 2;
   end; then
   ].p,q.[ c= [. p,q .] by TARSKI:def 3; then
A10:for x be Point of S st x in ].p,q.[ holds g is_differentiable_in x by A6;
A11:for x be Point of S st x in [.p,q.] holds g is_continuous_in x
      by A6,NDIFF_1:44;

A12:now let h be Point of S;
    set y=reproj(modetrans(G,i),x).h;
    assume h in ]. p,q .[; then
A13: ||. partdiff(f,y,i) - L .|| <= M by A1;
    proj(modetrans(G,i)).y = h by Th46;
    hence ||. diff(g,h) - L .|| <= M by A13,Th48;
   end;
A14:p in dom g & q in dom g by A2,RLTOPSP1:68;
   f/.(reproj(modetrans(G,i),x).p) = f/.(reproj(modetrans(G,i),x)/.p) &
   f/.(reproj(modetrans(G,i),x).q) = f/.(reproj(modetrans(G,i),x)/.q); then
   f/.(reproj(modetrans(G,i),x).p) = g/.p &
   f/.(reproj(modetrans(G,i),x).q) = g/.q by A14,PARTFUN2:3;
   hence ||.f/.(reproj(modetrans(G,i),x).q)
          - f/.(reproj(modetrans(G,i),x).p) - L.(q-p) .||
     <= M * ||.q-p.|| by A12,Th20,A5,A10,A11;
end;

theorem Th52:
for G be non-trivial RealNormSpace-Sequence,
    x,y,z,w be Point of product G,
    i be Element of dom G,
    d be Real,
    p,q,r be Point of G.i
  st ||. y-x .|| < d & ||. z-x .|| < d & p= proj(i).y & z=reproj(i,y).q
   & r in [. p,q .] & w= reproj(i,y).r
holds ||. w-x .|| < d
proof
   let G be non-trivial RealNormSpace-Sequence,
       x,y,z,w be Point of product G,
       i be Element of dom G,
       d be Real,
       p,q,r be Point of G.i;
   assume that
A1: ||. y-x .|| < d & ||. z-x .|| < d and
A2: p= proj(i).y & z=reproj(i,y).q and
A3: r in [. p,q .] and
A4: w= reproj(i,y).r;
   set wx = w-x;
   set yx = y-x;
   set zx = z-x;
   reconsider xi = proj(i).x as Point of G.i;
   r in {(1-t)*p + t*q where t is Real : 0 <= t & t <= 1 }
     by A3,RLTOPSP1:def 2; then
   consider t be Real such that
A5: r = (1-t)*p + t*q & 0 <= t & t <= 1;
A6: r = p + t*(q-p) & 0 <= t & t <= 1 by A5,Lm2;
   reconsider wx0 = wx, yx0 = yx, zx0 = zx
      as Element of product carr G by Th10;
   reconsider Nwx = normsequence(G,wx0) as (len G)-element FinSequence of REAL;
   reconsider Nyx = normsequence(G,yx0) as (len G)-element FinSequence of REAL;
   reconsider Nzx = normsequence(G,zx0) as (len G)-element FinSequence of REAL;
   set tyz = (1-t)*yx + t*zx;
   reconsider tyz0 = tyz as Element of product carr G by Th10;
   reconsider Ntyz = normsequence(G,tyz0)
      as (len G)-element FinSequence of REAL;

A7:1 = 1-t+t;

   r = p + (t*q - t*p) by A6,RLVECT_1:34
    .= (p + -t*p) + t*q by RLVECT_1:def 3
    .= (1*p - t*p) + t*q by RLVECT_1:def 8
    .= (1-t)*p + t*q by RLVECT_1:35; then
A8:r-xi = (1-t)*p + t*q - 1*xi by RLVECT_1:def 8
    .= (1-t)*p + t*q - ((1-t)*xi + t*xi) by A7,RLVECT_1:def 6
    .= (1-t)*p + t*q - t*xi - (1-t)*xi by RLVECT_1:27
    .= (1-t)*p +(t*q - t*xi) - (1-t)*xi by RLVECT_1:28
    .= (t*q - t*xi) + ((1-t)*p - (1-t)*xi) by RLVECT_1:def 3
    .= t*(q-xi) + ((1-t)*p - (1-t)*xi) by RLVECT_1:34
    .= t*(q-xi) + (1-t)*(p-xi) by RLVECT_1:34;

   reconsider Swx = wx as (len G)-element FinSequence;
   reconsider Syz = (1-t)*yx + t*zx as (len G)-element FinSequence;
A9:dom Swx = Seg len G & dom Syz = Seg len G by FINSEQ_1:89;
A10:for k be Nat st k in dom Swx holds Swx.k = Syz.k
   proof
    let k be Nat;
    assume k in dom Swx; then
    reconsider k0 = k as Element of dom G by A9,FINSEQ_1:def 3;
    per cases;
    suppose A11: k = i; then
     Swx.k = proj(i).wx0 by Def3; then
A12:  Swx.k = proj(i).w - proj(i).x by Th37;

A13:  proj(i).z = q by A2,Th46;
     Syz.k = proj(i).tyz0 by A11,Def3; then
     Syz.k = proj(i).((1-t)*yx) + proj(i).(t*zx) by Th35; then
     Syz.k = (1-t)*(proj(i).yx) + proj(i).(t*zx) by Th40; then
     Syz.k = (1-t)*(proj(i).yx) + t*proj(i).zx by Th40; then
     Syz.k = (1-t)*(proj(i).y - proj(i).x) + t*proj(i).zx by Th37; then
     Syz.k = (1-t)*(p-xi) + t*(q-xi) by A2,A13,Th37;
     hence Swx.k = Syz.k by A12,A8,A4,Th46;
    end;
    suppose k <> i; then
A14:  proj(k0).y = proj(k0).w & proj(k0).z = proj(k0).y by A2,A4,Th49;

     Swx.k = proj(k0).wx0 by Def3; then
A15:  Swx.k = proj(k0).w - proj(k0).x by Th37;
     Syz.k = proj(k0).tyz0 by Def3
          .= proj(k0).((1-t)*yx) + proj(k0).(t*zx) by Th35
          .= (1-t)*(proj(k0).yx) + proj(k0).(t*zx) by Th40
          .= (1-t)*(proj(k0).yx) + t*proj(k0).zx by Th40; then
     Syz.k = (1-t)*(proj(k0).y - proj(k0).x) + t*proj(k0).zx by Th37; then
     Syz.k = (1-t)*(proj(k0).y - proj(k0).x) + t*(proj(k0).y - proj(k0).x)
        by A14,Th37; then
     Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x
             + t*(proj(k0).y - proj(k0).x) by RLVECT_1:34; then
     Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x
             + (t*proj(k0).y - t*proj(k0).x) by RLVECT_1:34; then
     Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x
             + t*proj(k0).y - t*proj(k0).x by RLVECT_1:def 3; then
     Syz.k = (1-t)*proj(k0).y
             - ((1-t)*proj(k0).x - t*proj(k0).y)
             - t*proj(k0).x by RLVECT_1:29; then
     Syz.k = (1-t)*proj(k0).y
             + (t*proj(k0).y + - (1-t)*proj(k0).x)
             - t*proj(k0).x by RLVECT_1:33; then
     Syz.k = (1-t)*proj(k0).y
             + t*proj(k0).y + - (1-t)*proj(k0).x
             - t*proj(k0).x by RLVECT_1:def 3; then
     Syz.k = ((1-t)+t)*proj(k0).y
             + - (1-t)*proj(k0).x
             - t*proj(k0).x by RLVECT_1:def 6; then
     Syz.k = proj(k0).y
             + - (1-t)*proj(k0).x
             - t*proj(k0).x by RLVECT_1:def 8; then
     Syz.k = proj(k0).y
             + (- (1-t)*proj(k0).x - t*proj(k0).x) by RLVECT_1:28; then
     Syz.k = proj(k0).y
             + (- (t*proj(k0).x + (1-t)*proj(k0).x)) by RLVECT_1:30; then
     Syz.k = proj(k0).y
             + (- (t+(1-t))*proj(k0).x) by RLVECT_1:def 6;
     hence Swx.k = Syz.k by A15,A14,RLVECT_1:def 8;
    end;
   end;
A16:len Nwx = len G & len Ntyz = len G by CARD_1:def 7;
   for k be Element of NAT st k in Seg len Nwx
    holds 0 <= Nwx.k & Nwx.k <= Ntyz.k
   proof
    let k be Element of NAT;
    assume A17: k in Seg len Nwx; then
    reconsider k1 = k as Element of dom G by A16,FINSEQ_1:def 3;
    reconsider wxk = wx0.k1 as Element of (G.k1);
A18: Nwx.k = ||. wxk .|| by PRVECT_2:def 11;
    wx0.k1 = Syz.k by A10,A17,A16,A9;
    hence thesis by A18,PRVECT_2:def 11;
   end; then
A19: |. Nwx .| <= |. Ntyz .| by A16,PRVECT_2:2;
A20: ||. w-x .|| = (productnorm G).wx by PRVECT_2:def 13;
    ||. (1-t)*yx + t*zx .|| = (productnorm G).tyz by PRVECT_2:def 13
              .= |. normsequence(G,tyz0) .| by PRVECT_2:def 12; then
A21: ||. w-x .|| <= ||. (1-t)*yx + t*zx .|| by A19,A20,PRVECT_2:def 12;
A22: ||. (1-t)*yx + t*zx .|| <= abs(1-t)*||. y-x .|| + abs(t)*||. z-x .||
       by NORMSP_1:5;
   1-t >= 0 by A6,XREAL_1:48; then
A23:abs(1-t) = 1-t & abs t = t by A6,ABSVALUE:def 1;
   abs(1-t)*||. y-x .|| + abs(t)*||. z-x .|| < d
   proof
    per cases;
    suppose t=1 or t=0;
     hence thesis by A1,A23;
    end;
    suppose t<>1 & t<>0; then
     0 < t & t < 1 by A6,XXREAL_0:1; then
     0 < t & 1-t > 0 by XREAL_1:50; then
     abs(1-t)*||. y-x .|| < (1-t)*d & abs(t)*||. z-x .|| < t*d
       by A1,A23,XREAL_1:68; then
     abs(1-t)*||. y-x .|| + abs(t)*||. z-x .|| < (1-t)*d + t*d by XREAL_1:8;
     hence thesis;
    end;
   end; then
   ||. (1-t)*yx + t*zx .|| < d by A22,XXREAL_0:2;
   hence ||. w-x .|| < d by A21,XXREAL_0:2;
end;

theorem Th53:
for G be non-trivial RealNormSpace-Sequence,
    S be non trivial RealNormSpace,
    f be PartFunc of product G,S,
    X be Subset of product G,
    x,y,z be Point of product G,
    i be set,
    p,q be Point of G.(modetrans(G,i)),
    d,r be Real
 st i in dom G & X is open & x in X &
    ||. y-x .|| < d & ||. z-x .|| < d & X c= dom f &
    (for x be Point of product G st x in X holds
      f is_partial_differentiable_in x,i) &
    (for z be Point of product G st ||. z-x .|| < d holds z in X) &
    (for z be Point of product G st ||. z-x .|| < d
        holds ||. partdiff(f,z,i) - partdiff(f,x,i).|| <=r) &
    z = reproj(modetrans(G,i),y).p & q = proj(modetrans(G,i)).y
holds
   ||. f/.z - f/.y - ((partdiff(f,x,i)).(p-q)) .|| <= ||. p-q .||*r
proof
   let G be non-trivial RealNormSpace-Sequence,
       S be non trivial RealNormSpace,
       f be PartFunc of product G,S,
       X be Subset of product G,
       x,y,z be Point of product G,
       i0 be set,
       p,q be Point of G.(modetrans(G,i0)),
       d,r be Real;
   assume
A1: i0 in dom G & X is open & x in X &
    ||. y-x .|| < d & ||. z-x .|| < d & X c= dom f &
    (for x be Point of product G st x in X holds
       f is_partial_differentiable_in x,i0) &
    (for z be Point of product G st ||. z-x .|| < d holds z in X) &
    (for z be Point of product G st ||. z-x .|| < d
       holds ||. partdiff(f,z,i0) - partdiff(f,x,i0).|| <=r) &
    z = reproj(modetrans(G,i0),y).p & q = proj(modetrans(G,i0)).y;
   set i=modetrans(G,i0);
A2:y = reproj(i,y).q by A1,Th47;
A3:now let h be Point of G.i;
    assume h in [. q,p .]; then
    ||. reproj(i,y).h - x .|| < d by A1,Th52; then
    reproj(i,y).h in X by A1;
    hence reproj(i,y).h in dom f by A1;
   end;
A4:now let h be Point of G.i;
    assume h in [. q,p .]; then
    ||. reproj(i,y).h - x .|| < d by A1,Th52;
    hence f is_partial_differentiable_in (reproj(i,y).h),i0 by A1;
   end;
   for h be Point of G.i st h in ]. q,p .[ holds
     ||. partdiff(f,reproj(i,y).h,i0) - partdiff(f,x,i0) .|| <=r
   proof
    let h be Point of G.i;
    assume A5: h in ]. q,p .[;
    ].q,p.[ c= [. q,p .] by Th16; then
    ||. reproj(i,y).h - x .|| < d by A1,A5,Th52;
    hence ||. partdiff(f,reproj(i,y).h,i0) - partdiff(f,x,i0).|| <=r by A1;
   end;
   hence thesis by A2,A1,Th51,A3,A4;
end;

theorem Th54:
for G be non-trivial RealNormSpace-Sequence,
    h be FinSequence of product G,
    y,x be Point of product G,
    y0,Z be Element of product carr G,
     j be Element of NAT
  st y=y0 & Z=0.(product G)
    & len h = (len G)+1 & 1 <= j & j <= len G &
  (for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i)))
  holds x + h/.j = reproj(modetrans(G,(len G)+1-'j),(x+h/.(j+1)))
         .(proj(modetrans(G,(len G)+1-'j)).(x+y))
proof
   let G be non-trivial RealNormSpace-Sequence,
       h be FinSequence of product G,
       y,x be Point of product G,
       y0,Z be Element of product carr G,
       j be Element of NAT;
   assume that
A1: y = y0 and
A2: Z = 0.(product G) and
A3: len h = len G + 1 and
A4: 1 <= j & j <= len G and
A5: for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg(len G + 1-'i));

   len G <= len h by A3,NAT_1:11; then
   j <= len h by A4,XXREAL_0:2; then
   j in Seg len h by A4; then
   j in dom h by FINSEQ_1:def 3; then
A6:h/.j = Z +* (y0| Seg(len G + 1 -'j)) by A5;

   1 <= j+1 & j+1 <= len h by A3,A4,NAT_1:12,XREAL_1:6; then
   j+1 in Seg len h; then
   j+1 in dom h by FINSEQ_1:def 3; then
A7:h/.(j+1) = Z +* (y0| Seg(len G + 1-'(j+1))) by A5;
   j in Seg len G by A4; then
   len G -'j + 1 in Seg len G by NAT_2:6; then
   len G + 1 -' j in Seg len G by A4,NAT_D:38; then
   len G + 1 -' j in dom G by FINSEQ_1:def 3; then
A8:modetrans(G,(len G)+1-'j) = len G + 1 -' j by Def5;
   set xh = x+h/.(j+1);
   reconsider x1 = x, y1 = y as Element of product carr G by Th10;
   reconsider xy = x + y as Element of product carr G by Th10;
   xh is Element of product carr G by Th10; then
   consider g being Function such that
A9:xh = g & dom g = dom carr G &
    for y be set st y in dom carr G holds g.y in (carr G).y by CARD_3:def 5;
A10:dom xh = dom G by A9,Lm1;
   proj(modetrans(G,(len G)+1-'j)).(x+y) = xy.(len G + 1 -' j) by A8,Def3; then
A11:reproj(modetrans(G,(len G)+1-'j),(x+h/.(j+1)))
     .(proj(modetrans(G,(len G)+1-'j)).(x+y))
     = xh +* (modetrans(G,(len G)+1-'j), xy.(len G + 1 -' j)) by Def4
    .= xh +* (modetrans(G,(len G)+1-'j) .--> xy.(len G + 1 -' j))
       by A10,FUNCT_7:def 3
    .= xh +* ({len G + 1 -'j} --> xy.(len G + 1 -' j)) by A8,FUNCOP_1:def 9;
   reconsider F1 = x + h/.j as (len G)-element FinSequence;
   reconsider F2 = reproj(modetrans(G,(len G)+1-'j),(x+h/.(j+1)))
     .(proj(modetrans(G,(len G)+1-'j)).(x+y))
        as (len G)-element FinSequence;
   reconsider h1 = h/.j as Element of product carr G by Th10;
   reconsider xh1 = x + h/.j as Element of product carr G by Th10;
   reconsider h2 = h/.(j+1) as Element of product carr G by Th10;
A12:len F1 = len G & len F2 = len G by CARD_1:def 7;
   for k be Nat st 1 <= k & k <= len F1 holds F1.k = F2.k
   proof
    let k be Nat;
    assume A13: 1 <= k & k <= len F1; then
A14: k in Seg len F1 by FINSEQ_1:1; then
    reconsider k1 = k as Element of dom G by A12,FINSEQ_1:def 3;
    proj(k1).xh1 = proj(k1).x + proj(k1).(h/.j) by Th35; then
A15: F1.k = proj(k1).x + proj(k1).(h/.j) by Def3;
    y0 is Element of the carrier of product G by Th10; then
A16: dom y0 = Seg len G by FINSEQ_1:89;
A17: proj(k1).(h/.j) = h1.k by Def3;
A18: dom(y0|Seg(len G + 1-'j)) = dom y0 /\ Seg (len G + 1 -' j) by RELAT_1:61;
A19:  the carrier of (product G) = product carr G by Th10;
    per cases;
    suppose A20: not k in Seg(len G + 1 -' j); then
     not k in dom(y0|Seg(len G +1 -'j)) by A18,XBOOLE_0:def 4; then
     proj(k1).(h/.j) = Z.k by A17,A6,FUNCT_4:11; then
A21:  proj(k1).(h/.j) = proj(k1).(0.(product G)) by A2,Def3;
     not 1 <= k or not k <= len G + 1 -' j by A20,FINSEQ_1:1; then
     not k in dom ({len G + 1 -'j} --> xy.(len G + 1 -' j))
       by A13,TARSKI:def 1; then
     (xh +* ({len G + 1 -'j} --> xy.(len G + 1 -' j))).k1
        = xh.k1 by FUNCT_4:11; then
A22:  F2.k = proj(k1).(x+h/.(j+1)) by A19,A11,Def3;
A23:  proj(k1).(h/.(j+1)) = h2.k by Def3;
     len G + 1-'(j+1) <= len G +1-'j by NAT_1:11,NAT_D:41; then
     Seg(len G +1-'(j+1)) c= Seg(len G +1-'j) by FINSEQ_1:5; then
     not k in Seg(len G+1-'(j+1)) by A20; then
     not k in dom y0 /\ Seg(len G +1-'(j+1)) by XBOOLE_0:def 4; then
     not k in dom(y0|Seg(len G+1-'(j+1))) by RELAT_1:61; then
     (Z +* (y0| Seg(len G + 1-'(j+1)))).k = Z.k by FUNCT_4:11; then
     proj(k1).(h/.(j+1)) = proj(k1).(0.(product G)) by A2,A23,A7,Def3;
     hence F1.k = F2.k by A21,A15,A22,Th35;
    end;
    suppose A24: k in Seg(len G + 1 -' j); then
A25:  k in dom(y0|Seg(len G +1 -' j)) by A18,A14,A16,A12,XBOOLE_0:def 4; then
     proj(k1).(h/.j) = (y0|Seg(len G +1-'j)).k by A17,A6,FUNCT_4:13; then
     proj(k1).(h/.j) = y0.k by A25,FUNCT_1:47; then
A26:  proj(k1).(h/.j) = proj(k1).y by A1,Def3; then
A27:  F1.k = proj(k1).(x+y) by A15,Th35;
     per cases;
     suppose A28: k = len G + 1 -' j;
A29:   k in {k} by TARSKI:def 1; then
      k in dom({k} --> xy.k) by FUNCOP_1:13; then
      ( xh +* ({k} --> xy.k)).k1 = ({k} --> xy.k).k by FUNCT_4:13; then
      F2.k = xy.k by A11,A29,A28,FUNCOP_1:7;
      hence F1.k = F2.k by A27,Def3;
     end;
     suppose A30: k <> len G + 1 -' j; then
     not k in dom({len G + 1 -'j} --> xy.(len G +1 -'j)) by TARSKI:def 1; then
      F2.k = xh.k by A11,FUNCT_4:11; then
A31:   F2.k = proj(k1).(x+h/.(j+1)) by A19,Def3;
      k <= len G + 1 -' j by A24,FINSEQ_1:1; then
      k < len G + 1 -' j by A30,XXREAL_0:1; then
      k <= len G + 1 -' j -' 1 by NAT_D:49; then
      k <= len G + 1 -' (j+1) by NAT_2:30; then
      k in Seg (len G+1-'(j+1)) by A13,FINSEQ_1:1; then
A32:   k in dom(y0| Seg(len G + 1-'(j+1))) by A14,A16,A12,RELAT_1:57;
      proj(k1).(h/.(j+1)) = h2.k by Def3; then
      proj(k1).(h/.(j+1)) = (y0| Seg(len G + 1-'(j+1))).k1
        by A7,A32,FUNCT_4:13; then
      proj(k1).(h/.(j+1)) = y0.k by A32,FUNCT_1:47; then
      proj(k1).(h/.(j+1)) = proj(k1).y by A1,Def3;
      hence F1.k = F2.k by A26,A15,A31,Th35;
     end;
    end;
   end;
   hence thesis by A12,FINSEQ_1:def 17;
end;

theorem Th55:
for G be non-trivial RealNormSpace-Sequence,
    h be FinSequence of product G,
    y,x be Point of product G,
    y0,Z be Element of product carr G,
    j be Element of NAT
  st y=y0 & Z=0.(product G)
    & len h = (len G)+1 & 1 <= j & j <= len G &
  (for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i)))
  holds
 (proj(modetrans(G,(len G)+1-'j)).(x+y))
- proj(modetrans(G,(len G)+1-'j)).(x+h/.(j+1))
 = (proj(modetrans(G,(len G)+1-'j)).y)
proof
   let G be non-trivial RealNormSpace-Sequence,
       h be FinSequence of product G,
       y,x be Point of product G,
       y0,Z be Element of product carr G,
       j be Element of NAT;
   assume that
A1: y = y0 and
A2: Z=0.(product G) and
A3: len h = (len G)+1 & 1 <= j & j <= len G and
A4: for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i));
   x + h/.j = reproj(modetrans(G,(len G)+1-'j),(x+h/.(j+1)))
           .(proj(modetrans(G,(len G)+1-'j)).(x+y)) by A1,A2,A3,A4,Th54; then
   proj(modetrans(G,(len G)+1-'j)).(x+h/.j)
     = proj(modetrans(G,(len G)+1-'j)).(x+y) by Th46; then
A5:proj(modetrans(G,(len G)+1-'j)).(x+y)
        - proj(modetrans(G,(len G)+1-'j)).(x+h/.(j+1))
     = proj(modetrans(G,(len G)+1-'j)).(x + h/.j - (x+h/.(j+1))) by Th37;
   x + h/.j - (x + h/.(j+1))
    = h/.j + x - x - h/.(j+1) by RLVECT_1:27
   .= h/.j + (x - x) - h/.(j+1) by RLVECT_1:28
   .= h/.j + 0.(product G) - h/.(j+1) by RLVECT_1:15
   .= h/.j - h/.(j+1) by RLVECT_1:4; then
A6:proj(modetrans(G,(len G)+1-'j)).(x+y)
        - proj(modetrans(G,(len G)+1-'j)).(x+h/.(j+1))
    = proj(modetrans(G,(len G)+1-'j)).(h/.j)
     - proj(modetrans(G,(len G)+1-'j)).(h/.(j+1)) by A5,Th37;
   y0 is Element of the carrier of product G by Th10; then
A7:dom y0 = Seg len G by FINSEQ_1:89;
   j in Seg len G by A3; then
   len G -'j + 1 in Seg len G by NAT_2:6; then
A8:len G + 1 -' j in Seg len G by A3,NAT_D:38;

A9:j < len G +1 by A3,NAT_1:13; then
   len G+1-'j in Seg(len G+1-'j) by FINSEQ_1:3,NAT_D:36; then
A10:len G+1-'j in dom (y0|Seg(len G+1-'j)) by A7,A8,RELAT_1:57;
   len G+1-'j = len G+1-'(j+1)+1 by A9,NAT_2:7; then
A11:len G+1-'(j+1) < len G+1-'j by NAT_1:13;
   dom (y0|Seg(len G+1-'(j+1))) c= Seg(len G+1-'(j+1)) by RELAT_1:58; then
A12:not len G+1-'j in dom (y0|Seg(len G+1-'(j+1))) by A11,FINSEQ_1:1;

   reconsider h1 = h/.j as Element of product carr G by Th10;
   reconsider h2 = h/.(j+1) as Element of product carr G by Th10;
   j in Seg len h by A3,A9; then
   j in dom h by FINSEQ_1:def 3; then
A13:h/.j = Z +* (y0|Seg(len G+1-'j)) by A4;
   len G + 1 -' j in dom G by A8,FINSEQ_1:def 3; then
A14:modetrans(G,(len G)+1-'j) = len G + 1 -' j by Def5; then
A15:proj(modetrans(G,(len G)+1-'j)).(h/.j)
    = h1.(len G+1-'j) by Def3
   .= (y0|Seg(len G+1-'j)).(len G+1-'j) by A10,A13,FUNCT_4:13
   .= y0.(len G +1-'j) by A10,FUNCT_1:47
   .= proj(modetrans(G,len G+1-'j)).y by A1,A14,Def3;

   1 <= j+1 & j+1 <= len h by A3,NAT_1:12,XREAL_1:6; then
   j+1 in Seg len h; then
   j+1 in dom h by FINSEQ_1:def 3; then
A16:h/.(j+1) = Z +* (y0|Seg(len G+1-'(j+1))) by A4;

   proj(modetrans(G,(len G)+1-'j)).(h/.(j+1))
    = h2.(len G+1-'j) by A14,Def3
   .= Z.(len G+1-'j) by A16,A12,FUNCT_4:11
   .= proj(modetrans(G,len G+1-'j)).(0.(product G)) by A14,A2,Def3;
   hence proj(modetrans(G,(len G)+1-'j)).(x+y)
        - proj(modetrans(G,(len G)+1-'j)).(x+h/.(j+1))
    = proj(modetrans(G,len G+1-'j)).(y - 0.(product G)) by A6,A15,Th37
   .= proj(modetrans(G,len G+1-'j)).y by RLVECT_1:13;
end;

theorem Th56:
for G be non-trivial RealNormSpace-Sequence,
    S be non trivial RealNormSpace,
    f be PartFunc of product G, S,
    X be Subset of product G,
    x be Point of product G
 st X is open & x in X &
    (for i be set st i in dom G 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 product G
   ex w be FinSequence of S st
    dom w = dom G &
    (for i be set st i in dom G holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).h))
  & diff(f,x).h = Sum w
proof
   let G be non-trivial RealNormSpace-Sequence,
       S be non trivial RealNormSpace,
       f be PartFunc of product G, S,
       X be Subset of product G,
       x be Point of product G;
   assume
A1: X is open & x in X &
    (for i be set st i in dom G holds
      f is_partial_differentiable_on X,i &
      f`partial|(X,i) is_continuous_on X);
   set m = len G;
A2: dom G = Seg m by FINSEQ_1:def 3;
   reconsider Z0 = 0.(product G) as Element of product carr G by Th10;
   reconsider x0 = x as Element of product carr G by Th10;
   reconsider x1 = x as (len G)-element FinSequence;
   reconsider Z1=0.(product G) as (len G)-element FinSequence;
   consider L be Lipschitzian LinearOperator of product G,S such that
A3: for h be Point of product G
     ex w be FinSequence of S st
      dom w = Seg m &
      (for i be Element of NAT st i in Seg m holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).h))
        & L.h = Sum w by Lm5;
A4:
   for h be Point of product G
    ex w be FinSequence of S st
      dom w = dom G
    & (for i be set st i in dom G  holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).h))
    & L.h = Sum w
   proof
    let h be Point of product G;
    consider w be FinSequence of S such that
A5:  dom w = Seg m &
     (for i be Element of NAT st i in Seg m holds
          w.i = partdiff(f,x,i).(proj(modetrans(G,i)).h))
   & L.h = Sum w by A3;
    take w;
    thus dom w = dom G by A5,FINSEQ_1:def 3;
    thus thesis by A5,A2;
   end;
   consider d0 be Real such that
A6: d0 >0 and
A7: {y where y is Element of product G: ||. y-x .|| < d0} c= X by A1,NDIFF_1:3;
   set N = {y where y is Element of product G: ||. y-x .|| < d0};

   N c= the carrier of product G by A7,XBOOLE_1:1; then
A8:
   N is Neighbourhood of x by A6,NFCONT_1:def 1;
A9:
   1 <= m by NAT_1:14; then
   m in dom G by A2; then
   f is_partial_differentiable_on X,m by A1; then
   X c= dom f by Def8; then
A10:N c= dom f by A7,XBOOLE_1:1;

   deffunc RF(Element of product G) = f/.(x+$1) - f/.x - L.$1;

   consider R be Function of the carrier of product G,the carrier of S
      such that
A11:for h be Element of the carrier of product G holds R.h = RF(h)
         from FUNCT_2:sch 4;

   now let r0 be Real;
    assume A12: r0 > 0;
    set r1=r0/2;
    set r=r1/m;
    defpred DSQ[Nat, Element of REAL] means
     ex k be Element of NAT st $1=k & 0 < $2 &
      for q be Element of product G st q in X & ||. q-x .|| < $2 holds
       ||. partdiff(f,q,k)- partdiff(f,x,k) .|| < r;

A13: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 A14: k0 in Seg m;

     reconsider k = k0 as Element of NAT by ORDINAL1:def 12;
     f`partial|(X,k) is_continuous_on X by A2,A14,A1; then
     consider d be Real such that
A15:  0 < d &
      for q be Point of product G st q in X & ||. q- x .|| < d holds
       ||. (f`partial|(X,k))/.q - (f`partial|(X,k))/.x .|| < r
          by A12,A1,NFCONT_1:19;
     take d;
     for q be Point of product G st q in X & ||. q-x .|| < d holds
       ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r
     proof
      let q be Point of product G;
      assume A16:q in X & ||. q- x .|| < d; then
A17:  ||. (f`partial|(X,k))/.q - (f`partial|(X,k))/.x .|| < r by A15;

A18:  f is_partial_differentiable_on X,k by A1,A14,A2; then
      (f`partial|(X,k))/.q = partdiff(f,q,k) by A16,A14,A2,Def9;
      hence ||. partdiff(f,q,k)- partdiff(f,x,k) .|| < r
         by A17,A18,A1,A14,A2,Def9;
     end;
     hence ex k be Element of NAT st k0=k & 0 < d &
      for q be Element of product G st q in X & ||. q-x .|| < d holds
       ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A15;
    end;

    consider Dseq be FinSequence of REAL such that
A19: dom Dseq = Seg m &
     for i be Nat st i in Seg m holds DSQ[i,Dseq.i] from FINSEQ_1:sch 5(A13);

    m in Seg m by A9; then
    reconsider rDseq = rng Dseq as non empty ext-real-membered set
      by A19,FUNCT_1:3;
    reconsider rDseq as left_end right_end non empty ext-real-membered set;
A20:min rDseq in rng Dseq by XXREAL_2:def 7; then
    reconsider d1 = min rDseq as Real;

    set d = min(d0,d1);
A21: d <= d0 & d <= d1 by XXREAL_0:17;
    consider i1 be set such that
A22: i1 in dom Dseq & d1 = Dseq.i1 by A20,FUNCT_1:def 3;

    reconsider i1 as Nat by A22;

A23:ex k be Element of NAT st i1=k & 0 < Dseq.i1 &
     for q be Element of product G st q in X & ||. q-x .|| < Dseq.i1 holds
       ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A19,A22;

A24:now let q be Element of product G;
     assume ||. q-x .|| < d; then
     ||. q-x .|| < d0 by A21,XXREAL_0:2; then
     q in {y where y is Element of product G: ||. y-x .|| < d0};
     hence q in X by A7;
    end;

A25:now let q be Element of product G, i be Element of NAT;
     assume A26: ||. q-x .|| < d & i in Seg m;
     reconsider i0=i as Nat;
     consider k be Element of NAT such that
A27:  i0 = k & 0 < Dseq.i0 &
      for q be Element of product G st q in X & ||. q-x .|| < Dseq.i0 holds
       ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A19,A26;
     Dseq.i0 in rng Dseq by A19,A26,FUNCT_1:3; then
     d1 <= Dseq.i0 by XXREAL_2:def 7; then
     d <= Dseq.i0 by A21,XXREAL_0:2; then
     ||. q-x .|| < Dseq.i0 by A26,XXREAL_0:2;
     hence ||. partdiff(f,q,i) - partdiff(f,x,i) .|| < r by A24,A26,A27;
    end;
    take d;
    thus 0 < d by A6,A22,A23,XXREAL_0:21;
    thus for y be Point of product G st
       y <> 0.(product G) & ||.y.|| < d holds ||.y.||"* ||. R/.y .|| < r0
    proof
     let y be Point of product G;
     assume A28: y <> 0.(product G) & ||. y .||< d; then
A29:0 <> ||. y .|| by NORMSP_0:def 5;
     set z= R/.y;
     consider h be FinSequence of product G, g be FinSequence of S,
              Z,y0 be Element of product carr G such that
A30:  y0=y & Z = 0.(product G)
    & len h = len G + 1 & len g = len G
    & (for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg (len G + 1-'i)))
    & (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 Point of product G st
          i in dom h & h/.i= hi holds ||. hi .|| <=||. y .||)
    & f /.(x+y) - f/.x = Sum g by Th45;
     consider w be FinSequence of S such that
A31:  dom w = Seg m
    & (for i be Element of NAT st i in Seg m holds
           w.i = partdiff(f,x,i).(proj(modetrans(G,i)).y))
    & L.y = Sum w by A3;

A32: dom idseq m = Seg m & rng idseq m = Seg m by FUNCT_2:def 1,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;

A34: len (idseq m) = m & len w = m by A31,A32,FINSEQ_1:def 3;

     dom (w * Ri) = dom Ri by A33,RELAT_1:27; then
A35: dom (w * Ri) = dom Rev w by A33,A31,FINSEQ_5:57;
     reconsider wRi=w * Ri as FinSequence of S by FINSEQ_2:47;
     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 zr0=0 as Nat;
      0 <= mk; then
A39:  zr0 + 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
A40:  mk+1 in Seg m by A39;
      (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 A40,A34,FINSEQ_2:49
        .= w.((Rev idseq m).k) by A37,FINSEQ_5:def 3;
      hence (Rev w).k = wRi.k by A36,A35,FUNCT_1:12;
     end; then
A41: Sum Rev w = Sum w by A35,FINSEQ_1:13,RLVECT_2:7;

     deffunc GW(Nat) = g/.$1 - (Rev w)/.$1;
     consider gw be FinSequence of S such that
A42:  len gw =m &
      for j being Nat st j in dom gw holds gw.j = GW(j) from FINSEQ_2:sch 1;
A43: now let j be Element of NAT;
      assume j in dom g; then
      j in Seg m by A30,FINSEQ_1:def 3; then
      j in dom gw by A42,FINSEQ_1:def 3;
      hence gw.j = g/.j - (Rev w)/.j by A42;
     end;
    len Rev w = len g by A30,A34,FINSEQ_5:def 3; then
     Sum gw = Sum g - Sum(Rev w) by A30,A42,A43,RLVECT_2:5; then
A44: R/.y = Sum gw by A11,A30,A31,A41;
A45: for j be Element of NAT st j in dom gw holds ||. gw/.j .|| <= ||. y .||*r
     proof
      let j be Element of NAT;
      assume A46: j in dom gw; then
A47:  j in Seg m by A42,FINSEQ_1:def 3; then
A48: j in dom g by A30,FINSEQ_1:def 3; then
A49:  g/.j = f/.(x+h/.j) - f/.(x+h/.(j+1)) by A30;
A50:  1 <= j & j <=m by A47,FINSEQ_1:1; then
A51:  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,20; then
      m+1-'j <= m & 1 <= m+1-'j by A50,NAT_D:37; then
A52:  m+1-'j in Seg m; then
      f is_partial_differentiable_on X,(m+1-'j) by A1,A2; then
A53:  X c=dom f &
      for x be Element of product G st x in X holds
       f is_partial_differentiable_in x,(m+1-'j) by Th24,A1;
      w/.(m+1-'j) = w.(m+1-'j) by A31,A52,PARTFUN1:def 6; then
A54:  w/.(m+1-'j) = (partdiff(f,x,(m+1-'j))).(proj(modetrans(G,m+1-'j)).y)
         by A52,A31;
A55:  now let j be Element of NAT;
       reconsider hj = h/.j as Element of product G;
       assume 1 <= j & j <= m + 1; then
       j in dom h by A30,FINSEQ_3:25; then
A56:   ||. hj .|| <= ||. y .|| by A30;
       (x+h/.j)-x = h/.j + (x-x) by RLVECT_1:28
         .= h/.j + 0.(product G) by RLVECT_1:15; then
       (x+h/.j)-x = h/.j by RLVECT_1:4;
       hence ||. (x+h/.j)-x .|| < d by A56,A28,XXREAL_0:2;
      end;
      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 A47,FINSEQ_1:1; then
A57:  ||. (x+h/.j)-x .|| < d by A55;
      1 <= j+1 by NAT_1:11; then
A58:  ||. (x+h/.(j+1))-x .|| < d by A51,A55;
A59:  x + h/.j = reproj(modetrans(G,m+1-'j),(x+h/.(j+1)) )
                   .(proj(modetrans(G,m+1-'j)).(x+y)) by Th54,A30,A50;

A60:   (proj(modetrans(G,m+1-'j)).(x+y))
         - proj(modetrans(G,m+1-'j)).(x+h/.(j+1))
       = (proj(modetrans(G,m+1-'j)).y) by Th55,A30,A50;

      for z be Point of product G st ||. z-x .|| < d holds
        ||. partdiff(f,z,(m+1-'j)) - partdiff(f,x,(m+1-'j)).||
           <=r by A25,A52; then
A61:  ||. f/.(x+h/.j) - f/.(x+h/.(j+1))
          - (partdiff(f,x,(m+1-'j))).(proj(modetrans(G,m+1-'j)).y).||
        <= ||.(proj(modetrans(G,m+1-'j)).y).|| *r
             by A1,A53,A52,A2,A24,A57,A58,A59,A60,Th53;
A62:  m+1-'j = m+1-j by A50,NAT_1:12,XREAL_1:233;
      j in Seg len (Rev w) by A47,A34,FINSEQ_5:def 3; then
A63:  j in dom Rev w by FINSEQ_1:def 3; then
A64: (Rev w)/.j = (Rev w).j by PARTFUN1:def 6
        .= w.(m-j+1) by A34,A63,FINSEQ_5:def 3
        .= w/.(m+1-'j) by A62,A52,A31,PARTFUN1:def 6;
A65:  gw/.j = gw.j by A46,PARTFUN1:def 6
           .= f/.(x+h/.j) - f/.(x+h/.(j+1))
               - (partdiff(f,x,(m+1-'j))).(proj(modetrans(G,m+1-'j)).y)
                     by A54,A49,A64,A48,A43;
      ||. (proj(modetrans(G,m+1-'j)).y).||*r <= ||. y .||*r
         by A12,Th31,XREAL_1:64;
      hence ||. gw/.j .|| <= ||. y .||*r by A65,A61,XXREAL_0:2;
     end;
     defpred YSQ[set,set] means $2 = ||. gw/.$1 .||;
A66: for k be Nat st k in Seg m holds
       ex x be Element of REAL st YSQ[k,x];
     consider yseq be FinSequence of REAL such that
A67:  dom yseq = Seg m &
      for i be Nat st i in Seg m holds YSQ[i,yseq.i] from FINSEQ_1:sch 5(A66);
A68: len gw = len yseq by A42,A67,FINSEQ_1:def 3;
A69: now let i be Element of NAT;
      assume i in dom gw; then
      i in Seg m by A42,FINSEQ_1:def 3;
      hence yseq.i = ||. gw/.i .|| by A67;
     end;
     reconsider yseq as Element of REAL m by A68,A42,FINSEQ_2:92;
A70: ||. Sum gw .|| <= Sum yseq by A69,A68,Th7;
     for j be Nat st j in Seg m holds yseq.j <= (m |-> (||. y .||*r)).j
     proof
      let j be Nat;
      assume A71: j in Seg m; then
      j in dom gw by A42,FINSEQ_1:def 3; then
A72: ||. gw/.j .|| <= ||. y .||*r by A45;
      yseq.j = ||. gw/.j .|| by A67,A71;
      hence yseq.j <= (m |-> (||. y .||*r)).j by A71,A72,FINSEQ_2:57;
     end; then
     Sum yseq <= Sum(m |-> (||. y .||*r)) by RVSUM_1:82; then
     Sum yseq <= m*(||. y .||*r) by RVSUM_1:80; then
     ||. z .|| <= m*(||. y .||*r) by A44,A70,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 A29,XCMPLX_1:203; then
A73: ||.y.||"* ||. z .|| <= r1 by XCMPLX_1:87;
     r1 < r0 by A12,XREAL_1:216;
     hence (||.y.||"* ||. z .||) < r0 by A73,XXREAL_0:2;
    end;
   end; then
   reconsider R as RestFunc of product G,S by NDIFF_1:23;
   reconsider L as Point of
     R_NormSpace_of_BoundedLinearOperators(product G,S) by LOPBAN_1:def 9;
A74:
   for y being Point of product G st y in N
      holds f/.y - f/.x = L.(y-x) + R/.(y-x)
   proof
    let y be Point of product G;
    assume y in N;
    y-x in the carrier of (product G); then
    y-x in dom R by PARTFUN1:def 2; then
    R/.(y-x) = R.(y-x) by PARTFUN1:def 6; then
    R/.(y-x) = f/.(x+(y-x)) - f/.x - L.(y-x) by A11;
    hence L.(y-x) + R/.(y-x)
          = f/.(x+(y-x)) - f/.x - (L.(y-x) - L.(y-x)) by RLVECT_1:29
        .= f/.(x+(y-x)) - f/.x - 0.S by RLVECT_1:5
        .= f/.(x+(y-x)) - f/.x by RLVECT_1:13
        .= f/.(y-(x-x)) - f/.x by RLVECT_1:29
        .= f/.(y-0.(product G)) - f/.x by RLVECT_1:5
        .= f/.y - f/.x by RLVECT_1:13;
   end; then
   f is_differentiable_in x by A10,A8,NDIFF_1:def 6; then
   diff(f,x) = L by A8,A10,A74,NDIFF_1:def 7;
   hence thesis by A4,A74,A10,A8,NDIFF_1:def 6;
end;

theorem
for G be non-trivial RealNormSpace-Sequence,
    F be non trivial RealNormSpace,
    f be PartFunc of product G, F,
    X be Subset of product G
 st X is open holds
  (for i be set st i in dom G 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 G be non-trivial RealNormSpace-Sequence,
       F be non trivial RealNormSpace,
       f be PartFunc of product G, F,
       X be Subset of product G;
   assume A1: X is open;
   set m=len G;
A2: dom G = Seg m by FINSEQ_1:def 3;
   hereby assume
A3:  for i be set st i in dom G holds
      f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X;
A4: now let i be Element of NAT;
     assume 1 <=i & i <= m; then
     i in Seg m; then
     f`partial|(X,i) is_continuous_on X by A3,A2;
     hence X c= dom (f`partial|(X,i))
        & for y0 be Point of product G, r be Real st y0 in X & 0<r
            ex s be Real st 0<s &
        for y1 be Point of product G st y1 in X & ||. y1- y0 .|| < s holds
        ||. (f`partial|(X,i))/.y1-(f`partial|(X,i))/.y0 .||<r by NFCONT_1:19;
    end;
A5: 1 <= m by NAT_1:14; then
    m in dom G by A2; then
    f is_partial_differentiable_on X,m by A3; then
A6: X c= dom f by Def8;
    for x be Point of product G st x in X holds
      f is_differentiable_in x by A1,A3,Th56;
    hence
A7:   f is_differentiable_on X by A1,A6,NDIFF_1:31; then
A8: dom (f`|X) = X by NDIFF_1:def 9;
    for y0 be Point of product G, r be Real st y0 in X & 0<r
      ex s be Real st 0<s &
       for y1 be Point of product G st y1 in X & ||. y1- y0 .|| < s holds
        ||. (f`|X)/.y1-(f`|X)/.y0 .|| < r
    proof
     let y0 be Point of product G, r be Real;
     assume A9: y0 in X & 0<r;
     defpred P[Nat,Real] means
       for i being Element of NAT st i=$1 holds
        (0<$2 &
        for y1 be Point of product G st y1 in X & ||. y1- y0 .|| < $2 holds
        ||. (f`partial|(X,i))/.y1-(f`partial|(X,i))/.y0 .||<r/(2*m));
A10:  now let i be Nat;
      reconsider j=i as Element of NAT by ORDINAL1:def 12;
      assume i in Seg m; then
      1 <=j & j <= m by FINSEQ_1:1; then
      consider s be Real such that
A11:    0<s &
       for y1 be Point of product G st y1 in X & ||. y1- y0 .|| < s holds
        ||. (f`partial|(X,j))/.y1-(f`partial|(X,j))/.y0 .||<r/(2*m) by A9,A4;
      reconsider s as Element of REAL;
      take s;
      thus P[i,s] by A11;
     end;
     consider S being FinSequence of REAL such that
A12:  dom S = Seg m
    & for i be Nat st i in Seg m holds P[i,S.i] from FINSEQ_1:sch 5(A10);
     take s = min S;
A13: len S = m by A12,FINSEQ_1:def 3; then
     min_p S in dom S by RFINSEQ2:def 2;
     hence s > 0 by A12;
     let y1 be Point of product G;
     assume A14: y1 in X & ||. y1- y0 .|| < s;
     reconsider DD=diff(f,y1)-diff(f,y0) as Lipschitzian LinearOperator of
          product G, F by LOPBAN_1:def 9;
A15: upper_bound PreNorms(DD) = ||. diff(f,y1) - diff(f,y0) .|| by LOPBAN_1:30;
     now let mt be real number;
      assume mt in PreNorms(DD); then
      consider t being VECTOR of product G such that
A16:   mt=||.DD.t.|| & ||.t.|| <= 1;
      consider w0 be FinSequence of F such that
A17:   dom w0 = dom G &
       (for i be set st i in dom G holds
          w0.i = partdiff(f,y0,i).(proj(modetrans(G,i)).t)) &
          diff(f,y0).t=Sum(w0) by A1,A3,Th56,A9;
      reconsider Sw0=Sum w0 as Point of F;
      consider w1 be FinSequence of F such that
A18:   dom w1 = dom G &
       (for i be set st i in dom G holds
          w1.i = partdiff(f,y1,i).(proj(modetrans(G,i)).t)) &
        diff(f,y1).t=Sum(w1) by A1,A3,Th56,A14;
      reconsider Sw1=Sum w1 as Point of F;
      deffunc F(set) = w1/.$1 - w0/.$1;
      consider w2 being FinSequence of F such that
A19:   len w2 = m & for i being Nat st i in dom w2 holds
         w2.i = F(i) from FINSEQ_2:sch 1;
A20:  len w1 = m & len w0 = m by A2,A17,A18,FINSEQ_1:def 3;
      now let i be Element of NAT;
       assume i in dom w1; then
       i in dom w2 by A19,A2,A18,FINSEQ_1:def 3;
       hence w2.i = F(i) by A19;
      end; then
      Sum w2 = Sum w1 - Sum w0 by A19,A20,RLVECT_2:5; then
A21:  mt= ||. Sum w2 .|| by A16,A18,A17,LOPBAN_1:40;
      deffunc F(Nat) = ||. (w2/.$1) .||;
      consider ys being FinSequence of REAL such that
A22:   len ys = m & for j being Nat st j in dom ys holds ys.j = F(j)
          from FINSEQ_2:sch 1;
A23:  now let i be Element of NAT;
       assume i in dom w2; then
       i in Seg m by A19,FINSEQ_1:def 3; then
       i in dom ys by A22,FINSEQ_1:def 3;
       hence ys.i = ||.w2/.i.|| by A22;
      end; then
A24:  ||. Sum w2 .|| <= Sum ys by A19,A22,Th7;
      reconsider rm=r/(2*m) as Element of REAL;
      deffunc F(Nat) = rm;
      consider rs being FinSequence of REAL such that
A25:   len rs = m & for j being Nat st j in dom rs holds rs.j = F(j)
          from FINSEQ_2:sch 1;
A26:  dom rs = Seg m by A25,FINSEQ_1:def 3;
      now let a be set;
       assume a in rng rs; then
       consider b being set such that
A27:    b in dom rs & a=rs.b by FUNCT_1:def 3;
       reconsider b as Nat by A27;
       rs.b=rm by A27,A25;
       hence a in {rm} by A27,TARSKI:def 1;
      end; then
A28: rng rs c= {rm} by TARSKI:def 3;
      now let a be set;
       assume a in {rm}; then
A29:   a = rm by TARSKI:def 1;
A30:   1 in dom rs by A5,A26; then
       a = rs.1 by A29,A25;
       hence a in rng rs by A30,FUNCT_1:3;
      end; then
      {rm} c= rng rs by TARSKI:def 3; then
      {rm} = rng rs by A28,XBOOLE_0:def 10; then
      rs = m |-> (r/(2*m)) by A26,FUNCOP_1:9; then
      Sum rs = m*(r/(2*m)) by RVSUM_1:80
            .= m*(r/2/m) by XCMPLX_1:78; then
A31:  Sum rs = 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 A17,A18,A19,FINSEQ_1:def 3; then
A34:   ys.i = ||. w2/.i .|| & w2/.i= w2.i by A23,PARTFUN1:def 6;
A35:   i in dom rs by A25,A32,FINSEQ_1:def 3;
       reconsider p1=partdiff(f,y1,i),p0 = partdiff(f,y0,i)
        as Lipschitzian LinearOperator of G.(modetrans(G,i)), F
        by LOPBAN_1:def 9;
       reconsider P1 = p1.(proj(modetrans(G,i)).t) as VECTOR of F;
       reconsider P0=p0.(proj(modetrans(G,i)).t ) as VECTOR of F;
       w0/.i = w0.i & w1/.i = w1.i by A33,PARTFUN1:def 6; then
       w0/.i = P0 & w1/.i = P1 by A2,A17,A18,A32; then
A36:   w2.i = P1-P0 by A33,A19;
       1 <= i & i <= len S by A13,A32,FINSEQ_1:1; then
A37:   s <= S.i & f is_partial_differentiable_on X,i
          by A2,A32,A3,RFINSEQ2:2; then
       ||. y1- y0 .|| < S.i by A14,XXREAL_0:2; then
       ||. (f`partial|(X,i))/.y1-(f`partial|(X,i))/.y0 .||<r/(2*m)
            by A12,A32,A14; then
       ||. partdiff(f,y1,i)-(f`partial|(X,i))/.y0 .||<r/(2*m)
            by Def9,A14,A37,A2,A32; then
A38:   ||. partdiff(f,y1,i)-partdiff(f,y0,i) .||<r/(2*m)
            by Def9,A9,A37,A2,A32;
       reconsider PP=partdiff(f,y1,i)-partdiff(f,y0,i) as
            Lipschitzian LinearOperator of G.(modetrans(G,i)),F
            by LOPBAN_1:def 9;
A39:   upper_bound PreNorms(PP)
        = ||. partdiff(f,y1,i)-partdiff(f,y0,i) .|| by LOPBAN_1:30;
       reconsider pt=proj(modetrans(G,i)).t as VECTOR of G.(modetrans(G,i));
A40:   PP.pt=P1-P0 by LOPBAN_1:40;
       ||.pt.|| <= ||.t.|| by Th31; then
       ||.pt.|| <= 1 by A16,XXREAL_0:2; 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 A40,A38,A39,XXREAL_0:2;
       hence ys.i <= rs.i by A34,A25,A35,A36;
      end; then
      Sum ys <= r/2 by A31,A25,A22,INTEGRA5:3;
      hence mt <= r/2 by A21,A24,XXREAL_0:2;
     end; then
     ||. diff(f,y1) - diff(f,y0) .|| <= r/2 & r/2 < r
        by A15,A9,SEQ_4:45,XREAL_1:216; then
     ||. diff(f,y1) - diff(f,y0) .|| < r by XXREAL_0:2; then
     ||. diff(f,y1) -(f`|X)/.y0 .|| < r by A7,A9,NDIFF_1:def 9;
     hence ||. (f`|X)/.y1-(f`|X)/.y0 .|| < r by A7,A14,NDIFF_1:def 9;
    end;
    hence f`|X is_continuous_on X by A8,NFCONT_1:19;
   end;

   assume
A41:f is_differentiable_on X & f`|X is_continuous_on X; then
A42:
   X c= dom f & for x be Point of product G st x in X holds
    f is_differentiable_in x by A1,NDIFF_1:31;
   thus for i be set st i in dom G holds
       f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X
   proof
    let i be set;
    assume A43:i in dom G; then
    reconsider i0=i as Element of NAT;
    now let x be Point of product G;
     assume x in X; then
     f is_differentiable_in x by A41,A1,NDIFF_1:31;
     hence f is_partial_differentiable_in x,i &
       partdiff(f,x,i) = diff(f,x) * reproj(modetrans(G,i),0.(product G))
          by Th41;
    end; then
    for x be Point of product G st x in X
     holds f is_partial_differentiable_in x,i;
    hence
A44: f is_partial_differentiable_on X,i by A1,Th32,A42; then
A45:dom (f`partial|(X,i)) = X by Def9,A43;
    for y0 be Point of product G, r be Real st y0 in X & 0<r
      ex s be Real st 0<s & for y1 be Point of product G
        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 product G, r be Real;
     assume A46: y0 in X & 0<r; then
     consider s be Real such that
A47:  0<s & for y1 be Point of product G
       st y1 in X & ||. y1- y0 .|| < s holds
         ||. (f`|X)/.y1-(f`|X)/.y0 .||<r by A41,NFCONT_1:19;
     take s;
     thus 0<s by A47;
     let y1 be Point of product G;
     assume A48: y1 in X & ||. y1- y0 .|| < s; then
     ||. (f`|X)/.y1-(f`|X)/.y0 .||<r by A47; then
     ||. diff(f,y1) - (f`|X)/.y0 .||<r by A48,A41,NDIFF_1:def 9; then
A49: ||. diff(f,y1) - diff(f,y0) .||<r by A46,A41,NDIFF_1:def 9;
     f is_differentiable_in y1 & f is_differentiable_in y0 by A41,A1,A48,A46,
NDIFF_1:31; then
A50: partdiff(f,y1,i) = diff(f,y1)* reproj(modetrans(G,i),0.(product G))
   & partdiff(f,y0,i) = diff(f,y0)* reproj(modetrans(G,i),0.(product G))
          by Th41;
     reconsider PP=partdiff(f,y1,i)-partdiff(f,y0,i)
       as Lipschitzian LinearOperator of G.(modetrans(G,i)),F
       by LOPBAN_1:def 9;
     reconsider DD=diff(f,y1)-diff(f,y0)
       as Lipschitzian LinearOperator of product G,F by LOPBAN_1:def 9;
A51: upper_bound PreNorms(PP) = ||. partdiff(f,y1,i)-partdiff(f,y0,i) .||
   & upper_bound PreNorms(DD) = ||. diff(f,y1) - diff(f,y0) .|| by LOPBAN_1:30;
A52: PreNorms(PP) is bounded_above & PreNorms(DD) is bounded_above
       by LOPBAN_1:28;
     now let a be set;
      assume a in PreNorms(PP); then
      consider t being VECTOR of G.(modetrans(G,i)) such that
A53:   a=||.PP.t.|| & ||.t.|| <= 1;
A54:  dom reproj(modetrans(G,i),0.(product G))
        = the carrier of G.(modetrans(G,i)) by FUNCT_2:def 1;
      reconsider tm=reproj(modetrans(G,i),0.(product G)).t
         as Point of product G;
A55:  ||. tm .|| <= 1 by A53,Th21;
      partdiff(f,y1,i).t = diff(f,y1).tm &
      partdiff(f,y0,i).t = diff(f,y0).tm by A54,A50,FUNCT_1:13; then
      ||. PP.t .|| = ||. diff(f,y1).tm - diff(f,y0).tm.|| by LOPBAN_1:40; then
      ||. PP.t .|| = ||. DD.tm .|| by LOPBAN_1:40;
      hence a in PreNorms(DD) by A53,A55;
     end; then
     PreNorms(PP) c= PreNorms(DD) by TARSKI:def 3; then
     ||. partdiff(f,y1,i)-partdiff(f,y0,i) .|| <=
        ||. diff(f,y1) - diff(f,y0) .|| by A52,A51,SEQ_4:48; then
     ||. partdiff(f,y1,i)-partdiff(f,y0,i) .||<r by A49,XXREAL_0:2; then
     ||. partdiff(f,y1,i)-(f`partial|(X,i))/.y0 .||<r by Def9,A46,A44,A43;
     hence ||. (f`partial|(X,i))/.y1-(f`partial|(X,i))/.y0 .||<r
        by Def9,A48,A44,A43;
    end;
    hence f`partial|(X,i) is_continuous_on X by A45,NFCONT_1:19;
   end;
end;