:: The Differentiable Functions on Normed Linear Spaces
::  by Hiroshi Imura , Morishige Kimura and Yasunari Shidama
::
:: Received May 24, 2004
:: Copyright (c) 2004-2019 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, SUBSET_1, REAL_1, NORMSP_1, SEQ_1, NAT_1, PRE_TOPC,
      RCOMP_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, XXREAL_0, RELAT_1, FUNCT_1,
      SEQ_2, ORDINAL2, STRUCT_0, VALUED_0, SUPINF_2, RLVECT_1, VALUED_1,
      COMPLEX1, XXREAL_2, FDIFF_1, ZFMISC_1, PARTFUN1, FUNCOP_1, FUNCT_2,
      LOPBAN_1, XBOOLE_0, FCONT_1, RSSPACE, NFCONT_1, CFCONT_1, LOPBAN_2;
 notations TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PRE_TOPC,
      XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, ORDINAL1, NUMBERS, REAL_1, NAT_1,
      RLVECT_1, STRUCT_0, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, VFUNCT_1,
      NORMSP_0, NORMSP_1, RSSPACE, LOPBAN_1, LOPBAN_2, NFCONT_1, FDIFF_1,
      RECDEF_1;
 constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_2, FDIFF_1, RSSPACE, VFUNCT_1,
      LOPBAN_3, NFCONT_1, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2,
      NUMBERS;
 registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
      FDIFF_1, STRUCT_0, LOPBAN_1, LOPBAN_2, VALUED_0, VALUED_1, FUNCT_2,
      FUNCOP_1, NAT_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, XBOOLE_0, NFCONT_1, NORMSP_1, STRUCT_0;
 equalities XBOOLE_0, RLVECT_1, SUBSET_1, VALUED_1, STRUCT_0;
 expansions TARSKI, XBOOLE_0, NFCONT_1, NORMSP_1, STRUCT_0;
 theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, SUBSET_1, RELSET_1, RLVECT_1,
      XCMPLX_0, XCMPLX_1, ZFMISC_1, FUNCOP_1, SEQ_1, SEQ_2, NAT_1, SEQM_3,
      RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, SEQ_4, NORMSP_1, LOPBAN_1, LOPBAN_2,
      LOPBAN_3, PARTFUN1, PARTFUN2, NFCONT_1, XREAL_1, COMPLEX1, XXREAL_0,
      ORDINAL1, VALUED_1, STRUCT_0, VALUED_0, VECTSP_1, NORMSP_0, NUMBERS;
 schemes NAT_1, SEQ_1, RECDEF_1, FUNCT_2;

begin :: Differentiable Function on Normed Linear Spaces

reserve n,k for Element of NAT;
reserve x,y,X for set;
reserve g,r,p for Real;
reserve S for RealNormSpace;
reserve rseq for Real_Sequence;
reserve seq,seq1 for sequence of S;
reserve x0 for Point of S;
reserve Y for Subset of S;

:: Normed Linear Spaces varsions of RCOMP_1:37 -
:: RCOMP_1:37 --> NFCONT_1:4

theorem Th1:
  for x0 be Point of S for N1,N2 being Neighbourhood of x0 ex N
  being Neighbourhood of x0 st N c= N1 & N c= N2
proof
  let x0 be Point of S;
  let N1,N2 be Neighbourhood of x0;
  consider g1 be Real such that
A1: 0<g1 and
A2: {y where y is Point of S: ||.y-x0 .|| < g1} c= N1 by NFCONT_1:def 1;
  consider g2 be Real such that
A3: 0<g2 and
A4: {y where y is Point of S: ||.y-x0 .|| < g2} c= N2 by NFCONT_1:def 1;
  set g = min(g1,g2);
  take {y where y is Point of S: ||.y-x0 .|| < g};
A5: g<=g2 by XXREAL_0:17;
A6: {y where y is Point of S: ||.y-x0 .|| < g} c= {y where y is Point of S:
  ||.y-x0 .|| < g2}
  proof
    let z be object;
    assume z in {y where y is Point of S: ||.y-x0 .|| < g};
    then consider y be Point of S such that
A7: z=y and
A8: ||.y-x0 .|| < g;
    ||.y-x0 .|| < g2 by A5,A8,XXREAL_0:2;
    hence thesis by A7;
  end;
A9: g<=g1 by XXREAL_0:17;
A10: {y where y is Point of S: ||.y-x0 .|| < g} c= {y where y is Point of S:
  ||.y-x0 .|| < g1}
  proof
    let z be object;
    assume z in {y where y is Point of S: ||.y-x0 .|| < g};
    then consider y be Point of S such that
A11: z=y and
A12: ||.y-x0 .|| < g;
    ||.y-x0 .|| < g1 by A9,A12,XXREAL_0:2;
    hence thesis by A11;
  end;
  0<g by A1,A3,XXREAL_0:15;
  hence thesis by A2,A4,A10,A6,NFCONT_1:3;
end;

theorem Th2:
  for X being Subset of S st X is open for r be Point of S st r in
  X ex N being Neighbourhood of r st N c= X
proof
  let X be Subset of S;
  assume X is open;
  then
A1: X` is closed;
  let r be Point of S;
  assume that
A2: r in X and
A3: for N be Neighbourhood of r holds not N c= X;
  defpred P[Element of NAT,Point of S] means $2 in {y where y is Point of S:
  ||.y-r.|| < 1/($1+1)} & $2 in X`;
A4: now
    let g be Real such that
A5: 0<g;
    set N={y where y is Point of S:||.y-r.|| < g};
    N is Neighbourhood of r by A5,NFCONT_1:3;
    then not N c= X by A3;
    then consider x be object such that
A6: x in N and
A7: not x in X;
    consider s be Point of S such that
A8: x=s and
A9: ||.s-r.|| <g by A6;
    take s;
    thus s in N by A9;
    thus s in X` by A7,A8,XBOOLE_0:def 5;
  end;
A10: for n ex s be Point of S st P[n,s]
  proof
    let n;
    0 < 1 * (n + 1)";
    then 0 < 1/(n + 1) by XCMPLX_0:def 9;
    hence thesis by A4;
  end;
  consider s1 be sequence of S such that
A11: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A10);
A12: rng s1 c= X`
  proof
    let x be object;
    assume x in rng s1;
    then consider y be object such that
A13: y in dom s1 and
A14: s1.y=x by FUNCT_1:def 3;
    reconsider y as Element of NAT by A13;
    s1.y in X` by A11;
    hence thesis by A14;
  end;
A15: now
    let p be Real;
    assume
A16: 0<p;
    consider n being Nat such that
A17: p"<n by SEQ_4:3;
    p" + 0 < n + 1 by A17,XREAL_1:8;
    then 1/(n+1) < 1/p" by A16,XREAL_1:76;
    then
A18: 1/(n+1) < p by XCMPLX_1:216;
    take n;
    let m be Nat;
A19:  m in NAT by ORDINAL1:def 12;
    assume n<=m;
    then
A20: n + 1 <= m + 1 by XREAL_1:6;
    s1.m in {y where y is Point of S:||.y-r.|| < 1/(m+1)} by A11,A19;
    then
A21: ex y be Point of S st s1.m=y & ||.y-r.|| < 1/(m+1);
    1/(m+1) <= 1/(n+1) by A20,XREAL_1:118;
    then ||.s1.m - r.|| < 1/(n+1) by A21,XXREAL_0:2;
    hence ||.s1.m - r.|| <p by A18,XXREAL_0:2;
  end;
  then
A22: s1 is convergent;
  then lim s1 = r by A15,NORMSP_1:def 7;
  then r in X` by A22,A12,A1;
  hence contradiction by A2,XBOOLE_0:def 5;
end;

theorem
  for X being Subset of S st X is open for r be Point of S st r in X
  holds ex g st 0<g & {y where y is Point of S:||.y-r.|| < g} c= X
proof
  let X be Subset of S such that
A1: X is open;
  let r be Point of S;
  assume r in X;
  then consider N be Neighbourhood of r such that
A2: N c= X by A1,Th2;
  consider g such that
A3: 0<g & {y where y is Point of S:||.y-r.|| < g} c= N by NFCONT_1:def 1;
  take g;
  thus thesis by A2,A3;
end;

theorem Th4:
  for X being Subset of S holds ((for r be Point of S st r in X
  holds ex N be Neighbourhood of r st N c= X) implies X is open )
proof
  let X be Subset of S;
  assume that
A1: for r be Point of S st r in X holds ex N be Neighbourhood of r st N
  c= X and
A2: not X is open;
  not X` is closed by A2;
  then consider s1 be sequence of S such that
A3: rng s1 c= X` and
A4: s1 is convergent and
A5: not lim s1 in X`;
  consider N be Neighbourhood of (lim s1) such that
A6: N c= X by A1,A5,SUBSET_1:29;
  consider g be Real such that
A7: 0<g and
A8: {y where y is Point of S:||.y-(lim s1).|| < g} c= N by NFCONT_1:def 1;
  consider n being Nat such that
A9: for m be Nat st n<=m holds ||.(s1.m) - (lim s1).||<g by A4,A7,
NORMSP_1:def 7;
  n in NAT by ORDINAL1:def 12;
  then n in dom s1 by FUNCT_2:def 1;
  then
A10: s1.n in rng s1 by FUNCT_1:def 3;
  ||.s1.n - (lim s1).|| <g by A9;
  then s1.n in {y where y is Point of S:||.y-(lim s1).|| < g};
  then s1.n in N by A8;
  hence contradiction by A3,A6,A10,XBOOLE_0:def 5;
end;

theorem
  for X being Subset of S holds ( (for r be Point of S st r in X holds
  ex N be Neighbourhood of r st N c= X) iff X is open) by Th2,Th4;

:: Normed Linear Spaces versions of SEQ_1: -

definition
  let X be set, S be ZeroStr;
  let f be Function of X,S;
  redefine attr f is non-zero means

  rng f c= NonZero S;
  compatibility
  proof
    thus
    f is non-zero implies rng f c= NonZero S
     by ZFMISC_1:34;
    assume
A1: rng f c= NonZero S;
    assume 0.S in rng f;
    then not 0.S in {0.S} by A1,XBOOLE_0:def 5;
    hence contradiction by TARSKI:def 1;
  end;
end;

theorem Th6:
  seq is non-zero iff for x st x in NAT holds seq.x<>0.S
proof
  thus seq is non-zero implies for x st x in NAT holds seq.x<>0.S
  proof
    assume seq is non-zero;
    then
A1: rng seq c= NonZero S;
    let x;
    assume x in NAT;
    then x in dom seq by FUNCT_2:def 1;
    then seq.x in rng seq by FUNCT_1:def 3;
    then not seq.x in {0.S} by A1,XBOOLE_0:def 5;
    hence thesis by TARSKI:def 1;
  end;
  assume
A2: for x st x in NAT holds seq.x<>0.S;
  now
    let y be object;
    assume
A3: y in rng seq;
    then ex x being object st x in dom seq & seq.x=y by FUNCT_1:def 3;
    then y<>0.S by A2;
    then not y in {0.S} by TARSKI:def 1;
    hence y in NonZero S by A3,XBOOLE_0:def 5;
  end;
  then rng seq c= NonZero S;
  hence thesis;
end;

theorem Th7:
  seq is non-zero iff for n being Nat holds seq.n<>0.S
proof
  thus seq is non-zero implies for n being Nat holds seq.n<>0.S
   by ORDINAL1:def 12,Th6;
  assume for n being Nat holds seq.n<>0.S;
  then for x holds x in NAT implies seq.x<>0.S;
  hence thesis by Th6;
end;

definition
  let RNS be RealLinearSpace;
  let S be sequence of RNS;
  let a be Real_Sequence;
  func a (#) S -> sequence of RNS means
  :Def2:
  for n being Nat holds it.n = a.n * S.n;
  existence
  proof
    deffunc F(Element of NAT) = a.$1 * S.$1;
    consider S being sequence of RNS such that
A1:   for n holds S.n = F(n) from FUNCT_2:sch 4;
   take S;
   let n be Nat;
    n in NAT by ORDINAL1:def 12;
   hence thesis by A1;
  end;
  uniqueness
  proof
    let S1, S2 be sequence of RNS;
    assume that
A2: for n being Nat holds S1.n = a.n * S.n and
A3: for n being Nat holds S2.n = a.n * S.n;
    for n holds S1.n = S2.n
    proof
      let n;
      S1.n = a.n * S.n by A2;
      hence thesis by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let RNS be RealLinearSpace;
  let z be Point of RNS;
  let a be Real_Sequence;
  func a * z -> sequence of RNS means
  :Def3:
  for n being Nat holds it.n = a.n * z;
  existence
  proof
    deffunc F(Element of NAT) = a.$1 * z;
    consider S being sequence of RNS such that
A1:  for n holds S.n = F(n) from FUNCT_2:sch 4;
   take S;
   let n be Nat;
    n in NAT by ORDINAL1:def 12;
   hence thesis by A1;
  end;
  uniqueness
  proof
    let S1, S2 be sequence of RNS;
    assume that
A2: for n being Nat holds S1.n = a.n * z and
A3: for n being Nat holds S2.n = a.n * z;
    for n holds S1.n = S2.n
    proof
      let n;
      S1.n = a.n * z by A2;
      hence thesis by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem
  for rseq1,rseq2 be Real_Sequence holds (rseq1+rseq2)(#)seq=rseq1(#)seq
  +rseq2(#)seq
proof
  let rseq1,rseq2 be Real_Sequence;
  now
    let n;
    thus ((rseq1+rseq2)(#)seq).n =(rseq1+rseq2).n*seq.n by Def2
      .=(rseq1.n+rseq2.n)*seq.n by SEQ_1:7
      .=rseq1.n*seq.n+rseq2.n*seq.n by RLVECT_1:def 6
      .=(rseq1(#)seq).n+rseq2.n*seq.n by Def2
      .=(rseq1(#)seq).n+(rseq2(#)seq).n by Def2
      .=((rseq1(#)seq)+(rseq2(#)seq)).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th9:
  for rseq be Real_Sequence for seq1, seq2 be sequence of S holds
  rseq(#)(seq1+seq2)=rseq(#)seq1+rseq(#)seq2
proof
  let rseq be Real_Sequence;
  let seq1, seq2 be sequence of S;
  now
    let n;
    thus (rseq(#)(seq1+seq2)).n =rseq.n*(seq1+seq2).n by Def2
      .=rseq.n*(seq1.n+seq2.n ) by NORMSP_1:def 2
      .=rseq.n*seq1.n+rseq.n*seq2.n by RLVECT_1:def 5
      .=(rseq(#)seq1).n+rseq.n*seq2.n by Def2
      .=(rseq(#)seq1).n+(rseq(#)seq2).n by Def2
      .=((rseq(#)seq1)+(rseq(#)seq2)).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th10:
  for rseq be Real_Sequence holds r*(rseq(#)seq) =rseq(#)(r*seq)
proof
  let rseq be Real_Sequence;
  now
    let n;
    thus (r*(rseq(#)seq)).n =r*(rseq(#)seq).n by NORMSP_1:def 5
      .=r*(rseq.n*seq.n) by Def2
      .=(r*rseq.n)*seq.n by RLVECT_1:def 7
      .=rseq.n*(r*seq.n) by RLVECT_1:def 7
      .=rseq.n*(r*seq).n by NORMSP_1:def 5
      .=(rseq(#)(r*seq)).n by Def2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  for rseq1,rseq2 be Real_Sequence holds (rseq1-rseq2)(#)seq=rseq1(#)seq
  -rseq2(#)seq
proof
  let rseq1,rseq2 be Real_Sequence;
  now
    let n;
    thus ((rseq1-rseq2)(#)seq).n =(rseq1+-rseq2).n*seq.n by Def2
      .=(rseq1.n+(-rseq2).n)*seq.n by SEQ_1:7
      .=(rseq1.n+-rseq2.n)*seq.n by SEQ_1:10
      .=(rseq1.n-rseq2.n)*seq.n
      .=rseq1.n*seq.n-rseq2.n*seq.n by RLVECT_1:35
      .=(rseq1(#)seq).n-rseq2.n*seq.n by Def2
      .=(rseq1(#)seq).n-(rseq2(#)seq).n by Def2
      .=((rseq1(#)seq)-(rseq2(#)seq)).n by NORMSP_1:def 3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th12:
  for rseq be Real_Sequence for seq1, seq2 be sequence of S holds
  rseq(#)(seq1-seq2)=rseq(#)seq1-rseq(#)seq2
proof
  let rseq be Real_Sequence;
  let seq1, seq2 be sequence of S;
  now
    let n;
    thus (rseq(#)(seq1-seq2)).n =rseq.n*(seq1-seq2).n by Def2
      .=rseq.n*(seq1.n-seq2.n ) by NORMSP_1:def 3
      .=rseq.n*seq1.n-rseq.n*seq2.n by RLVECT_1:34
      .=(rseq(#)seq1).n-rseq.n*seq2.n by Def2
      .=(rseq(#)seq1).n-(rseq(#)seq2).n by Def2
      .=((rseq(#)seq1)-(rseq(#)seq2)).n by NORMSP_1:def 3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th13:
  rseq is convergent & seq is convergent implies rseq (#) seq is convergent
proof
  assume that
A1: rseq is convergent and
A2: seq is convergent;
  consider g1 be Real such that
A3: for p be Real st 0<p ex n be Nat st for m be
  Nat st n<=m holds |.rseq.m-g1.|<p by A1,SEQ_2:def 6;
  consider g2 be Point of S such that
A4: for p be Real st 0<p
   ex n be Nat st for m be Nat st n<=m holds ||.seq.m-g2.||<p
    by A2;
  reconsider g1 as Real;
  take g=g1*g2;
  let p;
  rseq is bounded by A1,SEQ_2:13;
  then consider r be Real such that
A5: 0<r and
A6: for n be Nat holds |.rseq.n.|<r by SEQ_2:3;
  reconsider r as Real;
A7: 0+0<||.g2.||+r by A5,NORMSP_1:4,XREAL_1:8;
  assume
A8: 0<p;
  then consider n1 be Nat such that
A9: for m be Nat st n1<=m holds |.rseq.m-g1.|<p/(||.g2.||+r
  ) by A3,A7,XREAL_1:139;
  consider n2 be Nat such that
A10: for m be Nat st n2<=m holds ||.seq.m-g2.||<p/(||.g2.||+r
  ) by A4,A7,A8,XREAL_1:139;
   reconsider n=n1+n2 as Nat;
  take n;
  let m be Nat such that
A11: n<=m;
  n1<=n1+n2 by NAT_1:12;
  then n1<=m by A11,XXREAL_0:2;
  then
A12: |.rseq.m-g1.|<=p/(||.g2.||+r) by A9;
  0<=||.g2.|| & ||.(rseq.m-g1)*g2.||=||.g2.||*|.rseq.m-g1.| by NORMSP_1:4
,def 1;
  then
A13: ||.(rseq.m-g1)*g2.||<=||.g2.||*(p/(||.g2.||+r)) by A12,XREAL_1:64;
  ||.((rseq(#)seq).m)-g.|| =||.rseq.m*seq.m-g1*g2.|| by Def2
    .=||.rseq.m*seq.m-0.S-g1*g2.|| by RLVECT_1:13
    .=||.rseq.m*seq.m-(rseq.m*g2-rseq.m*g2)-g1*g2.|| by RLVECT_1:15
    .=||.(rseq.m*seq.m-rseq.m*g2+rseq.m*g2)-g1*g2.|| by RLVECT_1:29
    .=||.rseq.m*(seq.m-g2)+rseq.m*g2-g1*g2.|| by RLVECT_1:34
    .=||.rseq.m*(seq.m-g2)+(rseq.m*g2-g1*g2).|| by RLVECT_1:def 3
    .=||.rseq.m*(seq.m-g2)+(rseq.m-g1)*g2.|| by RLVECT_1:35;
  then
A14: ||.((rseq(#)seq).m)-g.||<= ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2.||
  by NORMSP_1:def 1;
  n2<=n by NAT_1:12;
  then n2<=m by A11,XXREAL_0:2;
  then
A15: ||.seq.m-g2.||<p/(||.g2.||+r) by A10;
A16: 0<=|.rseq.m.| & 0<=||.seq.m-g2.|| by COMPLEX1:46,NORMSP_1:4;
  |.rseq.m.|<r by A6;
  then |.rseq.m.|*||.seq.m-g2.||<r*(p/(||.g2.||+r)) by A16,A15,XREAL_1:96;
  then
A17: ||.rseq.m*(seq.m-g2).||<r*(p/(||.g2.||+r)) by NORMSP_1:def 1;
  r*(p/(||.g2.||+r))+||.g2.||*(p/(||.g2.||+r)) =(p/(||.g2.||+r))*(||.g2 .||+r)
    .=p by A7,XCMPLX_1:87;
  then ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2.||<p by A17,A13,XREAL_1:8;
  hence thesis by A14,XXREAL_0:2;
end;

theorem Th14:
  rseq is convergent & seq is convergent implies lim (rseq (#) seq
  ) = (lim rseq) * (lim seq)
proof
  assume that
A1: rseq is convergent and
A2: seq is convergent;
  set g2= lim seq;
  reconsider g1 = lim rseq as Real;
  set g=g1*g2;
  rseq is bounded by A1,SEQ_2:13;
  then consider r be Real such that
A3: 0<r and
A4: for n be Nat holds |.rseq.n.|<r by SEQ_2:3;
  reconsider r as Real;
A5: 0+0<||.g2.||+r by A3,NORMSP_1:4,XREAL_1:8;
A6: 0<=||.g2.|| by NORMSP_1:4;
A7: for p be Real st 0<p
  ex n be Nat st for m be Nat
  st n <=m holds ||.((rseq(#)seq).m)-g.||<p
  proof
    let p be Real;
    assume 0<p;
    then
A8: 0<p/(||.g2.||+r) by A5,XREAL_1:139;
    then consider n1 be Nat such that
A9: for m be Nat st n1<=m holds |.rseq.m-g1.|<p/(||.g2.||
    +r) by A1,SEQ_2:def 7;
    consider n2 be Nat such that
A10: for m be Nat  st n2<=m holds ||.seq.m-g2.||<p/(||.g2.||
    +r) by A2,A8,NORMSP_1:def 7;
    take n=n1+n2;
    let m be Nat such that
A11: n<=m;
    n1<=n1+n2 by NAT_1:12;
    then n1<=m by A11,XXREAL_0:2;
    then
A12: |.rseq.m-g1.|<=p/(||.g2.||+r) by A9;
    ||.(rseq.m-g1)*g2.||=||.g2.||*|.rseq.m-g1.| by NORMSP_1:def 1;
    then
A13: ||.(rseq.m-g1)*g2.||<=||.g2.||*(p/(||.g2.||+r)) by A6,A12,XREAL_1:64;
A14: 0<=|.rseq.m.| & 0<=||.seq.m-g2.|| by COMPLEX1:46,NORMSP_1:4;
    n2<=n by NAT_1:12;
    then n2<=m by A11,XXREAL_0:2;
    then
A15: ||.seq.m-g2.||<p/(||.g2.||+r) by A10;
    ||.((rseq(#)seq).m)-g.|| =||.rseq.m*seq.m-g1*g2.|| by Def2
      .=||.rseq.m*seq.m-0.S-g1*g2.|| by RLVECT_1:13
      .=||.rseq.m*seq.m-(rseq.m*g2-rseq.m*g2)-g1*g2.|| by RLVECT_1:15
      .=||.(rseq.m*seq.m-rseq.m*g2+rseq.m*g2)-g1*g2.|| by RLVECT_1:29
      .=||.rseq.m*(seq.m-g2)+rseq.m*g2-g1*g2.|| by RLVECT_1:34
      .=||.rseq.m*(seq.m-g2)+(rseq.m*g2-g1*g2).|| by RLVECT_1:def 3
      .=||.rseq.m*(seq.m-g2)+(rseq.m-g1)*g2.|| by RLVECT_1:35;
    then
A16: ||.((rseq(#)seq).m)-g.||<= ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2
    .|| by NORMSP_1:def 1;
    |.rseq.m.|<r by A4;
    then |.rseq.m.|*||.seq.m-g2.||<r*(p/(||.g2.||+r)) by A14,A15,XREAL_1:96;
    then
A17: ||.rseq.m*(seq.m-g2).||<r*(p/(||.g2.||+r)) by NORMSP_1:def 1;
    r*(p/(||.g2.||+r))+||.g2.||*(p/(||.g2.||+r)) =(p/(||.g2.||+r))*(||.g2
    .||+r)
      .=p by A5,XCMPLX_1:87;
    then ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2.||<p by A17,A13,XREAL_1:8;
    hence thesis by A16,XXREAL_0:2;
  end;
  (rseq (#) seq) is convergent by A1,A2,Th13;
  hence thesis by A7,NORMSP_1:def 7;
end;

theorem Th15:
 for k being Nat
  holds (seq+seq1) ^\k=(seq ^\k) +(seq1 ^\k)
proof let k be Nat;
  now
    let n;
    thus ((seq+seq1) ^\k).n=(seq+seq1).(n+k) by NAT_1:def 3
      .=seq.(n+k) + seq1.(n+k) by NORMSP_1:def 2
      .=(seq ^\k).n +seq1.(n+k) by NAT_1:def 3
      .=(seq ^\k).n +(seq1 ^\k).n by NAT_1:def 3
      .=((seq ^\k) +(seq1 ^\k)).n by NORMSP_1:def 2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th16:
  (seq-seq1) ^\k=(seq ^\k) -(seq1 ^\k)
proof
  now
    let n;
    thus ((seq-seq1) ^\k).n=(seq-seq1).(n+k) by NAT_1:def 3
      .=seq.(n+k) - seq1.(n+k) by NORMSP_1:def 3
      .=(seq ^\k).n -seq1.(n+k) by NAT_1:def 3
      .=(seq ^\k).n -(seq1 ^\k).n by NAT_1:def 3
      .=((seq ^\k) -(seq1 ^\k)).n by NORMSP_1:def 3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th17:
  seq is non-zero implies seq ^\k is non-zero
proof
  assume
A1: seq is non-zero;
  now
    let n be Nat;
    (seq ^\k).n=seq.(n+k) by NAT_1:def 3;
    hence (seq ^\k).n<>0.S by A1,Th7;
  end;
  hence thesis by Th7;
end;

definition
  let S;
  let x be Point of S;
  let IT be sequence of S;
  attr IT is x-convergent means
  :Def4:
  IT is convergent & lim IT = x;
end;

theorem Th18:
  for X be RealNormSpace for seq be sequence of X holds seq is
constant implies ( seq is convergent & for k be Element of NAT holds lim seq =
  seq.k )
proof
  let X be RealNormSpace;
  let seq be sequence of X;
  assume
A1: seq is constant;
  then consider r be Point of X such that
A2: for n be Nat holds seq.n=r by VALUED_0:def 18;
  thus
A3: seq is convergent by A1,LOPBAN_3:12;
  now
    let k be Element of NAT;
    now
      let p be Real such that
A4:   0<p;
       reconsider n=0 as Nat;
      take n;
      let m be Nat such that
      n<=m;
      ||.(seq.m)-(seq.k).||=||.r-(seq.k).|| by A2
        .=||.r-r.|| by A2
        .=||.0.X.|| by RLVECT_1:15
        .=0 by NORMSP_1:1;
      hence ||.(seq.m)-(seq.k).||<p by A4;
    end;
    hence lim seq = seq.k by A3,NORMSP_1:def 7;
  end;
  hence thesis;
end;

theorem Th19:
  for r be Real st 0<r & (for n being Nat holds seq.n=(1/(n+r))*x0) holds
  seq is convergent
proof
  let r be Real;
  assume that
A1: 0<r and
A2: for n being Nat holds seq.n=(1/(n+r))*x0;
  take g = 0.S;
  let p be Real;
  assume
A3: 0<p;
  ex pp be Real st pp > 0 & pp*||.x0.|| < p
  proof
    take pp=p/(||.x0.||+1);
A4: ||.x0.||+0 < ||.x0.||+1 & 0 <= ||.x0.|| by NORMSP_1:4,XREAL_1:8;
A5: ||.x0.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
    then 0 < p/( ||.x0.||+1 ) by A3,XREAL_1:139;
    then pp* ||.x0.|| < pp*(||.x0.|| + 1) by A4,XREAL_1:97;
    hence thesis by A3,A5,XCMPLX_1:87;
  end;
  then consider pp be Real such that
A6: pp > 0 and
A7: pp*||.x0.|| < p;
  consider k1 be Nat such that
A8: pp"<k1 by SEQ_4:3;
  pp"+0<k1+r by A1,A8,XREAL_1:8;
  then 1/(k1+r)<1/pp" by A6,XREAL_1:76;
  then
A9: 1/(k1+r)<1*pp"" by XCMPLX_0:def 9;
   reconsider k1 as Element of NAT by ORDINAL1:def 12;
  take n=k1;
  let m be Nat;
  assume n<=m;
  then
A10: n+r<=m+r by XREAL_1:6;
A11: 0 <= ||.x0.|| by NORMSP_1:4;
  1/(m+r)<=1/(n+r) by A1,A10,XREAL_1:118;
  then 1/(m+r)<pp by A9,XXREAL_0:2;
  then
A12: (1/(m+r))*||.x0.|| <= pp* ||.x0.|| by A11,XREAL_1:64;
  ||.seq.m-g.|| = ||.(1/(m+r))*x0 - 0.S.|| by A2
    .= ||.(1/(m+r))*x0.|| by RLVECT_1:13
    .= |.1/(m+r).|*||.x0.|| by NORMSP_1:def 1
    .= (1/(m+r))*||.x0.|| by A1,ABSVALUE:def 1;
  hence thesis by A7,A12,XXREAL_0:2;
end;

theorem Th20:
  for r be Real st 0<r &
   (for n being Nat holds seq.n=(1/(n+r))*x0 ) holds lim seq=0.S
proof
  let r be Real;
  assume that
A1: 0<r and
A2: for n being Nat holds seq.n=1/(n+r)*x0;
A3: now
    let p;
A4: 0 <= ||.x0.|| by NORMSP_1:4;
    assume
A5: 0<p;
    ex pp be Real st pp > 0 & pp*||.x0.|| < p
    proof
      take pp=p/(||.x0.||+1);
A6:   ||.x0.||+0 < ||.x0.||+1 & 0 <= ||.x0.|| by NORMSP_1:4,XREAL_1:8;
A7:   ||.x0.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
      then 0 < p/(||.x0.||+1) by A5,XREAL_1:139;
      then pp* ||.x0.|| < pp*(||.x0.|| + 1) by A6,XREAL_1:97;
      hence thesis by A5,A7,XCMPLX_1:87;
    end;
    then consider pp be Real such that
A8: pp > 0 and
A9: pp*||.x0.|| < p;
    consider k1 be Nat such that
A10: pp"<k1 by SEQ_4:3;
    pp"+0<k1+r by A1,A10,XREAL_1:8;
    then 1/(k1+r)<1/pp" by A8,XREAL_1:76;
    then
A11: 1/(k1+r)<1*pp"" by XCMPLX_0:def 9;
     reconsider n=k1 as Nat;
    take n;
    let m be Nat;
    assume n<=m;
    then
A12: n+r<=m+r by XREAL_1:6;
    1/(m+r)<=1/(n+r) by A1,A12,XREAL_1:118;
    then 1/(m+r)<pp by A11,XXREAL_0:2;
    then
A13: (1/(m+r))*||.x0.|| <= pp* ||.x0.|| by A4,XREAL_1:64;
    ||.seq.m-0.S.|| = ||.(1/(m+r))*x0 - 0.S.|| by A2
      .= ||.(1/(m+r))*x0.|| by RLVECT_1:13
      .= |.1/(m+r).|*||.x0.|| by NORMSP_1:def 1
      .= (1/(m+r))*||.x0.|| by A1,ABSVALUE:def 1;
    hence ||.seq.m-0.S.||<p by A9,A13,XXREAL_0:2;
  end;
  seq is convergent by A1,A2,Th19;
  hence thesis by A3,NORMSP_1:def 7;
end;

registration
  let S be non trivial RealNormSpace;
  cluster non-zero (0.S)-convergent for sequence of S;
  existence
  proof
    consider x0 be Point of S such that
A1: x0 <> 0.S by STRUCT_0:def 18;
    deffunc F(Nat) = (1/($1+1))*x0;
    consider s1 be sequence of S such that
A2: for n holds s1.n=F(n) from FUNCT_2:sch 4;
A3: for n being Nat holds s1.n=F(n)
     proof let n be Nat;
       n in NAT by ORDINAL1:def 12;
      hence thesis by A2;
     end;
    take s1;
    now
      let n be Nat;
      (n+1)" <> 0;
      then
A4:   1/(n+1) <> 0 by XCMPLX_1:215;
      thus s1.n <> 0.S
      proof
        assume s1.n = 0.S;
        then (1/(n+1))*x0 = 0.S by A3;
        hence contradiction by A1,A4,RLVECT_1:11;
      end;
    end;
    hence s1 is non-zero by Th7;
A5: lim s1 = 0.S by A3,Th20;
    s1 is convergent by A3,Th19; then
    s1 is (0.S)-convergent by A5;
    hence thesis;
  end;
end;

registration
  let S be RealNormSpace;
  cluster  (0.S)-convergent for sequence of S;
  existence
  proof

 set x0 = the Point of S ;
    deffunc F(Nat) = (1/($1+1))*x0;
    consider s1 be sequence of S such that
A1: for n holds s1.n=F(n) from FUNCT_2:sch 4;
A2: for n being Nat holds s1.n=F(n)
     proof let n be Nat;
       n in NAT by ORDINAL1:def 12;
      hence thesis by A1;
     end;
    take s1;
A3: lim s1 = 0.S by A2,Th20;
    s1 is convergent by A2,Th19; then
    s1 is (0.S)-convergent by A3;
    hence thesis;
  end;
end;


theorem
  for a be 0-convergent non-zero Real_Sequence
    for z be Point of S st z <> 0.S
  holds a*z is non-zero (0.S)-convergent
proof
  let a be 0-convergent non-zero Real_Sequence;
  let z be Point of S such that
A1: z <> 0.S;
  now
    let n be Nat;
A2: a.n <> 0 by SEQ_1:5;
    assume (a*z).n = 0.S;
    then a.n*z = 0.S by Def3;
    hence contradiction by A1,A2,RLVECT_1:11;
  end;
  hence a*z is non-zero by Th7;
A3: now
    let p;
    assume
A4: 0<p;
    ex pp be Real st pp > 0 & pp*||.z.|| < p
    proof
      take pp=p/(||.z.||+1);
A5:   ||.z.||+0 < ||.z.||+1 & 0 <= ||.z.|| by NORMSP_1:4,XREAL_1:8;
A6:   ||.z.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
      then 0 < p/(||.z.||+1) by A4,XREAL_1:139;
      then pp* ||.z.|| < pp*(||.z.|| + 1) by A5,XREAL_1:97;
      hence thesis by A4,A6,XCMPLX_1:87;
    end;
    then consider pp be Real such that
A7: pp > 0 and
A8: pp*||.z.|| < p;
    a is convergent & lim a =0;
    then consider n be Nat such that
A9: for m be Nat st n <= m holds |.a.m- 0 .| < pp by A7,SEQ_2:def 7;
    reconsider n as Nat;
    take n;
    let m be Nat;
    assume n<=m;
    then
A10: |.a.m-0 .| < pp by A9;
A11: ||.(a*z).m-0.S.|| = ||.a.m*z - 0.S.|| by Def3
      .= ||.a.m*z.|| by RLVECT_1:13
      .= |.a.m.|*||.z.|| by NORMSP_1:def 1;
    0 <= ||.z.|| by NORMSP_1:4;
    then |.a.m.|*||.z.|| <= pp* ||.z.|| by A10,XREAL_1:64;
    hence ||.(a*z).m-0.S.||<p by A8,A11,XXREAL_0:2;
  end;
  hence a*z is convergent;
  hence thesis by A3,NORMSP_1:def 7;
end;

theorem
  (for r be Point of S holds r in Y iff r in the carrier of S) iff Y=the
  carrier of S
proof
  thus (for r be Point of S holds r in Y iff r in the carrier of S) implies Y=
  the carrier of S
  proof
    assume for r be Point of S holds r in Y iff r in the carrier of S;
    then for y being object holds y in Y iff y in the carrier of S;
    hence thesis by TARSKI:2;
  end;
  assume
A1: Y=the carrier of S;
  let r be Point of S;
  thus r in Y implies r in the carrier of S;
  thus thesis by A1;
end;

reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve s1 for sequence of S;
reserve x0 for Point of S;

registration
  let S;
  cluster constant for sequence of S;
  existence
  proof
    reconsider s1 = NAT --> 0.S as sequence of S;
    take s1;
    thus thesis;
  end;
end;

:: Normed Linear Spaces versions of FDIFF_1

reserve h for (0.S)-convergent sequence of S;
reserve c for constant sequence of S;

definition
  let S,T;
  let IT be PartFunc of S,T;
  attr IT is RestFunc-like means
  :Def5:
  IT is total & for h st h is non-zero holds (||.h.||")(#)(IT
  /*h) is convergent & lim ((||.h.||")(#)(IT/*h)) = 0.T;
end;

registration
  let S,T;
  cluster RestFunc-like for PartFunc of S,T;
  existence
  proof
    reconsider f = (the carrier of S) --> 0.T as PartFunc of S,T;
    take f;
    thus f is total;
A1: dom f = the carrier of S;
    now
      let h ;
      assume  h is non-zero ;
      now
        let n be Nat;
A2:     f/.(h.n) =f.(h.n) by A1,PARTFUN1:def 6
          .=0.T;
A3:     rng h c= dom f;
A4:     n in NAT by ORDINAL1:def 12;
        thus ((||.h.||")(#)(f/*h)).n = (||.h.||").n*((f/*h).n) by Def2
          .= (||.h.||").n*(f/.(h.n)) by A3,A4,FUNCT_2:109
          .= 0.T by A2,RLVECT_1:10;
      end;
      then (||.h.||")(#)(f/*h) is constant & ((||.h.||")(#)(f/*h)).0 = 0.T by
VALUED_0:def 18;
      hence
      (||.h.||")(#)(f/*h) is convergent & lim ((||.h.||")(#)(f/*h)) = 0.T
      by Th18;
    end;
    hence thesis;
  end;
end;

definition
  let S,T;
  mode RestFunc of S,T is RestFunc-like PartFunc of S,T;
end;

theorem
  for R be PartFunc of S,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 Point of S st z <> 0.S &
  ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r
proof
  let R be PartFunc of S,T such that
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 Point
    of S st z <> 0.S & ||.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
    ex z be Point of S st z <> 0.S & ||.z
    .|| < d & not ( ||.z.||"* ||. R/.z .||) < r;
    defpred P[Nat,Point of S] means $2 <> 0.S & ||.$2.|| < (1/($1+1
    )) & not ( ( ||.$2.||"* ||. R/.$2 .||) < r );
A6: for n be Element of NAT ex z be Point of S st P[n,z]
    proof
      let n be Element of NAT;
      0 < 1 * (n + 1)";
      then 0 < 1/(n + 1) by XCMPLX_0:def 9;
      hence thesis by A5;
    end;
    consider s be sequence of S such that
A7: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6);
A8: for n being Nat holds P[n,s.n]
     proof let n be Nat;
       n in NAT by ORDINAL1:def 12;
      hence thesis by A7;
     end;
A9: now
      let p be Real;
      assume
A10:   0<p;
      consider n being Nat such that
A11:  p"<n by SEQ_4:3;
      p" + 0 < n + 1 by A11,XREAL_1:8;
      then 1/(n+1) < 1/p" by A10,XREAL_1:76;
      then
A12:  1/(n+1) < p by XCMPLX_1:216;
       reconsider n as Nat;
      take n;
      let m be Nat;
      assume n<=m;
      then
A13:  n + 1 <= m + 1 by XREAL_1:6;
      ||.s.m.|| < (1/(m+1)) by A8;
      then
A14:  ||.s.m-0.S.|| < (1/(m+1)) by RLVECT_1:13;
      1/(m+1) <= 1/(n+1) by A13,XREAL_1:118;
      then ||.s.m - 0.S.|| < 1/(n+1) by A14,XXREAL_0:2;
      hence ||.s.m - 0.S.|| <p by A12,XXREAL_0:2;
    end;
    then
A15: s is convergent;
    then
    lim s = 0.S by A9,NORMSP_1:def 7;
    then reconsider s as (0.S)-convergent sequence of S
      by A15,Def4;
    s is non-zero by A8,Th7;
    then
    (||.s.||")(#)(R/*s) is convergent & lim ((||.s.||")(#)(R/*s)) = 0.T
    by A3;
    then consider n be Nat such that
A16: for m be Nat st n <=m holds ||. ((||.s.||")(#)(R/*s)).
    m- 0.T.|| < r by A4,NORMSP_1:def 7;
A17:   n in NAT by ORDINAL1:def 12;
A18: ||. ((||.s.||")(#)(R/*s)).n- 0.T.|| < r by A16;
    s.n <> 0.S by A8;
    then ||.s.n.|| <> 0 by NORMSP_0:def 5;
    then
A19: ||.s.n.|| > 0 by NORMSP_1:4;
A20: ||.(||.s.n.||)"*(R/.(s.n)).|| = |.(||.s.n.||)".| * ||.(R/.(s.n)).||
    by NORMSP_1:def 1
      .=(||.s.n.||)" * ||.(R/.(s.n)).|| by A19,ABSVALUE:def 1;
    dom R = the carrier of S by A1,PARTFUN1:def 2;
    then
A21: 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 Def2
      .= ||.(||.s.||.n)"*((R/*s).n).|| by VALUED_1:10
      .= ||.(||.s.n.||)"*((R/*s).n).|| by NORMSP_0:def 4
      .= ||.(||.s.n.||)"*(R/.(s.n)).|| by A21,FUNCT_2:109,A17;
    hence
    for r be Real
    st r > 0 ex d be Real st d > 0 & for z be Point of S st
    z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r
               by A8,A18,A20;
  end;
  now
    assume
A22: for r be Real st r > 0
    ex d be Real st d > 0 & for z be Point of
    S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r;
    now
      let s be (0.S)-convergent sequence of S
         such that A23: s is non-zero;
A24:  s is convergent & lim s = 0.S by Def4;
A25:  now
        let r be Real;
        assume r > 0;
        then consider d be Real such that
A26:    d > 0 and
A27:    for z be Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||
        "* ||. R/.z .||) < r by A22;
        consider n be Nat such that
A28:    for m be Nat st n <=m holds ||.s.m-0.S.|| < d by A24,A26,
NORMSP_1:def 7;
        take n;
        thus for m be Nat st n <=m holds ||. ((||.s.||")(#)(R/*s)).
        m- 0.T.|| < r
        proof
          dom R = the carrier of S by A1,PARTFUN1:def 2;
          then
A29:      rng s c= dom R;
          let m be Nat;
A30:   m in NAT by ORDINAL1:def 12;
          assume n <=m;
          then ||.s.m-0.S .|| < d by A28;
          then
A31:      ||.s.m.|| < d by RLVECT_1:13;
A32:      s.m <> 0.S by Th7,A23;
          then ||.s.m.|| <> 0 by NORMSP_0:def 5;
          then ||.s.m.|| > 0 by NORMSP_1:4;
          then
          (||.s.m.||)" * ||.(R/.(s.m)).|| =|.(||.s.m.||)".| * ||.(R/.(s.
          m)).|| by ABSVALUE:def 1
            .= ||.(||.s.m.||)"*(R/.(s.m)).|| by NORMSP_1:def 1
            .= ||.(||.s.m.||)"*((R/*s).m).|| by A29,FUNCT_2:109,A30
            .= ||.(||.s.||.m)"*((R/*s).m).|| by NORMSP_0:def 4
            .= ||.(||.s.||".m)*((R/*s).m).|| by VALUED_1:10
            .= ||. ((||.s.||")(#)(R/*s)).m .|| by Def2
            .= ||. ((||.s.||")(#)(R/*s)).m- 0.T.|| by RLVECT_1:13;
          hence thesis by A27,A31,A32;
        end;
      end;
      hence (||.s.||")(#)(R/*s) is convergent;
      hence lim ((||.s.||")(#)(R/*s)) = 0.T by A25,NORMSP_1:def 7;
    end;
    hence R is RestFunc-like by A1;
  end;
  hence thesis by A2;
end;

theorem Th24:
  for R be RestFunc of S,T for s be (0.S)-convergent sequence of S
   st s is non-zero
  holds (R/*s) is convergent & lim (R/*s) = 0.T
proof
  let R be RestFunc of S,T;
  let s be (0.S)-convergent sequence of S
  such that A1: s is non-zero ;
A2: (||.s.||") (#) (R/*s) is convergent by Def5,A1;
  now
    let n be Element of NAT;
    s.n <> 0.S by Th7,A1;
    then
A3: ||.s.n.|| <> 0 by NORMSP_0:def 5;
    thus (||.s.||(#) ( (||.s.||") (#) (R/*s) )).n =||.s.||.n*((||.s.||")(#)(R
    /*s)).n by Def2
      .=||.s.||.n*((||.s.||").n*((R/*s).n)) by Def2
      .= ||.s.n.||*((||.s.||").n*((R/*s).n)) by NORMSP_0:def 4
      .= ||.s.n.||*((||.s.||.n)"*((R/*s).n)) by VALUED_1:10
      .= ||.s.n.||*((||.s.n.||)"*((R/*s).n)) by NORMSP_0:def 4
      .= ||.s.n.||*(||.s.n.||)"*((R/*s).n) by RLVECT_1:def 7
      .= 1*(R/*s).n by A3,XCMPLX_0:def 7
      .=(R/*s).n by RLVECT_1:def 8;
  end;
  then
A4: ||.s.||(#) ( (||.s.||") (#) (R/*s) )= (R/*s) by FUNCT_2:63;
A5: s is convergent by Def4;
  then
A6: ||.s.|| is convergent by LOPBAN_1:41;
  lim s = 0.S by Def4;
  then lim ( ||.s.|| ) = ||.0.S.|| by A5,LOPBAN_1:41;
  then
A7: lim ( ||.s.|| ) =0 by NORMSP_1:1;
  lim ((||.s.||") (#) (R/*s) ) = 0.T by Def5,A1;
  then lim (R/*s) = 0* 0.T by A5,A4,A2,A7,Th14,LOPBAN_1:41;
  hence thesis by A4,A2,A6,Th13,RLVECT_1:10;
end;

reserve R,R1,R2 for RestFunc of S,T;
reserve L,L1,L2 for Point of R_NormSpace_of_BoundedLinearOperators(S,T);

theorem Th25:
  for h1,h2 be PartFunc of S,T for seq be sequence of S holds h1
is total & h2 is total implies (h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq
  = h1/*seq - h2/*seq
proof
  let h1,h2 be PartFunc of S,T;
  let seq be sequence of S;
  assume h1 is total & h2 is total;
  then h1+h2 is total by VFUNCT_1:32;
  then dom (h1+h2) = the carrier of S by PARTFUN1:def 2;
  then dom h1 /\ dom h2 = the carrier of S by VFUNCT_1:def 1;
  then
A1: rng seq c= dom h1 /\ dom h2;
  hence (h1+h2)/*seq = h1/*seq + h2/*seq by NFCONT_1:12;
  thus thesis by A1,NFCONT_1:12;
end;

theorem Th26:
  for h be PartFunc of S,T for seq be sequence of S for r be Real
  holds h is total implies (r(#)h)/*seq = r*(h/*seq)
proof
  let h be PartFunc of S,T;
  let seq be sequence of S;
  let r be Real;
  assume h is total;
  then dom h = the carrier of S by PARTFUN1:def 2;
  then rng seq c= dom h;
  hence thesis by NFCONT_1:13;
end;

theorem Th27:
  f is_continuous_in x0 iff x0 in dom f & for s1 be sequence of S
  st rng s1 c= dom f & s1 is convergent & lim s1=x0 &
   (for n being Nat holds s1.n<>x0)
  holds f/*s1 is convergent & f/.x0=lim(f/*s1)
proof
  thus f is_continuous_in x0 implies x0 in dom f & for s1 be sequence of S st
rng s1 c= dom f & s1 is convergent & lim s1=x0 &
  (for n being Nat holds s1.n<>x0) holds f
  /*s1 is convergent & f/.x0=lim(f/*s1);
  assume that
A1: x0 in dom f and
A2: for s1 st rng s1 c=dom f & s1 is convergent & lim s1=x0 & (for n being Nat
  holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1);
  thus x0 in dom f by A1;
  let s2 be sequence of S such that
A3: rng s2 c=dom f and
A4: s2 is convergent & lim s2=x0;
  now
    per cases;
    suppose
      ex n st for m be Element of NAT st n<=m holds s2.m=x0;
      then consider N be Element of NAT such that
A5:   for m be Element of NAT st N<=m holds s2.m=x0;
A6:   for n holds (s2^\N).n=x0
      proof
        let n;
        s2.(n+N)=x0 by A5,NAT_1:12;
        hence thesis by NAT_1:def 3;
      end;
A7:   rng (s2^\N) c= rng s2 by VALUED_0:21;
A8:   now
        let p be Real such that
A9:     p>0;
         reconsider n=0 as Nat;
        take n;
        let m be Nat such that
        n<=m;
A10:   m in NAT by ORDINAL1:def 12;
        ||.(f/*(s2^\N)).m-f/.x0.|| =||.f/.((s2^\N).m)-f/.x0.|| by A3,A7,
FUNCT_2:109,XBOOLE_1:1,A10
          .=||.f/.x0-f/.x0.|| by A6,A10
          .=||.0.T.|| by RLVECT_1:15
          .=0 by NORMSP_1:1;
        hence ||.(f/*(s2^\N)).m-f/.x0.||< p by A9;
      end;
      then
A11:  f/*(s2^\N) is convergent;
A12:  f/*(s2^\N)=(f/*s2)^\N by A3,VALUED_0:27;
      then
A13:  f/*s2 is convergent by A11,LOPBAN_3:10;
      f/.x0=lim((f/*s2)^\N) by A8,A11,A12,NORMSP_1:def 7;
      hence thesis by A13,LOPBAN_3:9;
    end;
    suppose
A14:  for n ex m be Element of NAT st n<=m & s2.m<>x0;
      defpred P[Nat,set,set] means for n,m be Element of NAT st $2=
      n & $3=m holds n<m & s2.m<>x0 & for k st n<k & s2.k<>x0 holds m<=k;
      defpred P[Nat] means s2.$1<>x0;
      ex m1 be Element of NAT st 0<=m1 & s2.m1<>x0 by A14;
      then
A15:  ex m be Nat st P[m];
      consider M be Nat such that
A16:  P[M] & for n be Nat st P[n] holds M<=n from NAT_1:sch 5(A15);
      reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A17:  now
        let n;
        consider m be Element of NAT such that
A18:    n+1<=m & s2.m<>x0 by A14;
        take m;
        thus n<m & s2.m<>x0 by A18,NAT_1:13;
      end;
A19:  for n being Nat
       for x be Element of NAT ex y be Element of NAT st P[n,x,y]
      proof
        let n be Nat;
        let x be Element of NAT;
        defpred P[Nat] means x<$1 & s2.$1<>x0;
        ex m be Element of NAT st P[m] by A17;
        then
A20:    ex m be Nat st P[m];
        consider l be Nat such that
A21:    P[l] & for k be Nat st P[k] holds l<=k from NAT_1:sch 5(A20);
        reconsider l as Element of NAT by ORDINAL1:def 12;
        take l;
        thus thesis by A21;
      end;
      consider F be sequence of NAT such that
A22:  F.0=M9 & for n be Nat holds P[n,F.n,F.(n+1)] from
      RECDEF_1:sch 2(A19);
A23:  rng F c= REAL by NUMBERS:19;
A24:  rng F c= NAT;
A25:  dom F=NAT by FUNCT_2:def 1;
      then reconsider F as Real_Sequence by A23,RELSET_1:4;
A26:  now
        let n;
        F.n in rng F by A25,FUNCT_1:def 3;
        hence F.n is Element of NAT by A24;
      end;
      now
        let n be Nat;
A27:      n in NAT by ORDINAL1:def 12;
        F.n is Element of NAT & F.(n+1) is Element of NAT by A26,A27;
        hence F.n<F.(n+1) by A22;
      end;
      then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A28:  s2*F is convergent & lim (s2*F)=x0 by A4,LOPBAN_3:7,8;
A29:  for n st s2.n<>x0 ex m be Element of NAT st F.m=n
      proof
        defpred P[Nat] means s2.$1<>x0 & for m be Element of NAT holds F.m<>$1;
        assume ex n st P[n];
        then
A30:    ex n be Nat st P[n];
        consider M1 be Nat such that
A31:    P[M1] & for n be Nat st P[n] holds M1<=n from NAT_1:sch 5(A30
        );
        defpred P[Nat] means $1<M1 & s2.$1<>x0 & ex m be Element of NAT st F.m
        =$1;
A32:    ex n be Nat st P[n]
        proof
          take M;
          M<=M1 & M <> M1 by A16,A22,A31;
          hence M<M1 by XXREAL_0:1;
          thus s2.M<>x0 by A16;
          take 0;
          thus thesis by A22;
        end;
A33:    for n be Nat st P[n] holds n<=M1;
        consider MX be Nat such that
A34:    P[MX] & for n be Nat st P[n] holds n<=MX from NAT_1:sch 6(A33
        ,A32);
A35:    for k st MX<k & k<M1 holds s2.k=x0
        proof
          given k such that
A36:      MX<k and
A37:      k<M1 & s2.k<>x0;
          now
            per cases;
            suppose
              ex m be Element of NAT st F.m=k;
              hence contradiction by A34,A36,A37;
            end;
            suppose
              for m be Element of NAT holds F.m<>k;
              hence contradiction by A31,A37;
            end;
          end;
          hence contradiction;
        end;
        consider m be Element of NAT such that
A38:    F.m=MX by A34;
A39:    MX<F.(m+1) & s2.(F.(m+1))<>x0 by A22,A38;
        M1 in NAT by ORDINAL1:def 12;
        then
A40:    F.(m+1)<=M1 by A22,A31,A34,A38;
        now
          assume F.(m+1)<>M1;
          then F.(m+1)<M1 by A40,XXREAL_0:1;
          hence contradiction by A35,A39;
        end;
        hence contradiction by A31;
      end;
A41:  for n being Nat holds (s2*F).n<>x0
      proof
        defpred P[Nat] means (s2*F).$1<>x0;
A42:    for k being Nat st P[k] holds P[k+1]
        proof
          let k be Nat such that
          (s2*F).k<>x0;
          P[k,F.k,F.(k+1)] by A22;
          then s2.(F.(k+1))<>x0;
          hence thesis by FUNCT_2:15;
        end;
A43:    P[0] by A16,A22,FUNCT_2:15;
        thus for n being Nat holds P[n] from NAT_1:sch 2(A43,A42);
      end;
A44:  rng (s2*F) c= rng s2 by VALUED_0:21;
      then rng (s2*F) c= dom f by A3;
      then
A45:  f/*(s2*F) is convergent & f/.x0=lim(f/*(s2*F)) by A2,A41,A28;
A46:  now
        let p be Real;
        assume
A47:    0<p;
        then consider n being Nat such that
A48:    for m be Nat st n<=m holds ||.(f/*(s2*F)).m-f/.x0
        .||<p by A45,NORMSP_1:def 7;
         reconsider k=F.n as Nat;
        take k;
        let m be Nat such that
A49:    k<=m;
A50:   m in NAT by ORDINAL1:def 12;
        now
          per cases;
          suppose
A51:        s2.m=x0;
            ||.(f/*s2).m-f/.x0.|| =||.f/.(s2.m)-f/.x0.|| by A3,FUNCT_2:109,A50
              .=||.0.T.|| by A51,RLVECT_1:15
              .=0 by NORMSP_1:1;
            hence ||.(f/*s2).m-f/.x0.||<p by A47;
          end;
          suppose
            s2.m<>x0;
            then consider l be Element of NAT such that
A52:        m=F.l by A29,A50;
            n<=l by A49,A52,SEQM_3:1;
            then ||.(f/*(s2*F)).l-f/.x0.||<p by A48;
            then ||.f/.((s2*F).l)-f/.x0.||<p by A3,A44,FUNCT_2:109,XBOOLE_1:1;
            then ||.f/.(s2.m)-f/.x0.||<p by A52,FUNCT_2:15;
            hence ||.(f/*s2).m-f/.x0.||<p by A3,FUNCT_2:109,A50;
          end;
        end;
        hence ||.(f/*s2).m-f/.x0.||<p;
      end;
      hence f/*s2 is convergent;
      hence f/.x0=lim(f/*s2) by A46,NORMSP_1:def 7;
    end;
  end;
  hence thesis;
end;

theorem Th28:
  for R1,R2 holds R1+R2 is RestFunc of S,T & R1-R2 is RestFunc of S,T
proof
  let R1,R2;
A1: R1 is total & R2 is total by Def5;
A2: now
    let h ;
    assume A3: h is non-zero;
A4: (||.h.||")(#)(R1/*h) is convergent & (||.h.||")(#)(R2/*h) is
    convergent by Def5,A3;
A5: (||.h.||")(#)((R1+R2)/*h) = (||.h.||")(#)((R1/*h)+(R2/*h)) by A1,Th25
      .= ((||.h.||")(#)(R1/*h))+((||.h.||")(#)(R2/*h)) by Th9;
    hence (||.h.||")(#)((R1+R2)/*h) is convergent by A4,NORMSP_1:19;
    lim ((||.h.||")(#)(R1/*h)) = 0.T & lim ((||.h.||")(#)(R2/*h)) = 0.T
    by A3,Def5;
    hence lim ((||.h.||")(#)((R1+R2)/*h)) = 0.T+0.T by A4,A5,NORMSP_1:25
      .= 0.T by RLVECT_1:4;
  end;
A6: now
    let h;
    assume A7: h is non-zero;
A8: (||.h.||")(#)(R1/*h) is convergent & (||.h.||")(#)(R2/*h) is
    convergent by Def5,A7;
A9: (||.h.||")(#)((R1-R2)/*h) = (||.h.||")(#)((R1/*h)-(R2/*h)) by A1,Th25
      .= ((||.h.||")(#)(R1/*h))-((||.h.||")(#)(R2/*h)) by Th12;
    hence (||.h.||")(#)((R1-R2)/*h) is convergent by A8,NORMSP_1:20;
    lim ((||.h.||")(#)(R1/*h)) = 0.T & lim ((||.h.||")(#)(R2/*h)) = 0.T
    by Def5,A7;
    hence lim ((||.h.||")(#)((R1-R2)/*h)) = 0.T-0.T by A8,A9,NORMSP_1:26
      .= 0.T by RLVECT_1:13;
  end;
  R1+R2 is total by A1,VFUNCT_1:32;
  hence R1+R2 is RestFunc of S,T by A2,Def5;
  R1-R2 is total by A1,VFUNCT_1:32;
  hence thesis by A6,Def5;
end;

theorem Th29:
  for r,R holds r(#)R is RestFunc of S,T
proof
  let r,R;
A1: R is total by Def5;
A2: now
    let h;
    assume A3: h is non-zero;
A4: (||.h.||")(#)(R/*h) is convergent by A3,Def5;
A5: (||.h.||")(#)((r(#)R)/*h) = (||.h.||")(#)(r*(R/*h)) by A1,Th26
      .= r*((||.h.||")(#)(R/*h)) by Th10;
    hence (||.h.||")(#)((r(#)R)/*h) is convergent by A4,NORMSP_1:22;
    lim ((||.h.||")(#)(R/*h)) = 0.T by A3,Def5;
    hence lim ((||.h.||")(#)((r(#)R)/*h)) = r*0.T by A4,A5,NORMSP_1:28
      .= 0.T by RLVECT_1:10;
  end;
  r(#)R is total by A1,VFUNCT_1:34;
  hence thesis by A2,Def5;
end;

definition
  let S,T;
  let f be PartFunc of S,T;
  let x0 be Point of S;
  pred f is_differentiable_in x0 means

  ex N being Neighbourhood of x0
st N c= dom f & ex L,R st for x be Point of S st x in N holds f/.x - f/.x0 = L.
  (x-x0) + R/.(x-x0);
end;

definition
  let S,T;
  let f be PartFunc of S,T;
  let x0 be Point of S;
  assume
A1: f is_differentiable_in x0;
  func diff(f,x0) -> Point of R_NormSpace_of_BoundedLinearOperators(S,T) means
  :Def7:
  ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be Point of
  S st x in N holds f/.x-f/.x0 = it.(x-x0) + R/.(x-x0);
  existence
  by A1;
  uniqueness
  proof
    let LB,LB1 be Point of R_NormSpace_of_BoundedLinearOperators(S,T);
A2: R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
      BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
      R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
    then reconsider L = LB as Element of BoundedLinearOperators(S,T);
    reconsider L1=LB1 as Element of BoundedLinearOperators(S,T) by A2;
    assume that
A3: ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be
    Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0)+R/.(x-x0) and
A4: ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be
    Point of S st x in N holds f/.x-f/.x0 = LB1.(x-x0) + R/.(x-x0);
    consider N being Neighbourhood of x0 such that
    N c= dom f and
A5: ex R st for x be Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0)
    +R /.(x-x0) by A3;
    consider R such that
A6: for x be Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0) + R/.(x
    -x0) by A5;
    consider N1 being Neighbourhood of x0 such that
    N1 c= dom f and
A7: ex R st for x be Point of S st x in N1 holds f/.x-f/.x0=LB1.(x-x0
    )+ R/.(x-x0) by A4;
    consider R1 such that
A8: for x be Point of S st x in N1 holds f/.x-f/.x0 = LB1.(x-x0) + R1
    /.(x-x0) by A7;
A9: for z be Point of S holds modetrans(L,S,T).z = modetrans(L1,S,T).z
    proof
      let z be Point of S;
      now
        per cases;
        case
A10:      z= 0.S;
          hence modetrans(L,S,T).z =modetrans(L,S,T).(0*z) by RLVECT_1:10
            .=0*modetrans(L,S,T).z by LOPBAN_1:def 5
            .=0.T by RLVECT_1:10
            .=0*modetrans(L1,S,T).z by RLVECT_1:10
            .=modetrans(L1,S,T).(0*z) by LOPBAN_1:def 5
            .=modetrans(L1,S,T).z by A10,RLVECT_1:10;
        end;
        case
A11:      z<> 0.S;
          consider N0 be Neighbourhood of x0 such that
A12:      N0 c= N & N0 c= N1 by Th1;
          consider g be Real such that
A13:      0<g and
A14:      {y where y is Point of S: ||.y - x0 .|| < g} c= N0 by NFCONT_1:def 1;
          consider n0 be Nat such that
A15:      ||.z.|| /g < n0 by SEQ_4:3;
          set n1=n0+1;
          n0 <= n0+1 by NAT_1:11;
          then ||.z.|| /g < (n0+1) by A15,XXREAL_0:2;
          then ( ||.z.|| /g)*g < (n0+1)*g by A13,XREAL_1:68;
          then ||.z.|| < (n0+1)*g by A13,XCMPLX_1:87;
          then
A16:      ||.z.|| /(n0+1) < g by XREAL_1:83;
          ex r be Real_Sequence st (for n be Element of NAT holds (r.n=1
          /(n+n1) & r.n > 0 & r.n*z+x0 in N0) ) & r is convergent & lim r =0
          proof
            deffunc F(Nat) = 1 /($1+n1);
            consider r be Real_Sequence such that
A17:        for n being Nat holds r.n = F(n) from SEQ_1:sch 1;
            take r;
            thus for n be Element of NAT holds r.n=1 /(n+n1) & r.n > 0 & r.n*z
            +x0 in N0
            proof
              let n be Element of NAT;
              thus r.n=1 /(n+n1) by A17;
              n1 <= n+n1 & 0 <= ||.z.|| by NAT_1:12,NORMSP_1:4;
              then
A18:          ||.z.|| /(n+n1) <= ||.z.|| /n1 by XREAL_1:118;
              0 < 1 * (n + n1)";
              then
          0 < 1/(n + n1) by XCMPLX_0:def 9;
              hence r.n >0 by A17;
              ||.r.n*z+x0-x0.|| = ||.r.n*z+(x0-x0).|| by RLVECT_1:def 3
                .= ||.r.n*z+0.S.|| by RLVECT_1:15
                .= ||.r.n*z.|| by RLVECT_1:4
                .= ||.(1 /(n+n1))*z.|| by A17
                .= |.1 /(n+n1).|* ||.z.|| by NORMSP_1:def 1
                .= ( 1 /(n+n1) )* ||.z.|| by ABSVALUE:def 1
                .= ||.z.|| /(n+n1) by XCMPLX_1:99;
              then ||.r.n*z+x0-x0.|| < g by A16,A18,XXREAL_0:2;
              then (r.n*z+x0) in {y where y is Point of S: ||.y - x0 .|| < g};
              hence thesis by A14;
            end;
            thus thesis by A17,SEQ_4:31;
          end;
          then consider r be Real_Sequence such that
A19:      for n be Element of NAT holds r.n=1 /(n+n1) & r.n > 0 & r.n
          *z+x0 in N0 and
          r is convergent and
          lim r =0;
          deffunc F(Element of NAT) = r.$1*z;
          consider s be sequence of S such that
A20:      for n holds s.n = F(n) from FUNCT_2:sch 4;
          now
            let n be Nat;
A21:           n in NAT by ORDINAL1:def 12;
            assume s.n = 0.S;
            then r.n*z = 0.S by A20,A21;
            then r.n =0 or z=0.S by RLVECT_1:11;
            hence contradiction by A11,A19,A21;
          end;
          then
A22:      s is non-zero by Th7;
          now
            let n be Nat;
A23:           n in NAT by ORDINAL1:def 12;
            hence s.n = r.n*z by A20
              .=(1 /(n+n1))*z by A19,A23;
          end;
          then s is convergent & lim s = 0.S by Th19,Th20;
          then reconsider s as (0.S)-convergent sequence of S
            by Def4;
A24:      now
            let x be Point of S;
            assume that
A25:        x in N and
A26:        x in N1;
            f/.x-f/.x0 = L.(x-x0) + R/.(x-x0) by A6,A25;
            hence L.(x-x0) + R/.(x-x0) = L1.(x-x0) + R1/.(x-x0) by A8,A26;
          end;
          now
            R1 is total by Def5;
            then dom R1 = the carrier of S by PARTFUN1:def 2;
            then
A27:        rng s c= dom R1;
            R is total by Def5;
            then dom R = the carrier of S by PARTFUN1:def 2;
            then
A28:        rng s c= dom R;
            let n be Nat;
            set x=(r.n)*z+x0;
A29:        x-x0 = (r.n)*z+(x0 -x0) by RLVECT_1:def 3
              .= (r.n)*z+0.S by RLVECT_1:15
              .=(r.n)*z by RLVECT_1:4;
A30:        n in NAT by ORDINAL1:def 12;
            then
A31:        r.n <> 0 by A19;
            s.n <> 0.S by A22,Th7;
            then
A32:        ||.s.n.|| <> 0 by NORMSP_0:def 5;
A33:        r.n > 0 by A19,A30;
            ||.s.n.|| = ||.(r.n)*z.|| by A20,A30
              .= |.r.n.| * ||.z.|| by NORMSP_1:def 1
              .=r.n * ||.z.|| by A33,ABSVALUE:def 1;
            then (r.n)"* ||.s.n.|| = (r.n)"* r.n * ||.z.||
              .= ((r.n)/(r.n))* ||.z.|| by XCMPLX_0:def 9
              .= 1* ||.z.|| by A31,XCMPLX_1:60
              .= ||.z.||;
            then
            ||.z.|| *( ||.s.n.|| )" = (r.n)"* (||.s.n.|| *( ||.s.n.|| )")
              .= (r.n)"* (||.s.n.|| /( ||.s.n.|| )) by XCMPLX_0:def 9
              .= (r.n)"*1 by A32,XCMPLX_1:60
              .= (r.n)";
            then
A34:        ||.z.|| *( ||.s.||.n )" = (r.n)" by NORMSP_0:def 4;
            x in N0 by A19,A30;
            then
            L.((r.n)*z) + R/.((r.n)*z) = L1.((r.n)*z) + R1/.(( r.n)*z) by A24
,A12,A29;
            then
A35:        (r.n)"*(L.((r.n)*z))+(r.n)"*(R/.((r.n)*z)) =(r.n)"*(L1.((r.n)
            *z)+R1/.((r.n)*z)) by RLVECT_1:def 5;
A36:        (r.n)"*(L1.((r.n)*z)) =(r.n)"*(modetrans(L1,S,T).((r.n)*z))
            by LOPBAN_1:def 11
              .=(r.n)"*((r.n)*modetrans(L1,S,T).z) by LOPBAN_1:def 5
              .= (r.n)"*((r.n)*L1.z ) by LOPBAN_1:def 11
              .= ((r.n)"*(r.n))*L1.z by RLVECT_1:def 7
              .= ((r.n)/(r.n))*L1.z by XCMPLX_0:def 9
              .= 1*L1.z by A31,XCMPLX_1:60
              .= L1.z by RLVECT_1:def 8;
            (r.n)"*(L.((r.n)*z)) =(r.n)"*(modetrans(L,S,T).((r.n)*z)) by
LOPBAN_1:def 11
              .=(r.n)"*((r.n)*modetrans(L,S,T).z) by LOPBAN_1:def 5
              .= (r.n)"*((r.n)*L.z ) by LOPBAN_1:def 11
              .= ((r.n)"*(r.n))*L.z by RLVECT_1:def 7
              .= ((r.n)/(r.n))*L.z by XCMPLX_0:def 9
              .= 1*L.z by A31,XCMPLX_1:60
              .= L.z by RLVECT_1:def 8;
            then
A37:        L.z + (r.n)" *(R/.((r.n)*z)) = L1.z + (r.n)"*(R1/. ((r.n)*z))
            by A35,A36,RLVECT_1:def 5;
A38:        (r.n)"*(R1/.((r.n)*z)) = (r.n)"*(R1/.(s.n)) by A20,A30
              .= ( ||.z.|| *||.s.||".n)*(R1/.(s.n)) by A34,VALUED_1:10
              .= ||.z.|| *(||.s.||".n *(R1/.(s.n)) ) by RLVECT_1:def 7
              .= ||.z.|| *((||.s.||".n)*((R1/*s).n)) by A30,A27,FUNCT_2:109
              .= ||.z.|| *((||.s.||")(#)(R1/*s)).n by Def2;
            (r.n)"*(R/.((r.n)*z)) = (r.n)"*(R/.(s.n)) by A20,A30
              .= ( ||.z.|| *||.s.||".n)*(R/.(s.n)) by A34,VALUED_1:10
              .= ||.z.|| *(||.s.||".n *(R/.(s.n)) ) by RLVECT_1:def 7
              .= ||.z.|| *((||.s.||".n)*((R/*s).n)) by A30,A28,FUNCT_2:109
              .= ||.z.|| *((||.s.||")(#)(R/*s)).n by Def2;
            then L.z + ( ||.z.|| *((||.s.||")(#)(R/*s)).n -( ||.z.|| *((||.s
.||")(#)(R/*s)).n)) = L1.z + ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z.|| *((||.
            s.||")(#)(R/*s)).n) by A37,A38,RLVECT_1:def 3;
            then L.z + 0.T = L1.z + ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z
            .|| *((||.s.||")(#)(R/*s)).n) by RLVECT_1:15;
            then L.z = L1.z + ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z.|| *((
            ||.s.||")(#)(R/*s)).n) by RLVECT_1:def 4;
            then
            L.z - L1.z = (- L1.z)+ (L1.z + ( ||.z.|| *((||.s.||")(#)(R1/*
            s)).n -(||.z.|| *((||.s.||")(#)(R/*s)).n) )) by RLVECT_1:def 3;
            then
            L.z - L1.z = (- L1.z)+ L1.z + (||.z.|| *((||.s.||")(#)(R1/*s)
            ).n -(||.z.|| *((||.s.||")(#)(R/*s)).n) ) by RLVECT_1:def 3;
            then L.z - L1.z = 0.T+ ( ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z
            .|| *((||.s.||")(#)(R/*s)).n) ) by RLVECT_1:5;
            then
            L.z - L1.z = (||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z.|| *((
            ||.s.||")(#)(R/*s)).n) ) by RLVECT_1:4;
            then L.z - L1.z = ||.z.|| *((||.s.||"(#)(R1/*s)).n-(||.s.||"(#)(R
            /*s)).n) by RLVECT_1:34;
            then
            L.z - L1.z = ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s
            ))).n by NORMSP_1:def 3;
            hence L.z - L1.z = ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R
            /*s)))).n by NORMSP_1:def 5;
          end;
          then
          ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s))) is constant
& ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s)))).1 =L.z - L1.z by
VALUED_0:def 18;
          then
A39:      lim ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s)) )) = L
          .z - L1.z by Th18;
A40:      (||.s.||")(#)(R/*s) is convergent & (||.s.||")(#)(R1/*s) is
          convergent by A22,Def5;
          lim ((||.s.||")(#)(R/*s)) = 0.T & lim ((||.s.||")(#)(R1/*s)) =
          0.T by A22,Def5;
          then
A41:      lim ((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s))) = 0.T - 0.T by A40,
NORMSP_1:26
            .= 0.T by RLVECT_1:13;
A42:      lim ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s)))) =
||.z.|| * lim ((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s))) by A40,NORMSP_1:20,28
            .=0.T by A41,RLVECT_1:10;
          thus modetrans(L,S,T).z =L.z by LOPBAN_1:def 11
            .=L1.z by A39,A42,RLVECT_1:21
            .= modetrans(L1,S,T).z by LOPBAN_1:def 11;
        end;
      end;
      hence thesis;
    end;
    thus LB=modetrans(L,S,T) by LOPBAN_1:def 11
      .=modetrans(L1,S,T) by A9,FUNCT_2:63
      .=LB1 by LOPBAN_1:def 11;
  end;
end;

definition
  let X;
  let S,T;
  let f be PartFunc of S,T;
  pred f is_differentiable_on X means

  X c=dom f & for x be Point of S st x in X holds f|X is_differentiable_in x;
end;

theorem Th30:
  for f be PartFunc of S,T holds (f is_differentiable_on X implies
  X is Subset of S)
by XBOOLE_1:1;

theorem Th31:
  for f be PartFunc of S,T for Z be Subset of S st Z is open holds
( f is_differentiable_on Z iff Z c=dom f & for x be Point of S st x in Z holds
  f is_differentiable_in x )
proof
  let f be PartFunc of S,T;
  let Z be Subset of S such that
A1: Z is open;
  thus f is_differentiable_on Z implies Z c=dom f & for x be Point of S st x
  in Z holds f is_differentiable_in x
  proof
    assume
A2: f is_differentiable_on Z;
    hence
A3: Z c=dom f;
    let x0 be Point of S;
    assume
A4: x0 in Z;
    then f|Z is_differentiable_in x0 by A2;
    then consider N being Neighbourhood of x0 such that
A5: N c= dom(f|Z) and
A6: ex L,R st for x be Point of S st x in N holds (f|Z)/.x-(f|Z)/.x0=L
    .( x-x0)+R/.(x-x0);
    consider L,R such that
A7: for x be Point of S st x in N holds (f|Z)/.x - (f|Z)/.x0 = L.(x-
    x0) + R/.(x-x0) by A6;
    take N;
A8: dom(f|Z)=dom f/\Z by RELAT_1:61;
    then dom(f|Z) c=dom f by XBOOLE_1:17;
    hence N c= dom f by A5;
    take L,R;
    let x be Point of S;
    assume
A9: x in N;
    then (f|Z)/.x-(f|Z)/.x0=L.(x-x0)+R/.(x-x0) by A7;
    then f/.x-(f|Z)/.x0=L.(x-x0)+R/.(x-x0) by A5,A8,A9,PARTFUN2:16;
    hence thesis by A3,A4,PARTFUN2:17;
  end;
  assume that
A10: Z c=dom f and
A11: for x be Point of S st x in Z holds f is_differentiable_in x;
  thus Z c=dom f by A10;
  let x0 be Point of S;
  assume
A12: x0 in Z;
  then consider N1 being Neighbourhood of x0 such that
A13: N1 c= Z by A1,Th2;
  f is_differentiable_in x0 by A11,A12;
  then consider N being Neighbourhood of x0 such that
A14: N c= dom f and
A15: ex L,R st for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R
  /.(x-x0);
  consider N2 being Neighbourhood of x0 such that
A16: N2 c= N1 and
A17: N2 c= N by Th1;
A18: N2 c= Z by A13,A16;
  take N2;
  N2 c= dom f by A14,A17;
  then
A19: N2 c= dom f/\Z by A18,XBOOLE_1:19;
  hence N2 c= dom(f|Z) by RELAT_1:61;
A20: x0 in N2 by NFCONT_1:4;
  consider L,R such that
A21: for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A15;
  take L,R;
  let x be Point of S;
  assume
A22: x in N2;
  then f/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A17,A21;
  then (f|Z)/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A19,A22,PARTFUN2:16;
  hence thesis by A19,A20,PARTFUN2:16;
end;

theorem
  for f be PartFunc of S,T for Y be Subset of S holds f
  is_differentiable_on Y implies Y is open
proof
  let f be PartFunc of S,T;
  let Y be Subset of S;
  assume
A1: f is_differentiable_on Y;
  now
    let x0 be Point of S;
    assume x0 in Y;
    then f|Y is_differentiable_in x0 by A1;
    then consider N being Neighbourhood of x0 such that
A2: N c= dom(f|Y) and
    ex L,R st for x be Point of S st x in N holds (f|Y)/.x-(f|Y)/.x0=L.( x
    -x0)+R/.(x-x0);
    take N;
    dom(f|Y)=dom f/\Y by RELAT_1:61;
    then dom(f|Y) c=Y by XBOOLE_1:17;
    hence N c= Y by A2;
  end;
  hence thesis by Th4;
end;

definition
  let S,T;
  let f be PartFunc of S,T;
  let X be set;
  assume
A1: f is_differentiable_on X;
  func f`|X -> PartFunc of S, R_NormSpace_of_BoundedLinearOperators(S,T) means
  :Def9:
  dom it = X & for x be Point of S st x in X holds it/.x = diff(f,x);
  existence
  proof
    deffunc F(Point of S) = diff(f,$1);
    defpred P[Point of S] means $1 in X;
    consider F being PartFunc of S,R_NormSpace_of_BoundedLinearOperators(S,T)
    such that
A2: (for x be Point of S holds x in dom F iff P[x]) & for x be Point
    of S st x in dom F holds F.x = F(x) from SEQ_1:sch 3;
    take F;
    now
A3:   X is Subset of S by A1,Th30;
      let y be object;
      assume y in X;
      hence y in dom F by A2,A3;
    end;
    then
A4: X c= dom F;
    for y being object st y in dom F holds y in X by A2;
    then dom F c= X;
    hence dom F = X by A4;
    now
      let x be Point of S;
      assume x in X;
      then
A5:   x in dom F by A2;
      then F.x = diff(f,x) by A2;
      hence F/.x = diff(f,x) by A5,PARTFUN1:def 6;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let F,G be PartFunc of S,R_NormSpace_of_BoundedLinearOperators(S,T);
    assume that
A6: dom F = X and
A7: for x be Point of S st x in X holds F/.x = diff(f,x) and
A8: dom G = X and
A9: for x be Point of S st x in X holds G/.x = diff(f,x);
    now
      let x be Point of S;
      assume
A10:  x in dom F;
      then F/.x = diff(f,x) by A6,A7;
      hence F/.x=G/.x by A6,A9,A10;
    end;
    hence thesis by A6,A8,PARTFUN2:1;
  end;
end;

theorem
  for f be PartFunc of S,T for Z be Subset of S st Z is open & Z c= dom
f & ex r be Point of T st rng f = {r} holds f is_differentiable_on Z & for x be
Point of S st x in Z holds (f`|Z)/.x = 0.R_NormSpace_of_BoundedLinearOperators(
  S,T)
proof
  let f be PartFunc of S,T;
  let Z be Subset of S such that
A1: Z is open and
A2: Z c= dom f;
  reconsider R = (the carrier of S) --> 0.T as PartFunc of S,T;
  set L = 0.R_NormSpace_of_BoundedLinearOperators(S,T);
  given r be Point of T such that
A3: rng f = {r};
  R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
    BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
    R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
    R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
  then reconsider L as Element of BoundedLinearOperators(S,T);
A4: dom R = the carrier of S;
A5: now
    let h;
    assume  h is non-zero;
A6: now
      let n be Nat;
A7:   R/.(h.n) =R.(h.n) by A4,PARTFUN1:def 6
        .=0.T;
A8:   rng h c= dom R;
A9:   n in NAT by ORDINAL1:def 12;
      thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
        .= (||.h.||".n)*(R/.(h.n)) by A9,A8,FUNCT_2:109
        .= 0.T by A7,RLVECT_1:10;
    end;
    then
A10: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
    hence (||.h.||")(#)(R/*h) is convergent by Th18;
    ((||.h.||")(#)(R/*h)).0 = 0.T by A6;
    hence lim ((||.h.||")(#)(R/*h)) = 0.T by A10,Th18;
  end;
A11: now
    let x0 be Point of S;
    assume
A12: x0 in dom f;
    then f.x0 in {r} by A3,FUNCT_1:def 3;
    then f/.x0 in {r} by A12,PARTFUN1:def 6;
    hence f/.x0 = r by TARSKI:def 1;
  end;
  reconsider R as RestFunc of S,T by A5,Def5;
A13: ((the carrier of S) --> 0.T) = L by LOPBAN_1:31;
A14: now
    let x0 be Point of S;
    assume
A15: x0 in Z;
    then consider N being Neighbourhood of x0 such that
A16: N c= Z by A1,Th2;
A17: N c= dom f by A2,A16;
    for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x- x0)
    proof
      let x be Point of S;
A18:  R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
        .=0.T;
      assume x in N;
      hence f/.x - f/.x0 = r - f/.x0 by A11,A17
        .= r - r by A2,A11,A15
        .=0.T by RLVECT_1:15
        .= 0.T + 0.T by RLVECT_1:4
        .= L.(x-x0)+R/.(x-x0) by A13,A18;
    end;
    hence f is_differentiable_in x0 by A17;
  end;
  hence
A19: f is_differentiable_on Z by A1,A2,Th31;
  let x0 be Point of S;
  assume
A20: x0 in Z;
  then
A21: f is_differentiable_in x0 by A14;
  then
  ex N being Neighbourhood of x0 st N c= dom f & ex L,R st for x be Point
  of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0);
  then consider N being Neighbourhood of x0 such that
A22: N c= dom f;
A23: for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0)
  proof
    let x be Point of S;
A24: R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
      .=0.T;
    assume x in N;
    hence f/.x - f/.x0 = r - f/.x0 by A11,A22
      .=r - r by A2,A11,A20
      .=0.T by RLVECT_1:15
      .= 0.T + 0.T by RLVECT_1:4
      .=L.(x-x0) + R/.(x-x0) by A13,A24;
  end;
  thus (f`|Z)/.x0 = diff(f,x0) by A19,A20,Def9
    .= 0.R_NormSpace_of_BoundedLinearOperators(S,T) by A21,A22,A23,Def7;
end;

registration
  let S;
  let h,n;
  cluster h^\n -> (0.S)-convergent for sequence of S;
  coherence
  proof
A1: h is convergent by Def4;
    lim h = 0.S by Def4;
    then
A2: lim (h^\n) = 0.S by A1,LOPBAN_3:9;
    h^\n is convergent by A1,LOPBAN_3:9;
    hence thesis by A2;
  end;
end;

registration
  let S be non trivial RealNormSpace;
  let h be (0.S)-convergent non-zero sequence of S ;
  let n;
  cluster h^\n -> (0.S)-convergent non-zero for sequence of S;
  coherence by Th17;
end;


theorem Th34:
  for x0 be Point of S for N being Neighbourhood of x0 st f
is_differentiable_in x0 & N c= dom f holds
for h be (0.S)-convergent sequence of S st h is non-zero
 holds
   for c st rng c = {x0} & rng (h+c) c= N holds (f/*(h+c) - f/*c) is convergent
  & lim (f/*(h+c) - f/*c) = 0.T
proof
  let x0 be Point of S;
  let N be Neighbourhood of x0;
  assume that
A1: f is_differentiable_in x0 and
A2: N c= dom f;
  let h be (0.S)-convergent sequence of S;
  assume A3: h is non-zero;
  let c such that
A4: rng c = {x0} and
A5: rng (h+c) c= N;
  consider N1 be Neighbourhood of x0 such that
  N1 c= dom f and
A6: ex L,R st for x be Point of S st x in N1 holds f/.x - f/.x0 = L.(x-
  x0) + R/.(x-x0) by A1;
  consider N2 be Neighbourhood of x0 such that
A7: N2 c= N and
A8: N2 c= N1 by Th1;
  consider L,R such that
A9: for x be Point of S st x in N1 holds f/.x - f/.x0 = L.(x-x0) + R/.(x
  -x0) by A6;
  consider g be Real such that
A10: 0<g and
A11: {y where y is Point of S: ||.y-x0.|| < g} c= N2 by NFCONT_1:def 1;
A12: x0 in N2 by NFCONT_1:4;
  ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
  proof
    c.0 in rng c by NFCONT_1:6;
    then c.0=x0 by A4,TARSKI:def 1;
    then
A13: lim c = x0 by Th18;
A14: c is convergent & h is convergent by Def4,Th18;
    then
A15: h + c is convergent by NORMSP_1:19;
    lim h = 0.S by Def4;
    then lim (h + c) = 0.S + x0 by A13,A14,NORMSP_1:25
      .= x0 by RLVECT_1:4;
    then consider n being Nat such that
A16: for m being Nat st n<=m holds ||.(h+c).m-x0.||<g by A10,A15,
NORMSP_1:def 7;
     reconsider n as Element of NAT by ORDINAL1:def 12;
    take n;
A17: rng (c^\n) = {x0} by A4,VALUED_0:26;
    thus rng (c^\n) c= N2
    by A12,A17,TARSKI:def 1;
    let y be object;
    assume y in rng ((h+c)^\n);
    then consider m be Nat such that
A18: y = ((h+c)^\n).m by NFCONT_1:6;
    reconsider y1=y as Point of S by A18;
    n + 0 <= n+m by XREAL_1:7;
    then ||.(h+c).(n+m)-x0.||<g by A16;
    then ||.((h+c)^\n).m - x0 .|| < g by NAT_1:def 3;
    then y1 in {z where z is Point of S: ||.z-x0.|| < g} by A18;
    hence thesis by A11;
  end;
  then consider n such that
  rng (c^\n) c= N2 and
A19: rng ((h+c)^\n) c= N2;
A20: lim (h^\n) = 0.S by Def4;
A21: for k holds f/.(((h+c)^\n).k) - f/.((c^\n).k) = L.((h^\n).k) + R/.((h^\
  n).k)
  proof
    let k;
    ((h+c)^\n).k in rng ((h+c)^\n) by NFCONT_1:6;
    then
A22: ((h+c)^\n).k in N2 by A19;
    (c^\n).k in rng (c^\n) & rng (c^\n) = rng c by NFCONT_1:6,VALUED_0:26;
    then
A23: (c^\n).k = x0 by A4,TARSKI:def 1;
    ((h+c)^\n).k - (c^\n).k = (h+c).(k+n) - (c^\n).k by NAT_1:def 3
      .=h.(k+n)+ c.(k+n) - (c^\n).k by NORMSP_1:def 2
      .=(h^\n).k+ c.(k+n) - (c^\n).k by NAT_1:def 3
      .=(h^\n).k+ (c^\n).k- (c^\n).k by NAT_1:def 3
      .= (h^\n).k + ((c^\n).k - (c^\n).k) by RLVECT_1:def 3
      .= (h^\n).k + 0.S by RLVECT_1:15
      .= (h^\n).k by RLVECT_1:4;
    hence thesis by A9,A8,A22,A23;
  end;
  R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
    BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
    R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
    R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
  then reconsider L as Element of BoundedLinearOperators(S,T);
  reconsider LP=modetrans(L,S,T) as PartFunc of S,T;
A24: h^\n is non-zero by A3,Th17;
then
A25: lim (R/*(h^\n)) = 0.T by Th24;
A26: rng ((h+c)^\n) c= dom f
  by A19,A7,A2;
  R is total by Def5;
  then dom R = the carrier of S by PARTFUN1:def 2;
  then
A27: rng (h^\n) c= dom R;
A28: rng (c^\n) c= dom f
  proof
    let y be object;
    assume
A29: y in rng (c^\n);
    rng (c^\n) = rng c by VALUED_0:26;
    then y = x0 by A4,A29,TARSKI:def 1;
    then y in N by NFCONT_1:4;
    hence thesis by A2;
  end;
A30: dom modetrans(L,S,T) = the carrier of S by FUNCT_2:def 1;
  then
A31: rng (h^\n) c= dom modetrans(L,S,T);
  now
    let k;
    thus (f/*((h+c)^\n)-f/*(c^\n)).k = (f/*((h+c)^\n)).k-(f/*(c^\n)).k by
NORMSP_1:def 3
      .= f/.(((h+c)^\n).k) - (f/*(c^\n)).k by A26,FUNCT_2:109
      .= f/.(((h+c)^\n).k) - f/.((c^\n).k) by A28,FUNCT_2:109
      .= L.((h^\n).k) + R/.((h^\n).k) by A21
      .= modetrans(L,S,T).((h^\n).k) + R/.((h^\n).k) by LOPBAN_1:def 11
      .= LP/.((h^\n).k) + R/.((h^\n).k) by A30,PARTFUN1:def 6
      .= (LP/*(h^\n)).k + R/.((h^\n).k) by A31,FUNCT_2:109
      .= (LP/*(h^\n)).k + (R/*(h^\n)).k by A27,FUNCT_2:109
      .= (LP/*(h^\n) + R/*(h^\n)).k by NORMSP_1:def 2;
  end;
  then
A32: f/*((h+c)^\n) - f/*(c^\n) = LP/*(h^\n) + R/*(h^\n) by FUNCT_2:63;
A33: dom modetrans(L,S,T) = the carrier of S by FUNCT_2:def 1;
  LP is_Lipschitzian_on the carrier of S
  proof
    thus the carrier of S c=dom LP by FUNCT_2:def 1;
    set LL=modetrans(L,S,T);
    consider K being Real such that
A34: 0 <= K and
A35: for x being VECTOR of S holds ||. LL.x .|| <= K * ||. x .|| by
LOPBAN_1:def 8;
    take K+1;
A36: 0 + K < 1 + K by XREAL_1:8;
    now
      let x1,x2 be Point of S such that
      x1 in the carrier of S and
      x2 in the carrier of S;
A37:  ||.LL.(x1-x2) .|| <= K * ||.x1-x2.|| by A35;
      0 <= ||.x1-x2.|| by NORMSP_1:4;
      then
A38:  K * ||.x1-x2.|| <= (K+1 ) * ||.x1-x2.|| by A36,XREAL_1:64;
      ||.LP/.x1-LP/.x2 .|| = ||.LL.x1-LP/.x2 .|| by A33,PARTFUN1:def 6
        .= ||.LL.x1+-LL.x2 .|| by A33,PARTFUN1:def 6
        .= ||.LL.x1+(-1)*LL.x2 .|| by RLVECT_1:16
        .= ||.LL.x1+LL.((-1)*x2) .|| by LOPBAN_1:def 5
        .= ||.LL.(x1+(-1)*x2) .|| by VECTSP_1:def 20
        .= ||.LL.(x1-x2) .|| by RLVECT_1:16;
      hence ||.LP/.x1-LP/.x2 .|| <= (K+1) * ||.x1-x2.|| by A37,A38,XXREAL_0:2;
    end;
    hence thesis by A34;
  end;
  then
A39: LP is_continuous_on the carrier of S by NFCONT_1:45;
A40: rng c c= dom f
  proof
    let y be object;
    assume y in rng c;
    then y = x0 by A4,TARSKI:def 1;
    then y in N by NFCONT_1:4;
    hence thesis by A2;
  end;
A41: h^\n is convergent & rng (h^\n) c= the carrier of S by Def4;
  then
A42: LP/*(h^\n) is convergent by A39,A20,NFCONT_1:18;
A43: R/*(h^\n) is convergent by A24,Th24;
  then
A44: (LP/*(h^\n) + R/*(h^\n)) is convergent by A42,NORMSP_1:19;
  LP/.(0.S) =modetrans(L,S,T).(0.S) by A33,PARTFUN1:def 6
    .= modetrans(L,S,T).(0*0.S) by RLVECT_1:10
    .=0*modetrans(L,S,T).0.S by LOPBAN_1:def 5
    .=0.T by RLVECT_1:10;
  then lim (LP/*(h^\n)) = 0.T by A39,A41,A20,NFCONT_1:18;
  then lim (LP/*(h^\n) + R/*(h^\n)) = 0.T+0.T by A43,A25,A42,NORMSP_1:25;
  then
A45: lim (LP/*(h^\n) + R/*(h^\n)) = 0.T by RLVECT_1:4;
  rng (h+c) c= dom f
  by A5,A2;
  then f/*((h+c)^\n) - f/*(c^\n) =(f/*(h+c))^\n - f/*(c^\n) by VALUED_0:27
    .=(f/*(h+c))^\n - (f/*c) ^\n by A40,VALUED_0:27
    .= (f/*(h+c) - f/*c) ^\n by Th16;
  hence thesis by A32,A44,A45,LOPBAN_3:10,11;
end;

theorem Th35:
  for f1,f2,x0 st f1 is_differentiable_in x0 & f2
  is_differentiable_in x0 holds f1+f2 is_differentiable_in x0 & diff(f1+f2,x0)=
  diff(f1,x0)+diff(f2,x0)
proof
  let f1,f2,x0;
  assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
  consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L.(x
  -x0) + R/.(x-x0) by A1;
  consider L1,R1 such that
A5: for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L1.(x-x0) + R1
  /.(x-x0) by A4;
  consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L.(x
  -x0) + R/.(x-x0) by A2;
  consider L2,R2 such that
A8: for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L2.(x-x0) + R2
  /.(x-x0) by A7;
  reconsider R=R1+R2 as RestFunc of S,T by Th28;
  set L=L1+L2;
  consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Th1;
A11: N c= dom f2 by A6,A10;
  N c= dom f1 by A3,A9;
  then N /\ N c= dom f1 /\ dom f2 by A11,XBOOLE_1:27;
  then
A12: N c= dom (f1+f2) by VFUNCT_1:def 1;
A13: R1 is total & R2 is total by Def5;
A14: now
    let x be Point of S;
A15: x0 in N by NFCONT_1:4;
    assume
A16: x in N;
    hence (f1+f2)/.x - (f1+f2)/.x0 = (f1/.x+f2/.x) - (f1+f2)/.x0 by A12,
VFUNCT_1:def 1
      .=f1/.x+f2/.x - (f1/.x0+f2/.x0) by A12,A15,VFUNCT_1:def 1
      .=f1/.x+f2/.x - f1/.x0 - f2/.x0 by RLVECT_1:27
      .=(f1/.x +-f1/.x0) + f2/.x - f2/.x0 by RLVECT_1:def 3
      .=(f1/.x - f1/.x0) + (f2/.x - f2/.x0) by RLVECT_1:def 3
      .=L1.(x-x0)+R1/.(x-x0) + (f2/.x - f2/.x0) by A5,A9,A16
      .=L1.(x-x0)+R1/.(x-x0) + (L2.(x-x0) + R2/.(x-x0)) by A8,A10,A16
      .=R1/.(x-x0)+L1.(x-x0) + L2.(x-x0) + R2/.(x-x0) by RLVECT_1:def 3
      .=(L1.(x-x0)+L2.(x-x0)) + R1/.(x-x0) + R2/.(x-x0) by RLVECT_1:def 3
      .=(L1.(x-x0)+L2.(x-x0)) + (R1/.(x-x0) + R2/.(x-x0)) by RLVECT_1:def 3
      .=L.(x-x0)+(R1/.(x-x0) + R2/.(x-x0)) by LOPBAN_1:35
      .=L.(x-x0)+R/.(x-x0) by A13,VFUNCT_1:37;
  end;
  hence f1+f2 is_differentiable_in x0 by A12;
  hence diff(f1+f2,x0)=L by A12,A14,Def7
    .=diff(f1,x0) + L2 by A1,A3,A5,Def7
    .=diff(f1,x0) + diff(f2,x0) by A2,A6,A8,Def7;
end;

theorem Th36:
  for f1,f2,x0 st f1 is_differentiable_in x0 & f2
  is_differentiable_in x0 holds f1-f2 is_differentiable_in x0 & diff(f1-f2,x0)=
  diff(f1,x0)-diff(f2,x0)
proof
  let f1,f2,x0;
  assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
  consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L.(x
  -x0) + R/.(x-x0) by A1;
  consider L1,R1 such that
A5: for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L1.(x-x0) + R1
  /.(x-x0) by A4;
  consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L.(x
  -x0) + R/.(x-x0) by A2;
  consider L2,R2 such that
A8: for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L2.(x-x0) + R2
  /.(x-x0) by A7;
  reconsider R=R1-R2 as RestFunc of S,T by Th28;
  set L=L1-L2;
  consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Th1;
A11: N c= dom f2 by A6,A10;
  N c= dom f1 by A3,A9;
  then N /\ N c= dom f1 /\ dom f2 by A11,XBOOLE_1:27;
  then
A12: N c= dom (f1-f2) by VFUNCT_1:def 2;
A13: R1 is total & R2 is total by Def5;
A14: now
    let x be Point of S;
A15: x0 in N by NFCONT_1:4;
    assume
A16: x in N;
    hence (f1-f2)/.x - (f1-f2)/.x0 = (f1/.x-f2/.x) - (f1-f2)/.x0 by A12,
VFUNCT_1:def 2
      .=f1/.x - f2/.x - (f1/.x0-f2/.x0) by A12,A15,VFUNCT_1:def 2
      .=f1/.x - f2/.x - f1/.x0 + f2/.x0 by RLVECT_1:29
      .=f1/.x - (f1/.x0 + f2/.x) + f2/.x0 by RLVECT_1:27
      .=f1/.x - f1/.x0 - f2/.x + f2/.x0 by RLVECT_1:27
      .=f1/.x - f1/.x0 - (f2/.x - f2/.x0) by RLVECT_1:29
      .=L1.(x-x0) + R1/.(x-x0) - (f2/.x - f2/.x0) by A5,A9,A16
      .=L1.(x-x0) + R1/.(x-x0) - (L2.(x-x0) + R2/.(x-x0)) by A8,A10,A16
      .=L1.(x-x0) + R1/.(x-x0) - L2.(x-x0) - R2/.(x-x0) by RLVECT_1:27
      .=L1.(x-x0) + (R1/.(x-x0) +- L2.(x-x0)) - R2/.(x-x0) by RLVECT_1:def 3
      .=L1.(x-x0) - (L2.(x-x0) - R1/.(x-x0)) - R2/.(x-x0) by RLVECT_1:33
      .=L1.(x-x0) - L2.(x-x0) + R1/.(x-x0) - R2/.(x-x0) by RLVECT_1:29
      .=L1.(x-x0) - L2.(x-x0) + (R1/.(x-x0) - R2/.(x-x0)) by RLVECT_1:def 3
      .=L.(x-x0) + (R1/.(x-x0) - R2/.(x-x0)) by LOPBAN_1:40
      .=L.(x-x0) + R/.(x-x0) by A13,VFUNCT_1:37;
  end;
  hence f1-f2 is_differentiable_in x0 by A12;
  hence diff(f1-f2,x0)=L by A12,A14,Def7
    .=diff(f1,x0) - L2 by A1,A3,A5,Def7
    .=diff(f1,x0) - diff(f2,x0) by A2,A6,A8,Def7;
end;

theorem Th37:
  for r,f,x0 st f is_differentiable_in x0 holds r(#)f
  is_differentiable_in x0 & diff((r(#)f),x0) = r*diff(f,x0)
proof
  let r,f,x0;
  assume
A1: f is_differentiable_in x0;
  then consider N1 be Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L,R st for x be Point of S st x in N1 holds f/.x - f/.x0 = L.(x-
  x0) + R/.(x-x0);
  consider L1,R1 such that
A4: for x be Point of S st x in N1 holds f/.x - f/.x0 = L1.(x-x0) + R1/.
  (x-x0) by A3;
  reconsider R = r(#)R1 as RestFunc of S,T by Th29;
  set L = r*L1;
A5: N1 c= dom(r(#)f) by A2,VFUNCT_1:def 4;
A6: R1 is total by Def5;
A7: now
    let x be Point of S;
A8: x0 in N1 by NFCONT_1:4;
    assume
A9: x in N1;
    hence (r(#)f)/.x - (r(#)f)/.x0 = r*(f/.x) - (r(#)f)/.x0 by A5,
VFUNCT_1:def 4
      .= r*f/.x - r*f/.x0 by A5,A8,VFUNCT_1:def 4
      .= r*(f/.x - f/.x0) by RLVECT_1:34
      .= r*(L1.(x-x0) + R1/.(x-x0)) by A4,A9
      .= r*L1.(x-x0) + r*R1/.(x-x0) by RLVECT_1:def 5
      .= L.(x-x0) + r*R1/.(x-x0) by LOPBAN_1:36
      .= L.(x-x0) + R/.(x-x0) by A6,VFUNCT_1:39;
  end;
  hence r(#)f is_differentiable_in x0 by A5;
  hence diff((r(#)f),x0) = L by A5,A7,Def7
    .= r*diff(f,x0) by A1,A2,A4,Def7;
end;

theorem
  for f be PartFunc of S,S for Z be Subset of S st Z is open & Z c= dom
  f & f|Z = id Z holds f is_differentiable_on Z & for x be Point of S st x in Z
  holds (f`|Z)/.x = id (the carrier of S)
proof
  set L= id (the carrier of S);
  R_NormSpace_of_BoundedLinearOperators(S,S) = NORMSTR (#
    BoundedLinearOperators(S,S), Zero_(BoundedLinearOperators(S,S),
    R_VectorSpace_of_LinearOperators(S,S)), Add_(BoundedLinearOperators(S,S),
    R_VectorSpace_of_LinearOperators(S,S)), Mult_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), BoundedLinearOperatorsNorm(S,S) #) & L
  is Lipschitzian LinearOperator of S,S by LOPBAN_1:def 14,LOPBAN_2:3;
  then reconsider L as Point of R_NormSpace_of_BoundedLinearOperators(S,S) by
LOPBAN_1:def 9;
  let f be PartFunc of S,S;
  let Z be Subset of S such that
A1: Z is open;
  reconsider R = (the carrier of S) --> 0.S as PartFunc of S,S;
A2: dom R = (the carrier of S);
  now
    let h;
    assume h is non-zero;

A3: now
      let n be Nat;
A4:   R/.(h.n) =R.(h.n) by A2,PARTFUN1:def 6
        .=0.S;
A5:   rng h c= dom R;
A6:   n in NAT by ORDINAL1:def 12;
      thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
        .= (||.h.||".n)*(R/.(h.n)) by A6,A5,FUNCT_2:109
        .= 0.S by A4,RLVECT_1:10;
    end;
    then
A7: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
    hence (||.h.||")(#)(R/*h) is convergent by Th18;
    ((||.h.||")(#)(R/*h)).0 = 0.S by A3;
    hence lim ((||.h.||")(#)(R/*h)) = 0.S by A7,Th18;
  end;
  then reconsider R as RestFunc of S,S by Def5;
  assume that
A8: Z c= dom f and
A9: f|Z = id Z;
A10: now
    let x be Point of S;
    assume
A11: x in Z;
    then f|Z.x = x by A9,FUNCT_1:18;
    then f.x = x by A11,FUNCT_1:49;
    hence f/.x =x by A8,A11,PARTFUN1:def 6;
  end;
A12: now
    let x0 be Point of S;
    assume
A13: x0 in Z;
    then consider N being Neighbourhood of x0 such that
A14: N c= Z by A1,Th2;
A15: for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x- x0)
    proof
      let x be Point of S;
A16:  R/.(x-x0) =R.(x-x0) by A2,PARTFUN1:def 6
        .=0.S;
      assume x in N;
      hence f/.x - f/.x0 = x - f/.x0 by A10,A14
        .= x - x0 by A10,A13
        .= L.(x-x0)
        .= L.(x-x0) + R/.(x-x0) by A16,RLVECT_1:4;
    end;
    N c= dom f by A8,A14;
    hence f is_differentiable_in x0 by A15;
  end;
  hence
A17: f is_differentiable_on Z by A1,A8,Th31;
  let x0 be Point of S;
  assume
A18: x0 in Z;
  then consider N1 being Neighbourhood of x0 such that
A19: N1 c= Z by A1,Th2;
A20: f is_differentiable_in x0 by A12,A18;
  then ex N being Neighbourhood of x0 st N c= dom f & ex L be Point of
R_NormSpace_of_BoundedLinearOperators(S,S),
 R be RestFunc of S,S st for x be Point
  of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0);
  then consider N being Neighbourhood of x0 such that
A21: N c= dom f;
  consider N2 being Neighbourhood of x0 such that
A22: N2 c= N1 and
A23: N2 c= N by Th1;
A24: N2 c= dom f by A21,A23;
A25: for x be Point of S st x in N2 holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0 )
  proof
    let x be Point of S;
A26: R/.(x-x0) =R.(x-x0) by A2,PARTFUN1:def 6
      .=0.S;
    assume x in N2;
    then x in N1 by A22;
    hence f/.x - f/.x0 = x - f/.x0 by A10,A19
      .= x - x0 by A10,A18
      .= L.(x-x0)
      .= L.(x-x0) + R/.(x-x0) by A26,RLVECT_1:4;
  end;
  thus (f`|Z)/.x0 = diff(f,x0) by A17,A18,Def9
    .= id the carrier of S by A20,A24,A25,Def7;
end;

theorem
  for Z be Subset of S st Z is open for f1,f2 st Z c= dom (f1+f2) & f1
  is_differentiable_on Z & f2 is_differentiable_on Z holds f1+f2
is_differentiable_on Z & for x be Point of S st x in Z holds ((f1+f2)`|Z)/.x =
  diff(f1,x) + diff(f2,x)
proof
  let Z be Subset of S such that
A1: Z is open;
  let f1,f2;
  assume that
A2: Z c= dom (f1+f2) and
A3: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
  now
    let x0 be Point of S;
    assume x0 in Z;
    then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1,A3,Th31;
    hence f1+f2 is_differentiable_in x0 by Th35;
  end;
  hence
A4: f1+f2 is_differentiable_on Z by A1,A2,Th31;
  now
    let x be Point of S;
    assume
A5: x in Z;
    then
A6: f1 is_differentiable_in x & f2 is_differentiable_in x by A1,A3,Th31;
    thus ((f1+f2)`|Z)/.x = diff((f1+f2),x) by A4,A5,Def9
      .= diff(f1,x) + diff(f2,x) by A6,Th35;
  end;
  hence thesis;
end;

theorem
  for Z be Subset of S st Z is open for f1,f2 st Z c= dom (f1-f2) & f1
  is_differentiable_on Z & f2 is_differentiable_on Z holds f1-f2
is_differentiable_on Z & for x be Point of S st x in Z holds ((f1-f2)`|Z)/.x =
  diff(f1,x) - diff(f2,x)
proof
  let Z be Subset of S such that
A1: Z is open;
  let f1,f2;
  assume that
A2: Z c= dom (f1-f2) and
A3: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
  now
    let x0 be Point of S;
    assume x0 in Z;
    then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1,A3,Th31;
    hence f1-f2 is_differentiable_in x0 by Th36;
  end;
  hence
A4: f1-f2 is_differentiable_on Z by A1,A2,Th31;
  now
    let x be Point of S;
    assume
A5: x in Z;
    then
A6: f1 is_differentiable_in x & f2 is_differentiable_in x by A1,A3,Th31;
    thus ((f1-f2)`|Z)/.x = diff((f1-f2),x) by A4,A5,Def9
      .= diff(f1,x) - diff(f2,x) by A6,Th36;
  end;
  hence thesis;
end;

theorem
  for Z be Subset of S st Z is open for r,f st Z c= dom (r(#)f) & f
is_differentiable_on Z holds r(#)f is_differentiable_on Z & for x be Point of S
  st x in Z holds ((r(#)f)`|Z)/.x =r*diff(f,x)
proof
  let Z be Subset of S such that
A1: Z is open;
  let r,f;
  assume that
A2: Z c= dom (r(#)f) and
A3: f is_differentiable_on Z;
  now
    let x0 be Point of S;
    assume x0 in Z;
    then f is_differentiable_in x0 by A1,A3,Th31;
    hence r(#)f is_differentiable_in x0 by Th37;
  end;
  hence
A4: r(#)f is_differentiable_on Z by A1,A2,Th31;
  now
    let x be Point of S;
    assume
A5: x in Z;
    then
A6: f is_differentiable_in x by A1,A3,Th31;
    thus ((r(#)f)`|Z)/.x = diff((r(#)f),x) by A4,A5,Def9
      .= r*diff(f,x) by A6,Th37;
  end;
  hence thesis;
end;

theorem
  for Z be Subset of S st Z is open holds (Z c= dom f & f|Z is constant
implies f is_differentiable_on Z & for x be Point of S st x in Z holds (f`|Z)/.
  x = 0.R_NormSpace_of_BoundedLinearOperators(S,T))
proof
  let Z be Subset of S such that
A1: Z is open;
  reconsider R = (the carrier of S) --> 0.T as PartFunc of S,T;
  set L=0.R_NormSpace_of_BoundedLinearOperators(S,T);
  assume that
A2: Z c= dom f and
A3: f|Z is constant;
  R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
    BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
    R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
    R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
  then reconsider L as Element of BoundedLinearOperators(S,T);
A4: dom R = the carrier of S;
  now
    let h;
    assume h is non-zero;
A5: now
      let n be Nat;
A6:   R/.(h.n) =R.(h.n) by A4,PARTFUN1:def 6
        .=0.T;
A7:   rng h c= dom R;
A8:   n in NAT by ORDINAL1:def 12;
      thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
        .=(||.h.||".n)*(R/.(h.n)) by A8,A7,FUNCT_2:109
        .=0.T by A6,RLVECT_1:10;
    end;
    then
A9: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
    hence (||.h.||")(#)(R/*h) is convergent by Th18;
    ((||.h.||")(#)(R/*h)).0 = 0.T by A5;
    hence lim ((||.h.||")(#)(R/*h)) = 0.T by A9,Th18;
  end;
  then reconsider R as RestFunc of S,T by Def5;
  consider r be Point of T such that
A10: for x be Point of S st x in Z/\dom f holds f.x=r by A3,PARTFUN2:57;
A11: now
    let x be Point of S;
    assume
A12: x in Z/\dom f;
    Z/\ dom f c= dom f by XBOOLE_1:17;
    hence f/.x=f.x by A12,PARTFUN1:def 6
      .=r by A10,A12;
  end;
A13: ((the carrier of S) --> 0.T) = L by LOPBAN_1:31;
A14: now
    let x0 be Point of S;
    assume
A15: x0 in Z;
    then consider N being Neighbourhood of x0 such that
A16: N c= Z by A1,Th2;
A17: N c= dom f by A2,A16;
A18: x0 in Z/\dom f by A2,A15,XBOOLE_0:def 4;
    for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0)
    proof
      let x be Point of S;
A19:  R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
        .=0.T;
      assume x in N;
      then x in Z/\dom f by A16,A17,XBOOLE_0:def 4;
      hence f/.x-f/.x0=r-f/.x0 by A11
        .=r - r by A11,A18
        .=0.T by RLVECT_1:15
        .= 0.T + 0.T by RLVECT_1:4
        .=L.(x-x0)+R/.(x-x0) by A13,A19;
    end;
    hence f is_differentiable_in x0 by A17;
  end;
  hence
A20: f is_differentiable_on Z by A1,A2,Th31;
  let x0 be Point of S;
  assume
A21: x0 in Z;
  then consider N being Neighbourhood of x0 such that
A22: N c= Z by A1,Th2;
A23: N c= dom f by A2,A22;
A24: x0 in Z/\dom f by A2,A21,XBOOLE_0:def 4;
A25: for x be Point of S st x in N holds f/.x-f/.x0 =L.(x-x0)+R/.(x-x0)
  proof
    let x be Point of S;
A26: R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
      .=0.T;
    assume x in N;
    then x in Z/\dom f by A22,A23,XBOOLE_0:def 4;
    hence f/.x - f/.x0 = r - f/.x0 by A11
      .=r - r by A11,A24
      .=0.T by RLVECT_1:15
      .= 0.T + 0.T by RLVECT_1:4
      .=L.(x-x0) + R/.(x-x0) by A13,A26;
  end;
A27: f is_differentiable_in x0 by A14,A21;
  thus (f`|Z)/.x0 = diff(f,x0) by A20,A21,Def9
    .=0.R_NormSpace_of_BoundedLinearOperators(S,T) by A27,A23,A25,Def7;
end;

theorem
  for f be PartFunc of S,S for r be Real for p be Point of S for Z be
  Subset of S st Z is open holds ( Z c= dom f & (for x be Point of S st x in Z
holds f/.x = r*x + p) implies f is_differentiable_on Z & for x be Point of S st
  x in Z holds (f`|Z)/.x = r * FuncUnit(S) )
proof
  let f be PartFunc of S,S;
  let r be Real;
  let p be Point of S;
  let Z be Subset of S such that
A1: Z is open;
A2: R_NormSpace_of_BoundedLinearOperators(S,S) = NORMSTR (#
    BoundedLinearOperators(S,S), Zero_(BoundedLinearOperators(S,S),
    R_VectorSpace_of_LinearOperators(S,S)), Add_(BoundedLinearOperators(S,S),
    R_VectorSpace_of_LinearOperators(S,S)), Mult_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), BoundedLinearOperatorsNorm(S,S) #) by
LOPBAN_1:def 14;
  then reconsider
  II=FuncUnit(S) as Point of R_NormSpace_of_BoundedLinearOperators(
  S,S);
  set L = r * II;
  reconsider L as Point of R_NormSpace_of_BoundedLinearOperators(S,S);
  reconsider R = (the carrier of S) --> 0.S as PartFunc of S,S;
  assume that
A3: Z c= dom f and
A4: for x be Point of S st x in Z holds f/.x = r*x + p;
A5: L=r*FuncUnit(S) by A2,LOPBAN_2:def 3;
A6: dom R = the carrier of S;
  now
    let h;
    assume  h is non-zero;
A7: now
      let n be Nat;
A8:   R/.(h.n) =R.(h.n) by A6,PARTFUN1:def 6
        .=0.S;
A9:   rng h c= dom R;
A10:  n in NAT by ORDINAL1:def 12;
      thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
        .=(||.h.||".n)*(R/.(h.n)) by A10,A9,FUNCT_2:109
        .=0.S by A8,RLVECT_1:10;
    end;
    then
A11: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
    hence (||.h.||")(#)(R/*h) is convergent by Th18;
    ((||.h.||")(#)(R/*h)).0 = 0.S by A7;
    hence lim ((||.h.||")(#)(R/*h)) = 0.S by A11,Th18;
  end;
  then reconsider R as RestFunc of S,S by Def5;
A12: now
    let x0 be Point of S;
    assume
A13: x0 in Z;
    then consider N being Neighbourhood of x0 such that
A14: N c= Z by A1,Th2;
A15: for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0)
    proof
      let x be Point of S;
A16:  R/.(x-x0) =R.(x-x0) by A6,PARTFUN1:def 6
        .=0.S;
      (x-x0)=(id the carrier of S).(x-x0);
      then
A17:  r* (x-x0)=r* ((FuncUnit(S)).(x-x0)) by LOPBAN_2:def 5
        .=L.(x-x0) by LOPBAN_1:36;
      assume x in N;
      hence f/.x-f/.x0=r*x+p-f/.x0 by A4,A14
        .=r*x+p - (r*x0+p) by A4,A13
        .=r*x+(p-(r*x0+p)) by RLVECT_1:def 3
        .=r*x+(p-r*x0-p) by RLVECT_1:27
        .=r*x+(p+-r*x0-p)
        .=r*x+(-r*x0+(p-p)) by RLVECT_1:def 3
        .=r*x+(-r*x0+0.S) by RLVECT_1:15
        .=r*x-r*x0 by RLVECT_1:4
        .=r*(x-x0) by RLVECT_1:34
        .=L.(x-x0)+R/.(x-x0) by A16,A17,RLVECT_1:4;
    end;
    N c= dom f by A3,A14;
    hence f is_differentiable_in x0 by A15;
  end;
  hence
A18: f is_differentiable_on Z by A1,A3,Th31;
  let x0 be Point of S;
  assume
A19: x0 in Z;
  then consider N being Neighbourhood of x0 such that
A20: N c= Z by A1,Th2;
A21: for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0)
  proof
    let x be Point of S;
A22: R/.(x-x0) =R.(x-x0) by A6,PARTFUN1:def 6
      .=0.S;
    (x-x0)=(id the carrier of S).(x-x0);
    then
A23: r* (x-x0)=r* ((FuncUnit(S)).(x-x0)) by LOPBAN_2:def 5
      .=L.(x-x0) by LOPBAN_1:36;
    assume x in N;
    hence f/.x - f/.x0 = r*x+p - f/.x0 by A4,A20
      .=r*x+p-(r*x0+p) by A4,A19
      .=r*x+(p-(r*x0+p)) by RLVECT_1:def 3
      .=r*x+(p-r*x0-p) by RLVECT_1:27
      .=r*x+(p+-r*x0-p)
      .=r*x+(-r*x0+(p-p)) by RLVECT_1:def 3
      .=r*x+(-r*x0+0.S) by RLVECT_1:15
      .=r*x-r*x0 by RLVECT_1:4
      .=r*(x-x0) by RLVECT_1:34
      .=L.(x-x0)+R/.(x-x0) by A22,A23,RLVECT_1:4;
  end;
A24: N c= dom f by A3,A20;
A25: f is_differentiable_in x0 by A12,A19;
  thus (f`|Z)/.x0 = diff(f,x0) by A18,A19,Def9
    .=r * FuncUnit(S) by A5,A25,A24,A21,Def7;
end;

theorem Th44:
  for x0 be Point of S holds f is_differentiable_in x0 implies f
  is_continuous_in x0
proof
  let x0 be Point of S;
  assume
A1: f is_differentiable_in x0;
  then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
  ex L,R st for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0 ) +
  R/.(x-x0);
A3: now
    consider g be Real such that
A4: 0<g and
A5: {y where y is Point of S:||.y-x0.|| < g } c= N by NFCONT_1:def 1;
    reconsider s2 = NAT --> x0 as sequence of S;
    let s1 be sequence of S such that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Nat holds s1.n<>x0;
    consider l be Nat such that
A10: for m be Nat st l<=m holds ||.s1.m-x0.||<g by A7,A8,A4,
NORMSP_1:def 7;
    deffunc G(Nat) = s1.$1-s2.$1;
    consider s3 be sequence of S such that
A11: for n holds s3.n=G(n) from FUNCT_2:sch 4;
A12: for n being Nat holds s3.n=G(n)
      proof let n be Nat;
        n in NAT by ORDINAL1:def 12;
       hence thesis by A11;
      end;
A13: now
      given n such that
A14:  s3.n=0.S;
      s1.n-s2.n=0.S by A12,A14;
      then s1.n-x0=0.S;
      hence contradiction by A9,RLVECT_1:21;
    end;
    now
      given n being Nat such that
A15:  (s3^\l).n=0.S;
A16:   n+l in NAT by ORDINAL1:def 12;
      s3.(n+l)=0.S by A15,NAT_1:def 3;
      hence contradiction by A13,A16;
    end;
    then
A17: s3^\l is non-zero by Th7;
    reconsider c =s2^\l as constant sequence of S;
A18: s3=s1-s2 by A12,NORMSP_1:def 3;
A19: s2 is convergent by Th18;
    then
A20: s3 is convergent by A7,A18,NORMSP_1:20;
    then
A21: s3^\l is convergent by LOPBAN_3:9;
    lim s2 = s2.0 by Th18
      .=x0;
    then lim s3 =x0-x0 by A7,A8,A19,A18,NORMSP_1:26
      .=0.S by RLVECT_1:15;
    then lim(s3^\l)=0.S by A20,LOPBAN_3:9;
    then reconsider h=s3^\l as (0.S)-convergent sequence of S
      by A21,Def4;

    now
      let n;
      thus (f/*(h+c)-f/*c+f/*c).n =(f/*(h+c)-f/*c).n+(f/*c).n by NORMSP_1:def 2
        .=(f/*(h+c)).n-(f/*c).n+(f/*c).n by NORMSP_1:def 3
        .=(f/*(h+c)).n-((f/*c).n-(f/*c).n) by RLVECT_1:29
        .=(f/*(h+c)).n-0.T by RLVECT_1:15
        .=(f/*(h+c)).n by RLVECT_1:13;
    end;
    then
A22: f/*(h+c)-f/*c+(f/*c)=f/*(h+c) by FUNCT_2:63;
    now
      let n;
      thus (h+c).n=((s1-s2+s2)^\l).n by A18,Th15
        .=(s1-s2+s2).(n+l) by NAT_1:def 3
        .=(s1-s2).(n+l)+s2.(n+l) by NORMSP_1:def 2
        .=s1.(n+l)-s2.(n+l)+s2.(n+l) by NORMSP_1:def 3
        .=s1.(n+l)-(s2.(n+l)-s2.(n+l)) by RLVECT_1:29
        .=s1.(n+l)-0.S by RLVECT_1:15
        .=s1.(l+n) by RLVECT_1:13
        .=(s1^\l).n by NAT_1:def 3;
    end;
    then
A23: f/*(h+c)-f/*c+(f/*c)=f/*(s1^\l) by A22,FUNCT_2:63
      .=(f/*s1)^\l by A6,VALUED_0:27;
A24: rng c = {x0}
    proof
      thus rng c c= {x0}
      proof
        let y be object;
        assume y in rng c;
        then consider n being Nat such that
A25:    y=(s2^\l).n by NFCONT_1:6;
A26:     n+l in NAT by ORDINAL1:def 12;
        y=s2.(n+l) by A25,NAT_1:def 3;
        then y=x0 by FUNCOP_1:7,A26;
        hence thesis by TARSKI:def 1;
      end;
      let y be object;
      assume y in {x0};
      then
A27:  y=x0 by TARSKI:def 1;
A28:     0+l in NAT by ORDINAL1:def 12;
      c.0=s2.(0+l) by NAT_1:def 3
        .= y by A27,FUNCOP_1:7,A28;
      hence thesis by NFCONT_1:6;
    end;
A29: now
      let p be Real such that
A30:  0<p;
       reconsider n=0 as Nat;
      take n;
      let m be Nat such that
      n<=m;
A31:   m in NAT by ORDINAL1:def 12;
A32:   m+l in NAT by ORDINAL1:def 12;
      x0 in N by NFCONT_1:4;
      then rng c c= dom f by A2,A24,ZFMISC_1:31;
      then ||.(f/*c).m-f/.x0.|| =||.f/.(c.m)-f/.x0.|| by FUNCT_2:109,A31
        .=||.f/.(s2.(m+l))-f/.x0.|| by NAT_1:def 3
        .=||.f/.x0-f/.x0.|| by FUNCOP_1:7,A32
        .=||.0.T.|| by RLVECT_1:15
        .=0 by NORMSP_1:1;
      hence ||.(f/*c).m-f/.x0.||<p by A30;
    end;
    then
A33: f/*c is convergent;
A34: rng (h+c) c= N
    proof
      let y be object;
      assume
A35:  y in rng(h+c);
      then consider n being Nat such that
A36:  y=(h+c).n by NFCONT_1:6;
      reconsider y1=y as Point of S by A35;
      (h+c).n=((s1-s2+s2)^\l).n by A18,Th15
        .=(s1-s2+s2).(n+l) by NAT_1:def 3
        .=(s1-s2).(n+l)+s2.(n+l) by NORMSP_1:def 2
        .=s1.(n+l)-s2.(n+l)+s2.(n+l) by NORMSP_1:def 3
        .=s1.(n+l)-(s2.(n+l)-s2.(n+l)) by RLVECT_1:29
        .=s1.(n+l)-0.S by RLVECT_1:15
        .=s1.(l+n) by RLVECT_1:13;
      then ||.(h+c).n-x0.||<g by A10,NAT_1:12;
      then y1 in {z where z is Point of S:||.z-x0.|| < g } by A36;
      hence thesis by A5;
    end;
    then
A37: (f/*(h+c) - f/*c) is convergent by A17,A1,A2,A24,Th34;
    then f/*(h+c)-f/*c+f/*c is convergent by A33,NORMSP_1:19;
    hence f/*s1 is convergent by A23,LOPBAN_3:10;
A38: lim (f/*(h+c) - f/*c) = 0.T by A17,A1,A2,A24,A34,Th34;
    lim(f/*c)=f/.x0 by A29,A33,NORMSP_1:def 7;
    then lim(f/*(h+c)-f/*c+f/*c)=0.T +f/.x0 by A37,A38,A33,NORMSP_1:25
      .=f/.x0 by RLVECT_1:4;
    hence f/.x0=lim(f/*s1) by A37,A33,A23,LOPBAN_3:11,NORMSP_1:19;
  end;
  x0 in N by NFCONT_1:4;
  hence thesis by A2,A3,Th27;
end;

theorem
  f is_differentiable_on X implies f is_continuous_on X
by Th44;

theorem
  for Z be Subset of S st Z is open holds ( f is_differentiable_on X & Z
  c= X implies f is_differentiable_on Z )
proof
  let Z be Subset of S such that
A1: Z is open;
  assume that
A2: f is_differentiable_on X and
A3: Z c= X;
  X c= dom f by A2;
  hence
A4: Z c= dom f by A3;
  let x0;
  assume
A5: x0 in Z;
  then consider N1 being Neighbourhood of x0 such that
A6: N1 c= Z by A1,Th2;
  f|X is_differentiable_in x0 by A2,A3,A5;
  then consider N being Neighbourhood of x0 such that
A7: N c= dom(f|X) and
A8: ex L,R st for x be Point of S st x in N holds (f|X)/.x-(f|X)/.x0=L.(
  x-x0)+R/.(x-x0);
  consider N2 being Neighbourhood of x0 such that
A9: N2 c= N and
A10: N2 c= N1 by Th1;
A11: N2 c= Z by A6,A10;
  take N2;
  dom(f|X)=dom f/\X by RELAT_1:61;
  then dom(f|X) c=dom f by XBOOLE_1:17;
  then N c= dom f by A7;
  then N2 c=dom f by A9;
  then N2 c=dom f/\Z by A11,XBOOLE_1:19;
  hence
A12: N2 c=dom(f|Z) by RELAT_1:61;
  consider L,R such that
A13: for x be Point of S st x in N holds (f|X)/.x-(f|X)/.x0=L.(x-x0)+R/.
  (x-x0) by A8;
  take L,R;
  let x be Point of S;
  assume
A14: x in N2;
  then (f|X)/.x-(f|X)/.x0=L.(x-x0)+R/.(x-x0) by A9,A13;
  then
A15: (f|X)/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A3,A4,A5,PARTFUN2:17;
  x in N by A9,A14;
  then f/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A7,A15,PARTFUN2:15;
  then f/.x-(f|Z)/.x0=L.(x-x0)+R/.(x-x0) by A4,A5,PARTFUN2:17;
  hence thesis by A12,A14,PARTFUN2:15;
end;

theorem
  f is_differentiable_in x0 implies ex N being Neighbourhood of x0 st N
c= dom f & ex R st R/.0.S=0.T & R is_continuous_in 0.S & for x be Point of S st
  x in N holds f/.x-f/.x0 = diff(f,x0).(x-x0) + R/.(x-x0)
proof
  assume f is_differentiable_in x0;
  then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: ex R st for x be Point of S st x in N holds f/.x - f/.x0 = diff(f,x0
  ).(x-x0) + R/.(x-x0) by Def7;
  take N;
  ex R st R/.0.S=0.T & R is_continuous_in 0.S & for x be Point of S st x
  in N holds f/.x-f/.x0 = diff(f,x0).(x-x0) + R/.(x-x0)
  proof
    R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
      BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
      R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
    then reconsider L =diff(f,x0) as Element of BoundedLinearOperators(S,T);
    consider R such that
A3: for x be Point of S st x in N holds f/.x-f/.x0 = diff(f,x0).(x-x0)
    + R/.(x-x0) by A2;
    take R;
    f/.x0 - f/.x0 = L.(x0-x0) + R/.(x0-x0) by A3,NFCONT_1:4;
    then 0.T = L.(x0-x0) + R/.(x0-x0) by RLVECT_1:15;
    then 0.T = L.0.S + R/.(x0-x0) by RLVECT_1:15;
    then
A4: 0.T = L.0.S + R/.0.S by RLVECT_1:15;
    L.(0.S) =modetrans(L,S,T).(0.S) by LOPBAN_1:def 11
      .= modetrans(L,S,T).(0*0.S) by RLVECT_1:10
      .=0*modetrans(L,S,T).0.S by LOPBAN_1:def 5
      .=0.T by RLVECT_1:10;
    hence
A5: R/.0.S=0.T by A4,RLVECT_1:4;
A6: now
      let s1 be sequence of S;
      assume that
      rng s1 c= dom R and
A7:   s1 is convergent & lim s1 = 0.S and
A8:   for n being Nat holds s1.n<>0.S;
      A9: s1 is (0.S)-convergent sequence of S by A7,Def4;
      s1 is non-zero by A8,Th7;
      hence R/*s1 is convergent & lim (R/*s1)=R/.(0.S) by A5,A9,Th24;
    end;
    R is total by Def5;
    then dom R=the carrier of S by PARTFUN1:def 2;
    hence thesis by A3,A6,Th27;
  end;
  hence thesis by A1;
end;


definition
  let S be non trivial RealNormSpace ,T;
  let IT be PartFunc of S,T;
  redefine attr IT is RestFunc-like means
  IT is total & for h be
       non-zero (0.S)-convergent sequence of S
  holds (||.h.||")(#)(IT  /*h) is convergent
  & lim ((||.h.||")(#)(IT/*h)) = 0.T;
  correctness;
end;