:: Contracting Mapping on Normed Linear Space
::  by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received August 19, 2012
:: Copyright (c) 2012-2021 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 PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS,
      CARD_1, XXREAL_0, FUNCT_7, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_1,
      SEQ_2, POWER, RSSPACE3, LOPBAN_1, ORDEQ_01, STRUCT_0, COMPLEX1, VALUED_1,
      ALI2, SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, FINSEQ_1, TARSKI, INTEGRA5,
      CARD_3, XXREAL_1, PARTFUN1, RLVECT_1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0,
      XXREAL_2, FCONT_1, ALGSTR_0, CFCONT_1, MEASURE5, RLSUB_1, RELAT_2,
      REWRITE1, NFCONT_1, C0SP2, RSSPACE, RSSPACE4, FUNCOP_1, REALSET1,
      FDIFF_1, PREPOWER, INTEGRA7, METRIC_1, SERIES_1, SIN_COS, SEQFUNC,
      REAL_NS1, FINSEQ_2, EUCLID, NEWTON, XCMPLX_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
      PARTFUN1, FUNCT_2, PARTFUN2, NUMBERS, XXREAL_0, XREAL_0, REAL_1, NAT_1,
      VALUED_0, COMPLEX1, XCMPLX_0, XXREAL_2, FUNCOP_1, FINSEQ_1, VALUED_1,
      FINSEQ_2, SEQ_1, SEQ_2, NEWTON, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1,
      FUNCT_7, ABIAN, PREPOWER, POWER, SERIES_1, SEQFUNC, MEASURE5, SIN_COS,
      TAYLOR_1, INTEGRA1, INTEGRA5, INTEGRA7, STRUCT_0, ALGSTR_0, PRE_TOPC,
      RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, VFUNCT_1, RSSPACE, EUCLID,
      RSSPACE3, LOPBAN_1, NFCONT_1, INTEGR19, RSSPACE4, REAL_NS1, PDIFF_1,
      INTEGR15, INTEGR18, NFCONT_3, NDIFF_3, NFCONT_2, NFCONT_4;
 constructors REAL_1, ABIAN, SEQ_1, SEQ_2, RSSPACE3, RELSET_1, SEQ_4, VFUNCT_1,
      PDIFF_1, INTEGRA5, NFCONT_3, RLSUB_1, PARTFUN2, FCONT_1, NFCONT_1,
      NDIFF_1, NDIFF_3, RSSPACE4, SEQFUNC, INTEGR18, RVSUM_1, BINOP_2,
      INTEGR19, INTEGR15, NFCONT_4, FDIFF_1, VALUED_2, PREPOWER, INTEGRA7,
      COMSEQ_2, COMSEQ_3, SIN_COS, TAYLOR_1, NFCONT_2, C0SP2;
 registrations STRUCT_0, NAT_1, VALUED_1, NORMSP_0, XXREAL_0, NUMBERS,
      XBOOLE_0, FUNCT_1, FUNCT_2, XREAL_0, MEMBERED, NORMSP_1, RELAT_1,
      FINSEQ_2, RELSET_1, INTEGRA1, ORDINAL1, FUNCOP_1, NEWTON, NFCONT_3,
      XXREAL_2, RSSPACE4, RCOMP_1, RLVECT_1, REAL_NS1, VALUED_0, FINSEQ_1,
      FDIFF_1, FCONT_1, EUCLID, MEASURE5, VALUED_2, FCONT_3, POWER, NFCONT_4,
      PREPOWER;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: The Principle of Contracting Mapping on Normed Linear Space

reserve n for non zero Element of NAT;
reserve a,b,r,t for Real;

definition
  let f be Function;
  attr f is with_unique_fixpoint means
:: ORDEQ_01:def 1
  ex x being set st x is_a_fixpoint_of f &
  for y being set st y is_a_fixpoint_of f holds x = y;
end;

theorem :: ORDEQ_01:1
  for x being set holds x is_a_fixpoint_of {[x,x]};

theorem :: ORDEQ_01:2
  for x,y,z being set st x is_a_fixpoint_of {[y,z]} holds x = y;

registration
  let x be set;
  cluster {[x,x]} -> with_unique_fixpoint;
end;

theorem :: ORDEQ_01:3
  for X being RealNormSpace, x being Point of X holds
  (for e being Real st e > 0 holds ||.x.|| < e) implies x = 0.X;

theorem :: ORDEQ_01:4
  for X being RealNormSpace, x,y being Point of X holds
  (for e being Real st e > 0 holds ||.x-y.|| < e) implies x = y;

theorem :: ORDEQ_01:5
  for K, L, e being Real st 0 < K & K < 1 & 0 < e
  ex n being Nat st |. L*(K to_power n) .| < e;

registration
  let X be RealNormSpace;
  cluster constant -> contraction for Function of X,X;
end;

registration
  let X be RealBanachSpace;
  cluster contraction -> with_unique_fixpoint for Function of X,X;
end;

::$CT

theorem :: ORDEQ_01:7
  for X being RealBanachSpace, f being Function of X,X st
      ex n0 being Nat st iter(f,n0) is contraction holds
  f is with_unique_fixpoint;

theorem :: ORDEQ_01:8
  for X being RealBanachSpace, f being Function of X,X st
      ex n0 being Element of NAT st iter(f,n0) is contraction holds
   ex xp being Point of X st f.xp = xp &
      for x being Point of X st f.x = x holds xp = x;

begin :: The Real Banach Space C([a,b],X)

theorem :: ORDEQ_01:9
 for X be non empty closed_interval Subset of REAL,
      Y be RealNormSpace,
      f be continuous PartFunc of REAL,Y
       st dom f = X holds
    f is bounded Function of X,Y;

definition
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  func ContinuousFunctions(X,Y)
  -> Subset of R_VectorSpace_of_BoundedFunctions(X,Y) means
:: ORDEQ_01:def 2
  for x being set holds x in it iff
  ex f be continuous PartFunc of REAL,Y st x = f & dom f = X;
 end;

registration
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  cluster ContinuousFunctions(X,Y) -> non empty;
end;

registration
  let X be non empty closed_interval Subset of REAL, Y be RealNormSpace;
  cluster ContinuousFunctions(X,Y) -> linearly-closed;
 end;

definition
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  func R_VectorSpace_of_ContinuousFunctions(X,Y) -> strict RealLinearSpace
    equals
:: ORDEQ_01:def 3
    RLSStruct (# ContinuousFunctions(X,Y), Zero_(ContinuousFunctions(X,Y),
    R_VectorSpace_of_BoundedFunctions (X,Y)), Add_(ContinuousFunctions(X,Y),
    R_VectorSpace_of_BoundedFunctions (X,Y)), Mult_(ContinuousFunctions(X,Y),
    R_VectorSpace_of_BoundedFunctions(X,Y)) #);
end;

registration
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  cluster R_VectorSpace_of_ContinuousFunctions(X,Y) ->
    Abelian add-associative
    right_zeroed right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital;
end;

theorem :: ORDEQ_01:10
  for X be non empty closed_interval Subset of REAL, Y be RealNormSpace,
  f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y),
  f9,g9,h9 be continuous PartFunc of REAL,Y
     st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
         holds (h = f+g iff for x
  be Element of X holds h9/.x = f9/.x + g9/.x );

theorem :: ORDEQ_01:11
  for X be non empty closed_interval Subset of REAL, Y be RealNormSpace,
   f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y),
   f9,h9 be continuous PartFunc of REAL,Y
      st f9=f & h9=h & dom f9=X & dom h9=X
      holds h = a*f iff for x be Element of X holds h9/.x = a*f9/.x;

theorem :: ORDEQ_01:12
  for X be non empty closed_interval Subset of REAL, Y be RealNormSpace holds
  0. R_VectorSpace_of_ContinuousFunctions(X,Y) = X -->0.Y;

definition
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  func ContinuousFunctionsNorm(X,Y) ->
    Function of ContinuousFunctions(X,Y),REAL equals
:: ORDEQ_01:def 4
  (BoundedFunctionsNorm(X,Y)) | (ContinuousFunctions(X,Y));
end;

definition
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  let f be set such that
 f in ContinuousFunctions(X,Y);
  func modetrans(f,X,Y) -> continuous PartFunc of REAL,Y means
:: ORDEQ_01:def 5
  it = f & dom it = X;
end;

definition
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  func R_NormSpace_of_ContinuousFunctions(X,Y) -> strict non empty NORMSTR
  equals
:: ORDEQ_01:def 6
  NORMSTR (# ContinuousFunctions(X,Y),
  Zero_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
  Add_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
  Mult_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
  ContinuousFunctionsNorm(X,Y) #);
end;

theorem :: ORDEQ_01:13
  for X be non empty closed_interval Subset of REAL,Y be RealNormSpace,
      f be continuous PartFunc of REAL,Y
    st dom f=X holds modetrans(f,X,Y)=f;

theorem :: ORDEQ_01:14
  for X be non empty closed_interval Subset of REAL,
  Y be RealNormSpace holds (X --> 0.Y)
  = 0.R_NormSpace_of_ContinuousFunctions(X,Y);

theorem :: ORDEQ_01:15
  for X be non empty closed_interval Subset of REAL,
      Y be RealNormSpace, f,g,h be Point of
         R_NormSpace_of_ContinuousFunctions(X,Y),
      f9,g9,h9 be continuous PartFunc of REAL,Y
  st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
    holds (h = f+g iff for x be Element of X
  holds h9/.x = f9/.x + g9/.x);

theorem :: ORDEQ_01:16
 for X be non empty closed_interval Subset of REAL,
     Y be RealNormSpace,
     f,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
     f9,h9 be continuous PartFunc of REAL,Y
   st f9=f & h9=h & dom f9=X & dom h9=X
     holds (h = a*f iff for x be Element of X
  holds h9/.x = a*f9/.x);

theorem :: ORDEQ_01:17
  for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
      f be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
      g be Point of R_NormSpace_of_BoundedFunctions(X,Y)
      st f=g holds ||.f.|| = ||.g.||;

theorem :: ORDEQ_01:18
  for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
    f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
    f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y)
      st f1=f & g1=g holds f+g = f1+g1;

theorem :: ORDEQ_01:19
  for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
      f be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
     f1 be Point of R_NormSpace_of_BoundedFunctions(X,Y) st f1=f
      holds a*f = a*f1;

registration
  let X be non empty closed_interval Subset of REAL;
  let Y be RealNormSpace;
  cluster R_NormSpace_of_ContinuousFunctions(X,Y) ->
    reflexive discerning RealNormSpace-like vector-distributive
    scalar-distributive scalar-associative scalar-unital
    Abelian add-associative right_zeroed right_complementable;
end;

theorem :: ORDEQ_01:20
  for X be non empty closed_interval Subset of REAL
  for Y be RealNormSpace
  for f,g,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y)
  for f9,g9,h9 be continuous PartFunc of REAL,Y
  st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
  holds (h = f-g iff for x be Element of X holds h9/.x = f9/.x - g9/.x );

theorem :: ORDEQ_01:21
  for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
    f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
    f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y)
      st f1=f & g1=g
      holds f-g = f1-g1;

registration
  let X be non empty closed_interval Subset of REAL,
      Y be RealNormSpace;
  cluster closed for Subset of R_NormSpace_of_BoundedFunctions(X,Y);
end;

theorem :: ORDEQ_01:22
  for X be non empty closed_interval Subset of REAL,
      Y be RealNormSpace holds
    ContinuousFunctions(X,Y)
      is closed Subset of R_NormSpace_of_BoundedFunctions(X,Y);

theorem :: ORDEQ_01:23
  for X be non empty closed_interval Subset of REAL,
      Y be RealNormSpace,
      seq be sequence of R_NormSpace_of_ContinuousFunctions(X,Y)
  st Y is complete &
    seq is Cauchy_sequence_by_Norm holds seq is convergent;

registration
  let X be non empty closed_interval Subset of REAL;
  let Y be RealBanachSpace;
  cluster R_NormSpace_of_ContinuousFunctions(X,Y) -> complete;
end;

theorem :: ORDEQ_01:24
 for X be non empty closed_interval Subset of REAL,
     Y be RealNormSpace,
     v be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
     g be PartFunc of REAL,Y st g=v
  holds for t be Real st t in X holds ||.g/.t.|| <= ||.v.||;

theorem :: ORDEQ_01:25
 for X be non empty closed_interval Subset of REAL,
     Y be RealNormSpace,
     K be Real,
     v being Point of R_NormSpace_of_ContinuousFunctions(X,Y),
     g be PartFunc of REAL,Y st g=v &
     for t be Real st t in X holds ||.g/.t.|| <= K
 holds ||.v.|| <= K;

theorem :: ORDEQ_01:26
 for X be non empty closed_interval Subset of REAL,
     Y be RealNormSpace,
     v1,v2 be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
     g1,g2 be PartFunc of REAL,Y
  st g1=v1 & g2=v2
holds for t be Real st t in X holds
           ||.g1/.t - g2/.t .|| <= ||.v1-v2.||;

theorem :: ORDEQ_01:27
 for X be non empty closed_interval Subset of REAL,
     Y be RealNormSpace,
     K be Real,
     v1,v2 being Point of R_NormSpace_of_ContinuousFunctions(X,Y),
     g1,g2 be PartFunc of REAL,Y
  st g1=v1 & g2=v2 &
   for t be Real st t in X holds
           ||.g1/.t - g2/.t .|| <= K
  holds ||.v1-v2.|| <= K;

begin :: Differential Equations

theorem :: ORDEQ_01:28
for n,i be Nat, f be PartFunc of REAL,REAL n,
 A be Subset of REAL holds proj(i,n)*(f|A) = (proj(i,n)*f)|A;

theorem :: ORDEQ_01:29
  for g be continuous PartFunc of REAL, REAL n st dom g = [' a,b ']
  holds g | [' a,b '] is bounded;

theorem :: ORDEQ_01:30
  for g be continuous PartFunc of REAL,REAL n
     st dom g =[' a,b ']
   holds g is_integrable_on [' a,b '];

theorem :: ORDEQ_01:31
for f,F be PartFunc of REAL,REAL n
  st a <= b
  & dom f =[' a,b '] & dom F =[' a,b ']
  & f is continuous
  & for t be Real st t in [.a,b.] holds F.t = integral(f,a,t)
  holds
    for x be Real st x in [.a,b.] holds F is_continuous_in x;

theorem :: ORDEQ_01:32
  for f be continuous PartFunc of REAL,REAL-NS n st dom f = [' a,b ']
   holds f|([' a,b ']) is bounded;

theorem :: ORDEQ_01:33
  for f be continuous PartFunc of REAL,REAL-NS n st dom f = [' a,b ']
  holds f is_integrable_on [' a,b '];

theorem :: ORDEQ_01:34
  for f be continuous PartFunc of REAL,REAL-NS n,
      F be PartFunc of REAL,REAL-NS n
       st a <= b
          & dom f =[' a,b '] & dom F =[' a,b ']
          & for t be Real st t in [.a,b.] holds F.t = integral(f,a,t)
   holds
 for x be Real st x in [.a,b.] holds F is_continuous_in x;

theorem :: ORDEQ_01:35
  for R be PartFunc of REAL, REAL
    st R is total holds R is RestFunc-like iff
    for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
    st z <> 0 & |. z .| < d holds |.z.|"* |. R/.z .| < r;

reserve
  Z for open Subset of REAL,
 y0 for VECTOR of REAL-NS n,
  G for Function of REAL-NS n,REAL-NS n;

theorem :: ORDEQ_01:36
  for f be continuous PartFunc of REAL,REAL-NS n,
      g be PartFunc of REAL,REAL-NS n st a <= b
          & dom f = [' a,b '] & dom g = [' a,b '] & Z = ]. a,b .[
          & for t be Real st t in [' a,b ']
                 holds g.t = y0+ integral(f,a,t) holds
       g is continuous & g/.a=y0 &
       g is_differentiable_on Z
       & for t be Real st t in Z holds diff(g,t) = f/.t;

theorem :: ORDEQ_01:37
for i be Nat,
    y1,y2 be Point of REAL-NS n holds
  proj(i,n).(y1 + y2) = proj(i,n).y1 + proj(i,n).y2;

theorem :: ORDEQ_01:38
for i be Nat,
   y1 be Point of REAL-NS n, r being Real holds
 proj(i,n).(r*y1) = r*(proj(i,n).y1);

theorem :: ORDEQ_01:39
for g be PartFunc of REAL,REAL-NS n,
   x0 be Real,
    i be Nat st
 1 <= i & i <= n & g is_differentiable_in x0 holds
   (proj(i,n)*g) is_differentiable_in x0 &
   proj(i,n).(diff(g,x0)) = diff((proj(i,n)*g),x0);

theorem :: ORDEQ_01:40
  for f be PartFunc of REAL,REAL-NS n,
      X be set st
      for i be Nat st 1 <= i & i <= n
       holds (proj(i,n)*f) | X is constant
 holds
   f| X is constant;

theorem :: ORDEQ_01:41
  for f be PartFunc of REAL,REAL-NS n
    st ].a,b.[ c= dom f
   & f is_differentiable_on ].a,b.[
   & for x be Real
       st x in ].a,b.[ holds diff(f,x) = 0.(REAL-NS n)
   holds f| (].a,b.[) is constant;

theorem :: ORDEQ_01:42
  for f be continuous PartFunc of REAL,REAL-NS n st a < b
        & [.a,b.] = dom f & f | ].a,b.[ is constant holds
    for x be Real st x in [.a,b.] holds f.x = f.a;

theorem :: ORDEQ_01:43
  for y,Gf be continuous PartFunc of REAL,REAL-NS n,
      g be PartFunc of REAL,REAL-NS n st a<b
     & Z = ]. a,b .[
     & dom y = [' a,b '] & dom g = [' a,b '] & dom Gf = [' a,b ']
     & y is_differentiable_on Z
     & y/.a = y0
     & (for t be Real st t in Z holds diff(y,t) = Gf/.t)
     & (for t be Real st t in [' a,b ']
          holds g.t = y0 + integral(Gf,a,t) )
 holds y=g;

theorem :: ORDEQ_01:44
  for a,b,c,d be Real,
      f be PartFunc of REAL,REAL-NS n
    st a <= b & f is_integrable_on ['a,b']
   & ||. f .|| is_integrable_on ['a,b']
   & f| ['a,b'] is bounded & ['a,b'] c= dom f
   & c in ['a,b'] & d in ['a,b']
  holds ||. f .|| is_integrable_on ['min(c,d),max(c,d)'] &
    (||. f .||) | ['min(c,d),max(c,d)'] is bounded &
    ||. integral(f,c,d) .|| <= integral((||. f .||),min(c,d),max(c,d));

theorem :: ORDEQ_01:45
  for a,b,c,d,e be Real,
              f be PartFunc of REAL,REAL-NS n
    st (a<=b & c <= d & f is_integrable_on ['a,b']
   & ||. f .|| is_integrable_on ['a,b'] & f| ['a,b'] is bounded &
     ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] &
     for x be Real st x in ['c,d'] holds ||. f/.x .|| <= e)
  holds
    ||. integral(f,c,d) .|| <= e * (d-c) &
    ||. integral(f,d,c).|| <= e * (d-c);

theorem :: ORDEQ_01:46
for n be Nat, g be Function of REAL,REAL
  st for x be Real holds g.x= (x-a) |^ (n+1)
 holds
    for x be Real holds g is_differentiable_in x
       & diff(g,x)= (n+1)* ((x-a) |^ n);

theorem :: ORDEQ_01:47
 for n be Nat, g be Function of REAL,REAL
   st for x be Real holds g.x = ((x-a) |^ (n+1)) / ((n+1)! ) holds
   for x be Real holds g is_differentiable_in x
     & diff(g,x) = ((x-a) |^ n) / (n!);

theorem :: ORDEQ_01:48
for f,g be PartFunc of REAL,REAL st a <= t &
    ['a,t'] c= dom f & f is_integrable_on ['a,t'] &
    f| ['a,t'] is bounded &
    ['a,t'] c= dom g & g is_integrable_on ['a,t'] &
    g| ['a,t'] is bounded &
   for x be Real st x in ['a,t'] holds f.x <= g.x holds
  integral(f,a,t) <= integral(g,a,t);

definition
  let n be non zero Element of NAT;
  let y0 be VECTOR of REAL-NS n,
      G be Function of REAL-NS n,REAL-NS n,
      a,b be Real;
  assume  a<=b & G is_continuous_on dom G;
  func Fredholm(G,a,b,y0) -> Function of
             R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
             R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) means
:: ORDEQ_01:def 7

  for x be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
  ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n
     st x=f & it.x = g & dom f =[' a,b '] & dom g =[' a,b '] & Gf = G*f
       & for t be Real st t in [' a,b '] holds g.t = y0 + integral(Gf,a,t);
end;

theorem :: ORDEQ_01:49
  a <= b & 0 < r &
  (for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
  implies
  for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
      g,h be continuous PartFunc of REAL,REAL-NS n
        st g= Fredholm(G,a,b,y0).u & h= Fredholm(G,a,b,y0).v holds
         for t be Real st t in [' a,b '] holds
         ||. g/.t - h/.t .|| <= r*(t-a) * ||.u-v.||;

theorem :: ORDEQ_01:50
  a <= b & 0 < r &
  (for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
  implies
  for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
        m be Element of NAT,
      g,h be continuous PartFunc of REAL,REAL-NS n
        st g = iter(Fredholm(G,a,b,y0),(m+1)).u
         & h = iter(Fredholm(G,a,b,y0),(m+1)).v holds
        for t be Real st t in [' a,b ']
          holds ||. g/.t - h/.t .|| <= ((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.||
;

theorem :: ORDEQ_01:51
  for m be Nat st a <= b & 0 < r &
  (for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
  holds
  for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
   holds ||. iter(Fredholm(G,a,b,y0),(m+1)).u
              - iter(Fredholm(G,a,b,y0),(m+1)).v .||
                     <= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.||;

theorem :: ORDEQ_01:52
  a<b & G is_Lipschitzian_on the carrier of REAL-NS n implies
    ex m be Nat st iter(Fredholm(G,a,b,y0),(m+1)) is contraction;

theorem :: ORDEQ_01:53
  a<b & G is_Lipschitzian_on the carrier of REAL-NS n implies
  Fredholm(G,a,b,y0) is with_unique_fixpoint;

theorem :: ORDEQ_01:54
  for f,g be continuous PartFunc of REAL,REAL-NS n
    st dom f =[' a,b '] & dom g =[' a,b '] & Z = ]. a,b .[
     & a<b
     & G is_Lipschitzian_on the carrier of REAL-NS n
     & g=Fredholm(G,a,b,y0).f holds g/.a=y0
      & g is_differentiable_on Z
      & for t be Real st t in Z holds diff(g,t) = (G*f)/.t;

theorem :: ORDEQ_01:55
  for y be continuous PartFunc of REAL,REAL-NS n st a<b
     & Z = ]. a,b .[
     & G is_Lipschitzian_on the carrier of REAL-NS n
     & dom y = [' a,b ']
     & y is_differentiable_on Z
     & y/.a = y0
     & (for t be Real st t in Z holds diff(y,t) = G.(y/.t))
   holds y is_a_fixpoint_of (Fredholm(G,a,b,y0));

theorem :: ORDEQ_01:56
  for y1,y2 be continuous PartFunc of REAL,REAL-NS n
    st a<b & Z = ]. a,b .[ & G is_Lipschitzian_on the carrier of REAL-NS n
     & dom y1 = [' a,b ']
     & y1 is_differentiable_on Z
     & y1/.a = y0
     & (for t be Real st t in Z holds diff(y1,t) = G.(y1/.t))
     & dom y2 = [' a,b ']
     & y2 is_differentiable_on Z
     & y2/.a = y0
     & (for t be Real st t in Z holds diff(y2,t) = G.(y2/.t))
     holds y1=y2;

theorem :: ORDEQ_01:57
  a<b & Z = ]. a,b .[ & G is_Lipschitzian_on the carrier of REAL-NS n implies
   ex y be continuous PartFunc of REAL,REAL-NS n st
      dom y = [' a,b ']
    & y is_differentiable_on Z
    & y/.a = y0
    & for t be Real st t in Z holds diff(y,t) = G.(y/.t);