:: Functional Space Consisted by Continuous Functions on Topological Space
::  by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
:: 
:: Received March 30, 2021
:: Copyright (c) 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 STRUCT_0, FUNCOP_1, NUMBERS, VALUED_0, PRE_TOPC, ORDINAL2,
      SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3,
      ARYTM_1, COMPLEX1, CONNSP_2, RLVECT_1, ALGSTR_0, FUNCSDOM, REAL_1,
      FUNCT_2, VALUED_1, RSSPACE, BINOP_1, SUPINF_2, REALSET1, ZFMISC_1,
      RSSPACE4, XXREAL_2, XXREAL_0, NORMSP_1, NORMSP_2, REWRITE1, NAT_1,
      MONOID_0, NORMSP_0, FRECHET, RSSPACE3, SEQ_2, TMAP_1, ORDEQ_01, PARTFUN1,
      SEQFUNC, C0SP2, LOPBAN_1, METRIC_1, RELAT_2, PRE_POLY, RLSUB_1, RLTOPSP1,
      SETFAM_1, FINSET_1, FCONT_1, CFCONT_1, SEQ_4, C0SP3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1,
      REALSET1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1,
      XXREAL_2, VALUED_0, SEQ_2, SEQ_4, RCOMP_1, SEQFUNC, STRUCT_0, ALGSTR_0,
      PRE_POLY, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, NFCONT_1, PRE_TOPC,
      TOPS_2, COMPTS_1, FRECHET, FRECHET2, VFUNCT_1, CONNSP_2, RUSUB_4, TMAP_1,
      CONVEX1, RLTOPSP1, RSSPACE, RSSPACE3, LOPBAN_1, NORMSP_2, MONOID_0,
      RSSPACE4, SEQFUNC2;
 constructors REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, C0SP1, FRECHET, FRECHET2,
      NFCONT_1, SEQFUNC, MEASURE6, TOPMETR, SEQ_4, COMPTS_1, COMSEQ_2,
      NORMSP_2, VFUNCT_1, TMAP_1, RUSUB_4, CONVEX1, TOPS_2, MONOID_0, RSSPACE4,
      PRE_POLY, SEQFUNC2;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
      NUMBERS, ORDINAL1, VALUED_0, PSCOMP_1, XXREAL_0, FUNCT_2, XXREAL_2,
      RELSET_1, WAYBEL_2, VFUNCT_1, NORMSP_0, NORMSP_1, NORMSP_2, RLVECT_1,
      RLTOPSP1, BORSUK_1, MONOID_0, RSSPACE4;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin :: Real Vector Space of Continuous Functions

 reserve
  S for non empty TopSpace,
  T for LinearTopSpace,
  X for non empty Subset of the carrier of S;

theorem :: C0SP3:1
for X be non empty TopSpace, S be non empty LinearTopSpace,
    f,g be Function of X,S,
    x be Point of X
  st f is_continuous_at x & g is_continuous_at x
holds f+g is_continuous_at x;

theorem :: C0SP3:2
for X be non empty TopSpace, S be non empty LinearTopSpace,
    f be Function of X,S,
    x be Point of X,
    a be Real
  st f is_continuous_at x
holds a(#)f is_continuous_at x;

theorem :: C0SP3:3
for X be non empty TopSpace, S be non empty LinearTopSpace,
     f,g be Function of X,S
  st f is continuous & g is continuous
holds f+g is continuous;

theorem :: C0SP3:4
  for X be non empty TopSpace, S be non empty LinearTopSpace,
      f be Function of X,S,
      a be Real
  st f is continuous
    holds a(#)f is continuous;

definition
  let S be non empty TopSpace, T be non empty LinearTopSpace;
  func ContinuousFunctions(S,T) -> Subset of
    RealVectSpace(the carrier of S,T) equals
:: C0SP3:def 1
  { f where f is Function of the carrier of S,
      the carrier of T :f is continuous };
end;

registration
  let S be non empty TopSpace, T be non empty LinearTopSpace;
  cluster ContinuousFunctions(S,T) -> non empty functional;
end;

theorem :: C0SP3:5
  for S be non empty TopSpace, T be non empty LinearTopSpace
    holds ContinuousFunctions(S,T) is linearly-closed;

theorem :: C0SP3:6
for S be non empty TopSpace, T be non empty LinearTopSpace
  holds RLSStruct
(# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#) is Subspace of RealVectSpace(the carrier of S,T);

registration
  let S be non empty TopSpace, T be non empty LinearTopSpace;
  cluster RLSStruct (# ContinuousFunctions(S,T),
    Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
    Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
    Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
    #) -> Abelian add-associative right_zeroed right_complementable
      vector-distributive scalar-distributive scalar-associative
        scalar-unital;
end;

definition
  let S be non empty TopSpace, T be non empty LinearTopSpace;
  func R_VectorSpace_of_ContinuousFunctions(S,T) -> strict RealLinearSpace
    equals
:: C0SP3:def 2
  RLSStruct (# ContinuousFunctions(S,T),
    Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
    Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
    Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
   #);
end;

registration
  let S be non empty TopSpace, T be non empty LinearTopSpace;
  cluster R_VectorSpace_of_ContinuousFunctions(S,T) -> constituted-Functions;
end;

definition
  let S be non empty TopSpace, T be non empty LinearTopSpace,
      f be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
  let v be Element of S;
  redefine func f .v -> VECTOR of T;
end;

theorem :: C0SP3:7
  for S be non empty TopSpace, T be non empty LinearTopSpace
  for f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
  holds h = f+g iff
    for x be Element of S holds h.x = f.x + g.x;

theorem :: C0SP3:8
  for S be non empty TopSpace, T be non empty LinearTopSpace
  for f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
  for a be Real holds h = a*f iff for x be Element of S holds h.x = a * f.x;

theorem :: C0SP3:9
  for S be non empty TopSpace, T be non empty LinearTopSpace
    holds 0. R_VectorSpace_of_ContinuousFunctions(S,T)
      = (the carrier of S) --> 0.T;

registration
  let S be non empty TopSpace, T be non empty LinearTopSpace;
  cluster the carrier of R_VectorSpace_of_ContinuousFunctions(S,T) ->
    functional;
end;

::::::::::::Norm Space version::::::::::::::::::::::::::::

begin :: Real Vector Space of Continuous Functions

 reserve
    S,T for RealNormSpace,
    X for non empty Subset of the carrier of S;

theorem :: C0SP3:10
  for x being Point of T holds
    (the carrier of S) --> x is_continuous_on the carrier of S;

definition
  let S,T be RealNormSpace;
  func ContinuousFunctions(S,T) -> Subset of
    RealVectSpace(the carrier of S,T) equals
:: C0SP3:def 3
  { f where f is Function of the carrier of S,
      the carrier of T :f is_continuous_on the carrier of S };
end;

registration
  let S,T be RealNormSpace;
  cluster ContinuousFunctions(S,T) -> non empty functional;
end;

theorem :: C0SP3:11
  for S,T be RealNormSpace
    holds ContinuousFunctions(S,T) is linearly-closed;

theorem :: C0SP3:12
  for S,T be RealNormSpace holds RLSStruct (# ContinuousFunctions(S,T),
    Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
    Add_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
    Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
      #) is Subspace of RealVectSpace(the carrier of S,T);

registration
  let S,T be RealNormSpace;
  cluster RLSStruct (# ContinuousFunctions(S,T),
  Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
  Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
  Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
    #) -> Abelian add-associative right_zeroed right_complementable
  vector-distributive scalar-distributive scalar-associative scalar-unital;
end;

definition
  let S,T be RealNormSpace;
  func R_VectorSpace_of_ContinuousFunctions(S,T) ->
    strict RealLinearSpace equals
:: C0SP3:def 4
  RLSStruct (# ContinuousFunctions(S,T),
  Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
  Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
  Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
  #);
end;

registration
  let S,T be RealNormSpace;
  cluster R_VectorSpace_of_ContinuousFunctions(S,T) -> constituted-Functions;
end;

definition
  let S,T be RealNormSpace,
    f be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
  let v be Element of S;
  redefine func f .v -> VECTOR of T;
end;

theorem :: C0SP3:13
  for S,T be RealNormSpace
    for f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
  holds h = f+g iff for x be Element of S holds h.x = f.x + g.x;

theorem :: C0SP3:14
  for S,T be RealNormSpace
  for f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
  for a be Real holds h = a*f iff for x be Element of S holds h.x = a * f.x;

theorem :: C0SP3:15
  for S,T be RealNormSpace holds
    R_VectorSpace_of_ContinuousFunctions(S,T)
  is Subspace of RealVectSpace(the carrier of S,T);

theorem :: C0SP3:16
  for S,T be RealNormSpace
  holds 0. R_VectorSpace_of_ContinuousFunctions(S,T)
    = (the carrier of S) --> 0.T;

definition
  let S,T be RealNormSpace;
  let f be object such that
 f in ContinuousFunctions(S,T);
  func modetrans(f,S,T) -> Function of S,T means
:: C0SP3:def 5
  it = f & it is_continuous_on the carrier of S;
end;

begin :: Normed Topological Linear Space

definition
  struct(RLTopStruct,NORMSTR) RLNormTopStruct
    (# carrier -> set, ZeroF -> Element of the carrier,
          addF -> BinOp of the carrier,
          Mult -> Function of [:REAL, the carrier:],the carrier,
      topology -> Subset-Family of the carrier,
         normF -> Function of the carrier,REAL #);
end;

registration
  let X be non empty set, O be Element of X,
      F be BinOp of X, G be Function of [:REAL,X:],X,
      T be Subset-Family of X,
      N be Function of X,REAL;
  cluster RLNormTopStruct (# X,O,F,G,T,N #) -> non empty;
end;

registration
  cluster strict non empty for RLNormTopStruct;
end;

definition
  let X be non empty RLNormTopStruct;
  attr X is norm-generated means
:: C0SP3:def 6
  ex RNS be RealNormSpace
  st RNS = the NORMSTR of X
     & the topology of X = the topology of TopSpaceNorm RNS;
end;

registration
  cluster strict add-continuous Mult-continuous TopSpace-like Abelian
    add-associative right_zeroed right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital
    discerning reflexive RealNormSpace-like
     norm-generated T_2 for non empty RLNormTopStruct;
end;

definition
  mode NormedLinearTopSpace is strict add-continuous
    Mult-continuous TopSpace-like Abelian add-associative right_zeroed
    right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital
   discerning reflexive RealNormSpace-like norm-generated
     T_2 non empty RLNormTopStruct;
end;

theorem :: C0SP3:17
  for X be NormedLinearTopSpace holds X is LinearTopSpace;

theorem :: C0SP3:18
  for X be NormedLinearTopSpace holds X is RealNormSpace;

theorem :: C0SP3:19
for X being NormedLinearTopSpace,
    RNS being RealNormSpace
  st RNS = the NORMSTR of X
for x,y be Point of X,
    x1,y1 be Point of RNS,
    a be Real
    st x1=x & y1=y
holds
   x+y = x1+y1
   &
   a*x = a*x1
   &
   x-y = x1-y1
   &
   ||.x.|| = ||.x1.||;

theorem :: C0SP3:20
for X being NormedLinearTopSpace,
    S being sequence of X,
    x being Point of X holds
 S is_convergent_to x
iff for r being Real st 0 < r holds
  ex m being Nat st
  for n being Nat st m <= n holds
    ||.((S . n) - x).|| < r;

theorem :: C0SP3:21
for X being NormedLinearTopSpace,
    S being sequence of X,
    x being Point of X holds
 S is convergent & x=lim S
iff
for r being Real st 0 < r holds
  ex m being Nat st
  for n being Nat st m <= n holds
    ||.((S . n) - x).|| < r;

theorem :: C0SP3:22
for X being NormedLinearTopSpace,
    S being sequence of X
 st S is convergent
holds
  for r being Real st 0 < r holds
  ex m being Nat st
  for n being Nat st m <= n holds
    ||.(S . n) - (lim S) .|| < r;

theorem :: C0SP3:23
for X being NormedLinearTopSpace,
    V being Subset of X holds
 V is open iff for x being Point of X st x in V holds
                 ex r being Real st
 r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V;

theorem :: C0SP3:24
for X being NormedLinearTopSpace
for x being Point of X
for r being Real
for V being Subset of X
   st V = { y where y is Point of X : ||.(x - y).|| < r } holds V is open;

theorem :: C0SP3:25
for X being NormedLinearTopSpace
for x being Point of X
for r being Real
for V being Subset of X
st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed;

theorem :: C0SP3:26
for X being NormedLinearTopSpace,
    RNS being RealNormSpace,
    t being sequence of X,
    s being sequence of RNS
st RNS = the NORMSTR of X & t=s
   & t is convergent
 holds s is convergent & lim s = lim t;

theorem :: C0SP3:27
for X being NormedLinearTopSpace,
    RNS being RealNormSpace,
    s being sequence of X,
    t being sequence of RNS
st RNS = the NORMSTR of X & s=t
 holds
 s is convergent
   iff
 t is convergent;

theorem :: C0SP3:28
for X being NormedLinearTopSpace,
    V being Subset of X
holds
V is closed iff
for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
   lim s1 in V;

theorem :: C0SP3:29
for X being NormedLinearTopSpace,
    RNS be RealNormSpace,
    V being Subset of X,
    W being Subset of RNS st
  RNS = the NORMSTR of X
  & the topology of X = the topology of (TopSpaceNorm RNS)
  & V = W
holds
V is closed iff W is closed;

theorem :: C0SP3:30
for X being NormedLinearTopSpace,
    V be Subset of X,
    x being Point of X
holds
( V is a_neighborhood of x
  iff
 ( ex r being Real st
  r > 0 & { y where y is Point of X : ||.y-x.|| < r } c= V ));

theorem :: C0SP3:31
for X being NormedLinearTopSpace,
    V being Subset of X holds
V is compact iff
for s1 being sequence of X st rng s1 c= V holds
ex s2 being sequence of X st
   s2 is subsequence of s1
 & s2 is convergent & lim s2 in V;

theorem :: C0SP3:32
for X being NormedLinearTopSpace,
   RNS be RealNormSpace,
   V being Subset of X,
   W being Subset of RNS st
  RNS = the NORMSTR of X
  & the topology of X = the topology of TopSpaceNorm RNS
  & V = W
holds
V is compact iff W is compact;

begin :: Real Norm Space of Continuous Functions

theorem :: C0SP3:33
for X, X1 being set
for S being RealNormSpace
for f being PartFunc of S,REAL
st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1;

theorem :: C0SP3:34
  for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
  for x being set st x in ContinuousFunctions(S,T) holds
  x in BoundedFunctions (the carrier of S,T);

theorem :: C0SP3:35
  for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
  (R_VectorSpace_of_ContinuousFunctions(S,T) is
    Subspace of R_VectorSpace_of_BoundedFunctions(the carrier of S,T));

definition
  let S be non empty compact TopSpace,T be NormedLinearTopSpace;
  func ContinuousFunctionsNorm(S,T) ->
    Function of (ContinuousFunctions(S,T)),REAL
    equals
:: C0SP3:def 7
  (BoundedFunctionsNorm(the carrier of S,T)) | (ContinuousFunctions(S,T));
end;

definition
  let S be non empty compact TopSpace,T be NormedLinearTopSpace;
  func R_NormSpace_of_ContinuousFunctions(S,T) -> strict NORMSTR equals
:: C0SP3:def 8
    NORMSTR (# ContinuousFunctions(S,T),
    Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
     Add_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
      Mult_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
      ContinuousFunctionsNorm(S,T) #);
end;

registration
  let S be non empty compact TopSpace,T be NormedLinearTopSpace;
  cluster R_NormSpace_of_ContinuousFunctions(S,T) -> non empty;
end;

theorem :: C0SP3:36
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for x be Point of R_NormSpace_of_ContinuousFunctions(S,T),
  y be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
    st x=y holds ||.x.||= ||.y.||;

theorem :: C0SP3:37
 for S be non empty compact TopSpace,
     T be NormedLinearTopSpace,
      f be Point of R_NormSpace_of_ContinuousFunctions(S,T),
      g be Function of S,T
   st f=g holds
  for t be Point of S holds ||.g.t.|| <= ||.f.||;

theorem :: C0SP3:38
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
  y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
  st x1=y1 & x2=y2 holds x1+x2=y1+y2;

theorem :: C0SP3:39
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for a be Real,
       x be Point of R_NormSpace_of_ContinuousFunctions(S,T),
  y be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
    st x=y holds a*x=a*y;

registration
  let S be non empty compact TopSpace,T be NormedLinearTopSpace;
  cluster R_NormSpace_of_ContinuousFunctions(S,T) -> non empty
    right_complementable Abelian add-associative right_zeroed
    vector-distributive scalar-distributive scalar-associative scalar-unital;
end;

theorem :: C0SP3:40
  for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
  (the carrier of S) --> 0.T = 0.R_NormSpace_of_ContinuousFunctions(S,T);

theorem :: C0SP3:41
  for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
  0.R_NormSpace_of_ContinuousFunctions(S,T)
    = 0.R_NormSpace_of_BoundedFunctions(the carrier of S,T);

theorem :: C0SP3:42
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for F be Point of R_NormSpace_of_ContinuousFunctions(S,T)
    holds 0 <= ||.F.||;

theorem :: C0SP3:43
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for F be Point of R_NormSpace_of_ContinuousFunctions(S,T) holds
  F = 0.R_NormSpace_of_ContinuousFunctions(S,T) implies 0 = ||.F.||;

theorem :: C0SP3:44
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for F,G,H being Point of R_NormSpace_of_ContinuousFunctions(S,T)
  for f,g,h be Function of S,T holds
  (f=F & g=G & h=H implies
  (H = F+G iff for x be Element of S holds h.x = f.x + g.x));

theorem :: C0SP3:45
  for a be Real
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for F,G being Point of R_NormSpace_of_ContinuousFunctions(S,T)
  for f,g being Function of S,T holds
  (f=F & g=G implies ( G = a*F iff for x be Element of S holds g.x = a*f.x ));

theorem :: C0SP3:46
  for a being Real
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for F,G being Point of R_NormSpace_of_ContinuousFunctions(S,T) holds
( ||.F.|| = 0 iff F = 0.R_NormSpace_of_ContinuousFunctions(S,T)) &
(||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||);

registration
  let S be non empty compact TopSpace,T be NormedLinearTopSpace;
  cluster R_NormSpace_of_ContinuousFunctions(S,T)
    -> reflexive discerning RealNormSpace-like;
end;

theorem :: C0SP3:47
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
  y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
    st x1=y1 & x2=y2 holds x1-x2=y1-y2;

theorem :: C0SP3:48
  for S be non empty compact TopSpace,T be NormedLinearTopSpace
  for F,G,H be Point of R_NormSpace_of_ContinuousFunctions(S,T)
  for f,g,h be Function of S,T holds
  f=F & g=G & h=H implies
  (H = F-G iff (for x be Element of S holds h.x = f.x - g.x));

theorem :: C0SP3:49
  for S be non empty TopSpace,T be NormedLinearTopSpace,
      H be Functional_Sequence of the carrier of S,the carrier of T,
      LimH be Function of S,T
    st H is_unif_conv_on (the carrier of S)
      &
       ( for n be Nat holds
         ex Hn be Function of S,T st Hn = H.n & Hn is continuous )
     & LimH = lim(H,the carrier of S)
  holds LimH is continuous;

theorem :: C0SP3:50
  for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
  for Y be Subset of the carrier of
         R_NormSpace_of_BoundedFunctions(the carrier of S,T) st
  Y = ContinuousFunctions(S,T) holds Y is closed;

theorem :: C0SP3:51
  for S be non empty compact TopSpace,
      T be NormedLinearTopSpace st T is complete holds
  for seq be sequence of R_NormSpace_of_ContinuousFunctions(S,T)
   st seq is Cauchy_sequence_by_Norm holds seq is convergent;

theorem :: C0SP3:52
  for S be non empty compact TopSpace,
      T be NormedLinearTopSpace st T is complete holds
   R_NormSpace_of_ContinuousFunctions(S,T) is complete;

begin :: Some Properties of Support

definition
  let X be ZeroStr;
  let f be (the carrier of X)-valued Function;
  func support f -> set means
:: C0SP3:def 9
  for x being object holds
  x in it iff x in dom f & f /. x <> 0.X;
end;

theorem :: C0SP3:53
  for X be ZeroStr,
  f be (the carrier of X)-valued Function
    holds support f c= dom f;

definition
  let X be non empty TopSpace, T be RealLinearSpace;
  let f be Function of X,T;
  redefine func support f -> Subset of X;
end;

theorem :: C0SP3:54
  for X be non empty TopSpace, T be RealLinearSpace
  for f,g be Function of X,T holds
    support(f+g) c= support(f) \/ support(g);

theorem :: C0SP3:55
  for X be non empty TopSpace,T be RealLinearSpace,
      f be Function of X,T,
      a be Real holds
    support(a(#)f) c= support(f);

begin :: Space of Real-valued Continuous Functionals with Bounded Support

definition
  let X be non empty TopSpace, T be NormedLinearTopSpace;
  func C_0_Functions(X,T) -> non empty Subset of
     RealVectSpace(the carrier of X,T) equals
:: C0SP3:def 10
  { f where f is Function of the carrier of X, the carrier of T :
  f is continuous & ex Y be non empty Subset of X st Y is compact
  & Cl support f c= Y };
end;

theorem :: C0SP3:56
  for X be non empty TopSpace,T be NormedLinearTopSpace
  for v,u be Element of RealVectSpace(the carrier of X,T)
     st v in C_0_Functions(X,T) & u in C_0_Functions(X,T)
                   holds v + u in C_0_Functions(X,T);

theorem :: C0SP3:57
  for X be non empty TopSpace,T be NormedLinearTopSpace
  for a be Real,u be Element of RealVectSpace(the carrier of X,T)
     st u in C_0_Functions(X,T) holds a * u in C_0_Functions(X,T);

theorem :: C0SP3:58
  for X be non empty TopSpace,T be NormedLinearTopSpace holds
  C_0_Functions(X,T) is linearly-closed;

registration
  let X be non empty TopSpace,T be NormedLinearTopSpace;
  cluster C_0_Functions(X,T) -> non empty linearly-closed;
end;

definition
  let X be non empty TopSpace,T be NormedLinearTopSpace;
  func R_VectorSpace_of_C_0_Functions(X,T) -> RealLinearSpace equals
:: C0SP3:def 11
  RLSStruct (# C_0_Functions(X,T),
  Zero_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
  Add_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
  Mult_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)) #);
end;

theorem :: C0SP3:59
  for X be non empty TopSpace,T be NormedLinearTopSpace holds
  R_VectorSpace_of_C_0_Functions(X,T)
  is Subspace of RealVectSpace(the carrier of X,T);

theorem :: C0SP3:60
  for X be non empty TopSpace,T be NormedLinearTopSpace
  for x being set st x in C_0_Functions(X,T) holds
  x in BoundedFunctions(the carrier of X,T);

definition
  let X be non empty TopSpace, T be NormedLinearTopSpace;
  func C_0_FunctionsNorm(X,T) -> Function of (C_0_Functions(X,T)),REAL equals
:: C0SP3:def 12
  (BoundedFunctionsNorm(the carrier of X,T)) | (C_0_Functions(X,T));
end;

definition
  let X be non empty TopSpace,T be NormedLinearTopSpace;
  func R_Normed_Space_of_C_0_Functions (X,T) -> NORMSTR equals
:: C0SP3:def 13
  NORMSTR (# C_0_Functions(X,T),
  Zero_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
  Add_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
  Mult_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
        C_0_FunctionsNorm(X,T) #);
end;

registration
  let X be non empty TopSpace,T be NormedLinearTopSpace;
  cluster R_Normed_Space_of_C_0_Functions (X,T) -> strict non empty;
end;

theorem :: C0SP3:61
  for X be non empty TopSpace, T be NormedLinearTopSpace
  for x being set st x in C_0_Functions(X,T) holds
  x in ContinuousFunctions(X,T);

theorem :: C0SP3:62
  for X be non empty TopSpace, T be NormedLinearTopSpace holds
  0.R_VectorSpace_of_C_0_Functions(X,T) = X -->0.T;

theorem :: C0SP3:63
  for X be non empty TopSpace,T be NormedLinearTopSpace holds
  0.R_Normed_Space_of_C_0_Functions (X,T) = X --> 0.T;

theorem :: C0SP3:64
  for X be non empty TopSpace,T be NormedLinearTopSpace
  for x1,x2 be Point of R_Normed_Space_of_C_0_Functions (X,T),
  y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T)
                    st x1=y1 & x2=y2 holds x1+x2=y1+y2;

theorem :: C0SP3:65
  for X be non empty TopSpace,T be NormedLinearTopSpace
  for a be Real,x be Point of R_Normed_Space_of_C_0_Functions (X,T),
  y be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T)
                     st x=y holds a*x=a*y;

theorem :: C0SP3:66
  for a be Real
  for X be non empty TopSpace,T be NormedLinearTopSpace
  for F,G be Point of R_Normed_Space_of_C_0_Functions (X,T) holds
  (||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions (X,T) ) &
  ||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||;

theorem :: C0SP3:67
  for X be non empty TopSpace,T be NormedLinearTopSpace holds
  R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace-like;

registration
  let X be non empty TopSpace,T be NormedLinearTopSpace;
  cluster R_Normed_Space_of_C_0_Functions (X,T) ->
  reflexive discerning RealNormSpace-like
  vector-distributive scalar-distributive scalar-associative scalar-unital
  Abelian add-associative right_zeroed right_complementable;
end;

theorem :: C0SP3:68
  for X be non empty TopSpace,T be NormedLinearTopSpace holds
    R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace;