:: Banach Algebra of Continuous Functionals
::  by Kanazashi Katuhiko , Noboru Endou and Yasunari Shidama
::
:: Received October 20, 2009
:: Copyright (c) 2009 Association of Mizar Users

environ

 vocabularies STRUCT_0, XREAL_0, ORDINAL1, FUNCOP_1, PSCOMP_1, NUMBERS,
      PRE_TOPC, ORDINAL2, SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1,
      TARSKI, CARD_1, ARYTM_3, XXREAL_1, ARYTM_1, COMPLEX1, CONNSP_2, RLVECT_1,
      ALGSTR_0, FUNCSDOM, REAL_1, FUNCT_2, C0SP1, IDEAL_1, VALUED_1, MESFUNC1,
      RSSPACE, POLYALG1, BINOP_1, VECTSP_1, SUPINF_2, GROUP_1, REALSET1,
      ZFMISC_1, RSSPACE4, XXREAL_2, XXREAL_0, LOPBAN_2, NORMSP_1, REWRITE1,
      NAT_1, RSSPACE3, SEQ_2, PARTFUN1, SEQFUNC, C0SP2, LOPBAN_1, METRIC_1,
      RELAT_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
      XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, REALSET1, FUNCT_1,
      FUNCT_2, STRUCT_0, ALGSTR_0, IDEAL_1, BINOP_1, DOMAIN_1, RELSET_1,
      PRE_TOPC, COMPTS_1, PSCOMP_1, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
      PARTFUN1, SEQFUNC, RSSPACE3, RCOMP_1, SEQ_2, NORMSP_0, NORMSP_1,
      NFCONT_1, LOPBAN_1, LOPBAN_2, C0SP1, CONNSP_2, FUNCOP_1, PARTFUN3;
 constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, IDEAL_1, COMPTS_1,
      SEQ_1, C0SP1, NFCONT_1, SEQFUNC, JORDAN_A, PARTFUN3, BINOP_2, SEQ_2,
      MEASURE6;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
      ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, RELAT_1, VECTSP_1,
      VECTSP_2, VALUED_0, LOPBAN_2, PSCOMP_1, RCOMP_1, C0SP1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions PSCOMP_1, REALSET1, ALGSTR_0, TARSKI, XCMPLX_0, NORMSP_1, RCOMP_1,
      FUNCSDOM, RLVECT_1, VECTSP_1, STRUCT_0, GROUP_1, BINOP_1, C0SP1,
      NORMSP_0;
 theorems RFUNCT_1, FUNCT_1, NFCONT_1, PARTFUN1, SEQ_2, ABSVALUE, ALGSTR_0,
      COMPLEX1, ZFMISC_1, TARSKI, RCOMP_1, XBOOLE_1, PSCOMP_1, IDEAL_1,
      RSSPACE3, RELAT_1, XREAL_0, XXREAL_0, FUNCSDOM, NORMSP_1, LOPBAN_1,
      FUNCT_2, XREAL_1, RLVECT_1, TOPS_1, FUNCOP_1, VECTSP_1, GROUP_1,
      LOPBAN_2, VALUED_1, C0SP1, CONNSP_2, XXREAL_1, NORMSP_0;

begin

definition
  let X be 1-sorted, y be real number;
  func X --> y -> RealMap of X equals
  (the carrier of X) --> y;
  coherence
  proof
    y in REAL by XREAL_0:def 1; then
    (the carrier of X) --> y is RealMap of X by FUNCOP_1:57;
    hence thesis;
  end;
end;

registration
  let X be TopSpace, y be real number;
  cluster X --> y -> continuous;
  coherence
  proof
   set f = X --> y;
   set HX=[#] X;
   let P1 being Subset of REAL such that P1 is closed;
   per cases;
   suppose y in P1;
    then f"P1 = HX by FUNCOP_1:20;
    hence f"P1 is closed;
   end;
   suppose not y in P1;
    then f"P1 = {}X by FUNCOP_1:22;
    hence f"P1 is closed;
   end;
 end;
end;

theorem Th1:
for X being non empty TopSpace, f be RealMap of X holds f is continuous iff
   for x being Point of X,V being Subset of REAL st
    f.x in V & V is open holds
     ex W being Subset of X st x in W & W is open & f.:W c= V
proof
   let X be non empty TopSpace,f be RealMap of X;
   hereby assume A1: f is continuous;
    now let x be Point of X,V being Subset of REAL;
     set r = f.x;
     assume r in V & V is open; then
     consider r0 be real number such that
A2: 0<r0 & ].r-r0,r+r0.[ c= V by RCOMP_1:40;
     set S = ]. r-r0,r+r0 .[;
     take W= f"S;
     abs(r-r) < r0 by A2,COMPLEX1:130; then
     r in S by RCOMP_1:8;
     hence x in W by FUNCT_2:46;
     thus W is open by A1,PSCOMP_1:54;
     f.:(f"S) c= S by FUNCT_1:145;
     hence f.:W c= V by A2,XBOOLE_1:1;
    end;
    hence for x being Point of X,V being Subset of REAL st
      f.x in V & V is open holds
       ex W being Subset of X st x in W & W is open & f.:W c= V;
   end;
   assume
A3: for x being Point of X,V being Subset of REAL st f.x in V & V is open holds
      ex W being Subset of X st x in W & W is open & f.:W c= V;
   now let Y be Subset of REAL;
    assume Y is closed; then
    Y`` is closed; then
A4: Y` is open by RCOMP_1:def 5;
    for x being Point of X st x in (f"Y)` ex W being Subset of X st
     W is a_neighborhood of x & W c= (f"Y)`
    proof
     let x be Point of X;
     assume x in (f"Y)`; then
     x in f"Y` by FUNCT_2:177; then
     f.x in Y` by FUNCT_2:46; then
     consider V being Subset of REAL such that
A5:   f.x in V & V is open & V c= Y` by A4;
     consider W being Subset of X such that
A6:   x in W & W is open & f.:W c= V by A3,A5;
     take W;
     thus W is a_neighborhood of x by A6,CONNSP_2:5;
     f.:W c= Y` by A5,A6,XBOOLE_1:1; then
A7:  f"(f.:W) c= f"Y` by RELAT_1:178;
     W c= f"(f.:W) by FUNCT_2:50; then
     W c= f"Y` by A7,XBOOLE_1:1;
     hence W c= (f"Y)` by FUNCT_2:177;
    end; then
    (f"Y)` is open by CONNSP_2:9; then
    (f"Y)`` is closed by TOPS_1:30;
    hence f"Y is closed;
   end;
   hence f is continuous by PSCOMP_1:def 25;
end;

reserve X for non empty TopSpace;

definition let X;
  func ContinuousFunctions(X) -> Subset of RAlgebra the carrier of X equals
  { f where f is continuous RealMap of X : not contradiction };
correctness
proof
  set A = { f where f is continuous RealMap of X : not contradiction };
  A c= Funcs(the carrier of X,REAL)
   proof
    let x be set;
    assume x in A;
    then ex f be continuous RealMap of X st x=f;
    hence x in Funcs(the carrier of X,REAL) by FUNCT_2:11;
   end;
   hence thesis;
 end;
end;

registration let X;
  cluster ContinuousFunctions(X) -> non empty;
  coherence
  proof
   X-->0 in { f where f is continuous RealMap of X : not contradiction };
   hence thesis;
 end;
end;

registration let X;
  cluster ContinuousFunctions X -> additively-linearly-closed
                                multiplicatively-closed;
  coherence
proof
   set W = ContinuousFunctions X;
   set V = RAlgebra the carrier of X;
A1:RAlgebra the carrier of X is RealLinearSpace by C0SP1:7;
   for v,u be Element of V st v in W & u in W holds v + u in W
   proof
    let v,u be Element of V such that
A2: v in W & u in W;
    consider v1 be continuous RealMap of X such that
A3:v1=v by A2;
    consider u1 be continuous RealMap of X such that
A4:u1=u by A2;
    reconsider h = v+u as Element of Funcs(the carrier of X,REAL);
A5:ex f being Function st
      h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
    dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1; then
A6: dom v1 /\ dom u1 = (the carrier of X) /\ (the carrier of X)
      by FUNCT_2:def 1;
    for x be set st x in dom h holds h.x = v1.x + u1.x
      by A3,A4,FUNCSDOM:10; then
    v+u=v1+u1 by A6,A5,VALUED_1:def 1;
    hence v+u in W;
   end; then
A7:W is add-closed by IDEAL_1:def 1;
   for v be Element of V st v in W holds -v in W
   proof
    let v be Element of V such that
A8: v in W;
    consider v1 be continuous RealMap of X such that
A9:v1=v by A8;
    reconsider h = -v, v2 = v as Element of Funcs(the carrier of X,REAL);
A10: h=(-1)*v by A1,RLVECT_1:29;
A11:ex f being Function st
      h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
A12: dom v1 =the carrier of X by FUNCT_2:def 1;
    now let x be set;
     assume x in dom h; then
     reconsider y=x as Element of the carrier of X;
     h.x = (-1)*(v2.y) by A10,FUNCSDOM:15;
     hence h.x = -v1.x by A9;
    end; then
    -v=-v1 by A12,A11,VALUED_1:9;
    hence -v in W;
   end; then
A13:W is having-inverse by C0SP1:def 1;
   for a be Real, u be Element of V st u in W holds a * u in W
   proof
    let a be Real, u be Element of V such that
A14: u in W;
    consider u1 be continuous RealMap of X such that
A15:u1=u by A14;
    reconsider h = a*u as Element of Funcs(the carrier of X,REAL);
A16:ex f being Function st
      h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
A17: dom u1 = the carrier of X by FUNCT_2:def 1;
    for x be set st x in dom h holds h.x = a*(u1.x) by A15,FUNCSDOM:15; then
    a*u=a(#)u1 by A17,A16,VALUED_1:def 5;
    hence a*u in W;
   end;
   hence ContinuousFunctions X is additively-linearly-closed
     by A7,A13,C0SP1:def 10;
A18:for v,u be Element of V st v in W & u in W holds v * u in W
   proof
    let v,u be Element of V such that
A19: v in W & u in W;
    consider v1 be continuous RealMap of X such that
A20:v1=v by A19;
    consider u1 be continuous RealMap of X such that
A21:u1=u by A19;
    reconsider h = v*u as Element of Funcs(the carrier of X,REAL);
A22:ex f being Function st
      h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
    dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1; then
A23: dom v1 /\ dom u1 = (the carrier of X) /\ (the carrier of X)
      by FUNCT_2:def 1;
    for x be set st x in dom h holds h.x = v1.x *u1.x
      by A20,A21,FUNCSDOM:11; then
    v*u=v1(#)u1 by A23,A22,VALUED_1:def 4;
    hence v*u in W;
   end;
   reconsider g = RealFuncUnit the carrier of X as RealMap of X;
   g = X --> 1; then
   1.V in W;
   hence thesis by A18,C0SP1:def 4;
 end;
end;

definition let X be non empty TopSpace;
  func R_Algebra_of_ContinuousFunctions X -> AlgebraStr equals
  AlgebraStr (# ContinuousFunctions X, mult_(ContinuousFunctions X,
  RAlgebra the carrier of X),
   Add_(ContinuousFunctions X,RAlgebra the carrier of X),
   Mult_(ContinuousFunctions X,RAlgebra the carrier of X),
   One_(ContinuousFunctions X,RAlgebra the carrier of X),
   Zero_(ContinuousFunctions X,RAlgebra the carrier of X)
  #);
  coherence;
end;

theorem
  R_Algebra_of_ContinuousFunctions X
   is Subalgebra of RAlgebra the carrier of X by C0SP1:6;

registration let X;
  cluster R_Algebra_of_ContinuousFunctions X -> strict non empty;
  coherence;
end;

registration let X;
  cluster R_Algebra_of_ContinuousFunctions X -> Abelian add-associative
    right_zeroed right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital
    commutative associative right_unital right-distributive
    vector-distributive scalar-distributive scalar-associative
    vector-associative;
  coherence
  proof
A1: R_Algebra_of_ContinuousFunctions X is Algebra by C0SP1:6;
   now let v be VECTOR of R_Algebra_of_ContinuousFunctions X;
    reconsider v1=v as VECTOR of RAlgebra the carrier of X by TARSKI:def 3;
    R_Algebra_of_ContinuousFunctions X
    is Subalgebra of RAlgebra the carrier of X by C0SP1:6; then
    1 * v = 1*v1 by C0SP1:8;
    hence 1 * v =v by FUNCSDOM:23;
   end;
   hence thesis by A1,RLVECT_1:def 11;
 end;
end;

reserve F,G,H for VECTOR of R_Algebra_of_ContinuousFunctions X;
reserve f,g,h for RealMap of X;
reserve a for Real;

theorem Th3:
f=F & g=G & h=H implies ( H = F+G iff (for x be Element of the carrier of X
  holds h.x = f.x + g.x) )
proof
   assume A1: f=F & g=G & h=H;
A2:R_Algebra_of_ContinuousFunctions X is
     Subalgebra of RAlgebra the carrier of X by C0SP1:6;
   reconsider f1=F, g1=G, h1=H as VECTOR of
   RAlgebra the carrier of X by TARSKI:def 3;
   hereby assume A3: H = F+G;
    let x be Element of the carrier of X;
    h1=f1+g1 by A2,A3,C0SP1:8;
    hence h.x = f.x+g.x by A1,FUNCSDOM:10;
   end;
   assume for x be Element of X holds h.x = f.x+g.x; then
   h1=f1+g1 by A1,FUNCSDOM:10;
   hence H =F+G by A2,C0SP1:8;
end;

theorem Th4:
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )
proof
   assume A1: f=F & g=G;
A2:R_Algebra_of_ContinuousFunctions X is
     Subalgebra of RAlgebra the carrier of X by C0SP1:6;
   reconsider f1=F, g1=G as VECTOR of
   RAlgebra the carrier of X by TARSKI:def 3;
   hereby assume A3: G = a*F;
    let x be Element of the carrier of X;
    g1=a*f1 by A2,A3,C0SP1:8;
    hence g.x=a*f.x by A1,FUNCSDOM:15;
   end;
   assume for x be Element of the carrier of X holds g.x=a*f.x; then
   g1=a*f1 by A1,FUNCSDOM:15;
   hence G =a*F by A2,C0SP1:8;
end;

theorem Th5:
f=F & g=G & h=H implies ( H = F*G iff (for x be Element of the carrier of X
  holds h.x = f.x * g.x) )
proof
   assume A1: f=F & g=G & h=H;
A2:R_Algebra_of_ContinuousFunctions X is
      Subalgebra of RAlgebra the carrier of X by C0SP1:6;
   reconsider f1=F, g1=G, h1=H as VECTOR of
   RAlgebra the carrier of X by TARSKI:def 3;
   hereby assume A3: H = F*G;
    let x be Element of the carrier of X;
    h1 = f1*g1 by A2,A3,C0SP1:8;
    hence h.x = f.x * g.x by A1,FUNCSDOM:11;
   end;
   assume for x be Element of X holds h.x = f.x * g.x; then
   h1 = f1 * g1 by A1,FUNCSDOM:11;
   hence H = F * G by A2,C0SP1:8;
end;

theorem Th6:
0.R_Algebra_of_ContinuousFunctions X = X --> 0
proof
A1:R_Algebra_of_ContinuousFunctions X
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
   0.RAlgebra  the carrier of X = X --> 0;
   hence thesis by A1,C0SP1:8;
end;

theorem Th7:
1_R_Algebra_of_ContinuousFunctions X = X --> 1
proof
A1:R_Algebra_of_ContinuousFunctions X
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
   1_RAlgebra the carrier of X = X --> 1;
   hence thesis by A1,C0SP1:8;
end;

reserve X for compact non empty TopSpace;

reserve f,g,h for RealMap of X;

theorem Th8:
for A being Algebra, A1,A2 being Subalgebra of A holds
  the carrier of A1 c= the carrier of A2 implies A1 is Subalgebra of A2
proof
   let A be Algebra, A1,A2 be Subalgebra of A;
   assume A1: the carrier of A1 c= the carrier of A2;
   set CA1 = the carrier of A1;
   set CA2 = the carrier of A2;
   set AA = the addF of A;
   set mA = the multF of A;
   set MA = the Mult of A;
A2:0.A1 = 0.A & 0.A2 = 0.A & 1.A1 = 1.A & 1.A2 = 1.A by C0SP1:def 9;
A3:the addF of A1 = (the addF of A2)||the carrier of A1
   proof
    the addF of A1 = AA||CA1 & the addF of A2 = AA||CA2 &
    [:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:119;
    hence thesis by FUNCT_1:82;
   end;
A4:the multF of A1 = (the multF of A2)||the carrier of A1
   proof
    the multF of A1 = mA||CA1 & the multF of A2 = mA||CA2 &
    [:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:119;
    hence thesis by FUNCT_1:82;
   end;
   the Mult of A1 = (the Mult of A2) | [:REAL,CA1:]
   proof
    the Mult of A1 = MA|[:REAL,CA1:] & the Mult of A2 = MA|[:REAL,CA2:] &
    [:REAL,CA1:] c= [:REAL,CA2:] by A1,C0SP1:def 9,ZFMISC_1:119;
    hence thesis by FUNCT_1:82;
   end;
   hence thesis by A1,A2,A3,A4,C0SP1:def 9;
end;

Lm1:
for x being set st x in ContinuousFunctions X holds
  x in BoundedFunctions the carrier of X
proof
   let x be set;
   assume x in ContinuousFunctions X; then
   consider h be continuous RealMap of X such that
A1: x=h;
A2:h is bounded_above & h is bounded_below by SEQ_2:def 8; then
   consider r1 being real number such that
A3: for y being set st y in dom h holds h.y < r1 by SEQ_2:def 1;
A4: (the carrier of X) /\ dom h c= dom h by XBOOLE_1:17; then
   for y being set st y in (the carrier of X) /\ dom h holds h.y<=r1
     by A3; then
A5: h|(the carrier of X) is bounded_above by RFUNCT_1:87;
   consider r2 being real number such that
A6: for y being set st y in dom h holds r2<h.y by A2,SEQ_2:def 2;
   for y being set st y in (the carrier of X) /\ dom h holds
     r2<=h.y by A4,A6; then
A7: h|(the carrier of X) is bounded_below by RFUNCT_1:88;
    (the carrier of X ) /\ (the carrier of X ) =(the carrier of X ); then
    h|(the carrier of X ) is bounded by A5,A7,RFUNCT_1:92;
    hence x in BoundedFunctions the carrier of X by A1;
end;

theorem
R_Algebra_of_ContinuousFunctions X is
  Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X
proof
A1:the carrier of R_Algebra_of_ContinuousFunctions X
     c= the carrier of R_Algebra_of_BoundedFunctions the carrier of X
   proof
    for x being set st x in ContinuousFunctions X holds
     x in BoundedFunctions the carrier of X by Lm1;
    hence thesis by TARSKI:def 3;
   end;
A2:R_Algebra_of_ContinuousFunctions X is
     Subalgebra of RAlgebra (the carrier of X) by C0SP1:6;
   R_Algebra_of_BoundedFunctions the carrier of X is
     Subalgebra of RAlgebra (the carrier of X) by C0SP1:10;
   hence thesis by A1,A2,Th8;
end;

definition let X;
  func ContinuousFunctionsNorm X -> Function of (ContinuousFunctions X),REAL
  equals
  (BoundedFunctionsNorm the carrier of X)|(ContinuousFunctions X);
correctness
proof
   for x being set st x in ContinuousFunctions X holds
     x in BoundedFunctions the carrier of X by Lm1; then
   ContinuousFunctions X c= BoundedFunctions the carrier of X by TARSKI:def 3;
   hence thesis by FUNCT_2:38;
end;
end;

definition let X;
 func R_Normed_Algebra_of_ContinuousFunctions X -> Normed_AlgebraStr equals
  Normed_AlgebraStr (# ContinuousFunctions X,
    mult_(ContinuousFunctions X,RAlgebra the carrier of X),
    Add_(ContinuousFunctions X,RAlgebra the carrier of X),
    Mult_(ContinuousFunctions X,RAlgebra the carrier of X),
    One_(ContinuousFunctions X,RAlgebra the carrier of X),
    Zero_(ContinuousFunctions X,RAlgebra the carrier of X),
    ContinuousFunctionsNorm X #);
correctness;
end;

registration let X;
  cluster R_Normed_Algebra_of_ContinuousFunctions X -> strict non empty;
  correctness;
end;

Lm2:
now let X;
   set F = R_Normed_Algebra_of_ContinuousFunctions X;
   let x,e be Element of F;
   assume
A1: e = One_(ContinuousFunctions X,RAlgebra the carrier of X);
   set X1 = ContinuousFunctions X;
   reconsider f = x as Element of X1;
   1_RAlgebra the carrier of X = X-->1
   .= 1_R_Algebra_of_ContinuousFunctions X by Th7; then
A2:[f,1_RAlgebra the carrier of X] in [:X1,X1:] &
   [1_RAlgebra the carrier of X,f] in [:X1,X1:] by ZFMISC_1:106;
   x * e = (mult_(X1,RAlgebra the carrier of X))
      .(f,1_RAlgebra the carrier of X) by A1,C0SP1:def 8; then
   x * e = ((the multF of RAlgebra the carrier of X)||X1)
        .(f,1_RAlgebra the carrier of X) by C0SP1:def 6; then
   x * e = f * 1_RAlgebra the carrier of X by A2,FUNCT_1:72;
   hence x * e = x by VECTSP_1:def 13;
   e * x = (mult_(X1,RAlgebra the carrier of X))
     .(1_RAlgebra the carrier of X,f) by A1,C0SP1:def 8; then
   e * x = ((the multF of RAlgebra the carrier of X)||X1)
       .(1_RAlgebra the carrier of X,f) by C0SP1:def 6; then
   e * x = (1_RAlgebra the carrier of X )* f by A2,FUNCT_1:72;
   hence e * x = x by VECTSP_1:def 13;
end;

registration let X;
  cluster R_Normed_Algebra_of_ContinuousFunctions X -> unital;
  correctness
  proof
    reconsider e = One_(ContinuousFunctions X, RAlgebra the carrier of X) as
    Element of R_Normed_Algebra_of_ContinuousFunctions X;
    take e;
    thus thesis by Lm2;
  end;
end;

theorem Th10:
for W be Normed_AlgebraStr, V be Algebra st
 the AlgebraStr of W = V holds W is Algebra
proof
   let W be Normed_AlgebraStr,V be Algebra such that
A1:the AlgebraStr of W = V;
   reconsider W as non empty AlgebraStr by A1;
A2:for x,y being VECTOR of W holds x + y = y + x
   proof
    let x,y be VECTOR of W;
    reconsider x1 = x, y1 = y as VECTOR of V by A1;
    x + y = x1+y1 by A1; then
    x + y =y1 + x1;
    hence x + y = y + x by A1;
   end;
A3:for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z)
   proof
    let x,y,z be VECTOR of W;
    reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1;
    (x + y) + z = (x1 + y1) + z1 by A1; then
    (x + y) + z = x1 + (y1 + z1) by RLVECT_1:def 6;
    hence (x + y) + z = x + (y + z) by A1;
   end;
A4:for x being VECTOR of W holds x + 0.W = x
   proof
    let x be VECTOR of W;
    reconsider y = x as VECTOR of V by A1;
    x + 0.W = y + 0.V by A1;
    hence x + 0.W = x by RLVECT_1:10;
   end;
A5:for x being Element of W holds x is right_complementable
   proof
    let x be Element of W;
    reconsider x1 = x as Element of V by A1;
    consider v be Element of V such that
A6:  x1 + v = 0.V by ALGSTR_0:def 11;
    reconsider y = v as Element of W by A1;
    x + y = 0.W by A6,A1;
    hence thesis by ALGSTR_0:def 11;
   end;
A7:for v,w being Element of W holds v * w = w * v
   proof
    let v,w be Element of W;
    reconsider v1 = v, w1 = w as Element of V by A1;
    v * w = v1*w1 by A1; then
    v * w = w1*v1;
    hence v * w =w*v by A1;
   end;
A8:for a,b,x being Element of W holds (a * b) * x = a * (b * x)
   proof
    let a,b,x be Element of W;
    reconsider y = x, a1 = a, b1 = b as Element of V by A1;
    (a * b) * x = (a1 * b1) * y by A1; then
    (a * b) * x = a1 * (b1 * y) by GROUP_1:def 4;
    hence (a * b) * x = a * (b * x) by A1;
   end;
A9:W is right_unital
   proof
    let x be Element of W;
    reconsider x1 = x as Element of V by A1;
    x*1.W = x1*1.V by A1;
    hence x*1.W = x by VECTSP_1:def 13;
   end;
A10:W is right-distributive
   proof
    let x,y,z being Element of W;
    reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;
    x*(y+z) = x1*(y1+z1) by A1; then
    x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 11;
    hence x*(y+z) = x*y + x*z by A1;
   end;
   W is vector-distributive scalar-distributive scalar-associative
   vector-associative
   proof
    thus W is vector-distributive
     proof
      let a be real number;
      let x,y being Element of W;
      reconsider x1 = x, y1 = y as Element of V by A1;
      a*(x+y) = a*(x1+y1) by A1; then
      a*(x+y) = a*x1 + a*y1 by RLVECT_1:def 8;
      hence a*(x+y) = a*x + a*y by A1;
     end;
    thus W is scalar-distributive
     proof
      let a,b be real number;
      let x being Element of W;
      reconsider x1 = x as Element of V by A1;
      (a+b)*x = (a+b)*x1 by A1; then
      (a+b)*x = a*x1 + b*x1 by RLVECT_1:def 9;
      hence (a+b)*x =a*x + b*x by A1;
     end;
    thus W is scalar-associative
     proof
      let a,b be real number;
      let x being Element of W;
      reconsider x1 = x as Element of V by A1;
      (a*b)*x = (a*b)*x1 by A1; then
      (a*b)*x = a*(b*x1) by RLVECT_1:def 10;
      hence (a*b)*x = a*(b*x) by A1;
     end;
    let x,y being Element of W;
    let a be Real;
    reconsider x1 = x, y1 = y as Element of V by A1;
    a*(x*y) = a*(x1*y1) by A1; then
    a*(x*y) = (a*x1)*y1 by FUNCSDOM:def 20;
    hence a*(x*y) = (a*x)*y by A1;
   end;
   hence thesis by A2,A3,A4,A5,A7,A8,A9,A10
,ALGSTR_0:def 16,GROUP_1:def 4,def 16
,RLVECT_1:def 5,def 6,def 7;
end;

reserve F,G,H for Point of R_Normed_Algebra_of_ContinuousFunctions X;

Lm3:
for x be Point of R_Normed_Algebra_of_ContinuousFunctions X,
 y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
  st x=y holds ||.x.||= ||.y.||
   by FUNCT_1:72;

Lm4:
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
 y1,y2  be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
  st x1=y1 & x2=y2 holds x1+x2=y1+y2
proof
   let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
       y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions
         the carrier of X;
   assume A1: x1=y1 & x2=y2;
   thus x1+x2 = ((the addF of RAlgebra the carrier of X)
         ||(ContinuousFunctions X)).([x1,x2]) by C0SP1:def 5
     .= (the addF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:72
     .= ((the addF of RAlgebra the carrier of X)
         ||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:72
     .=y1+y2 by C0SP1:def 5;
end;

Lm5:
for a be Real,x be Point of R_Normed_Algebra_of_ContinuousFunctions X,
  y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
  st x=y holds a*x=a*y
proof
   let a be Real, x be Point of R_Normed_Algebra_of_ContinuousFunctions X,
       y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
   assume A1: x=y;
   thus a*x = ((the Mult of RAlgebra the carrier of X)|
       [:REAL,(ContinuousFunctions X):]).([a,x]) by C0SP1:def 11
    .= (the Mult of RAlgebra the carrier of X).([a,x]) by FUNCT_1:72
    .= ((the Mult of RAlgebra the carrier of X)
       |[:REAL,(BoundedFunctions the carrier of X):]).([a,y]) by A1,FUNCT_1:72
    .=a*y by C0SP1:def 11;
end;

Lm6:
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
    y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
  st x1=y1 & x2=y2 holds x1*x2=y1*y2
proof
   let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
       y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
   assume A1: x1=y1 & x2=y2;
   thus x1*x2 = ((the multF of RAlgebra the carrier of X)||
      (ContinuousFunctions X)).([x1,x2]) by C0SP1:def 6
    .= (the multF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:72
    .= ((the multF of RAlgebra the carrier of X)
      ||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:72
    .=y1*y2 by C0SP1:def 6;
end;

registration let X;
  cluster R_Normed_Algebra_of_ContinuousFunctions X ->
          Abelian add-associative right_zeroed right_complementable
          commutative associative right_unital right-distributive
          vector-distributive scalar-distributive scalar-associative
          vector-associative;
  coherence
  proof
   1.(R_Normed_Algebra_of_ContinuousFunctions X)
     = 1_R_Algebra_of_ContinuousFunctions X;
   hence thesis by Th10;
 end;
end;

theorem Th11:
(Mult_(ContinuousFunctions X, RAlgebra the carrier of X)).(1,F) = F
proof
   set X1 = ContinuousFunctions X;
   reconsider f1 = F as Element of X1;
A1:[1,f1] in [:REAL,X1:] by ZFMISC_1:106;
   thus (Mult_(ContinuousFunctions X, RAlgebra the carrier of X)).(1,F)
    = ((the Mult of RAlgebra the carrier of X)| [:REAL,X1:]).(1,f1)
       by C0SP1:def 11
   .= (the Mult of RAlgebra the carrier of X).(1,f1) by A1,FUNCT_1:72
   .= F by FUNCSDOM:23;
end;

registration let X;
  cluster R_Normed_Algebra_of_ContinuousFunctions X -> vector-distributive
  scalar-distributive scalar-associative scalar-unital;
  coherence
proof
  for v being VECTOR of R_Normed_Algebra_of_ContinuousFunctions X
     holds 1 * v = v by Th11;
  hence thesis by RLVECT_1:def 11;
end;
end;

theorem Th12:
  X --> 0 = 0.R_Normed_Algebra_of_ContinuousFunctions X
proof
   X-->0 = 0.R_Algebra_of_ContinuousFunctions X by Th6;
   hence thesis;
end;

Lm7:
0.R_Normed_Algebra_of_ContinuousFunctions X
  = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X
proof
   thus 0.R_Normed_Algebra_of_ContinuousFunctions X = X-->0 by Th12
    .= 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:26;
end;

Lm8:
1.R_Normed_Algebra_of_ContinuousFunctions X
  = 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X
proof
   thus 1.R_Normed_Algebra_of_ContinuousFunctions X
    =1_R_Algebra_of_ContinuousFunctions X
   .= X-->1 by Th7
   .= 1_R_Algebra_of_BoundedFunctions the carrier of X by C0SP1:16
   .= 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X;
end;

theorem
0 <= ||.F.||
proof
   reconsider F1=F as Point of
     R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
   ||.F.|| =||.F1.|| by FUNCT_1:72;
   hence thesis by C0SP1:28;
end;

theorem
F = 0.R_Normed_Algebra_of_ContinuousFunctions X implies 0 = ||.F.||
proof
   assume A1: F = 0.R_Normed_Algebra_of_ContinuousFunctions X;
   reconsider F1=F as Point of
     R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A2: ||.F.|| =||.F1.|| by FUNCT_1:72;
   F= X--> 0 by A1,Th12; then
   F1 = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:26;
   hence thesis by A2,C0SP1:29;
end;

theorem Th15:
f=F & g=G & h=H implies
 (H = F+G iff for x be Element of X holds h.x = f.x + g.x)
proof
   reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions X;
   H=F+G iff h1=f1+g1;
   hence thesis by Th3;
end;

theorem
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )
proof
   reconsider f1=F, g1=G as VECTOR of R_Algebra_of_ContinuousFunctions X;
   G=a*F iff g1=a*f1;
   hence thesis by Th4;
end;

theorem
 f=F & g=G & h=H implies
(H = F*G iff for x be Element of X holds h.x = f.x * g.x)
proof
   reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions X;
   H=F*G iff h1=f1*g1;
   hence thesis by Th5;
end;

theorem Th18:
( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions X ) &
||.a*F.|| = abs a * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||
proof
   reconsider F1=F, G1=G as Point of
     R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A1: ||.F.|| =||.F1.|| by FUNCT_1:72;
A2: ||.G.|| =||.G1.|| by FUNCT_1:72;
A3: ||.F+G.|| =||.F1+G1.|| by Lm4,Lm3;
   ||.F1.|| = 0 iff
     F1=0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:33;
   hence ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions X
           by Lm7,FUNCT_1:72;
   thus ||.a*F.|| = ||.a*F1.|| by Lm5,Lm3
       .=abs a * ||.F1.|| by C0SP1:33
       .=abs a * ||.F.|| by FUNCT_1:72;
   thus ||.F+G.|| <= ||.F.|| + ||.G.|| by A1,A2,A3,C0SP1:33;
end;

registration let X;
  cluster R_Normed_Algebra_of_ContinuousFunctions X ->
   reflexive discerning RealNormSpace-like;
  coherence
  proof set R = R_Normed_Algebra_of_ContinuousFunctions X;
   thus ||.0.R.|| = 0 by Th18;
   for x,y being Point of R_Normed_Algebra_of_ContinuousFunctions X
   for a be Real holds
     ( ||.x.|| = 0 iff x = 0.R_Normed_Algebra_of_ContinuousFunctions(X) ) &
    ||.a*x.|| = abs(a) * ||.x.|| &
    ||.x+y.|| <= ||.x.|| + ||.y.|| by Th18;
   hence thesis by NORMSP_0:def 5,NORMSP_1:def 2;
 end;
end;

Lm9:
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
    y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
  st x1=y1 & x2=y2 holds x1-x2=y1-y2
proof
   let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
       y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
   assume A1: x1=y1 & x2=y2;
   -x2=(-1)*x2 by RLVECT_1:29
      .=(-1)*y2 by A1,Lm5
      .= -y2 by RLVECT_1:29;
   hence x1-x2 =y1-y2 by A1,Lm4;
end;

theorem
 f=F & g=G & h=H implies
  (H = F-G iff (for x be Element of X holds h.x = f.x - g.x))
proof
   assume A1: f=F & g=G & h=H;
A2:now assume H=F-G; then
    H+G=F-(G-G) by RLVECT_1:43; then
    H+G=F-0.R_Normed_Algebra_of_ContinuousFunctions X by RLVECT_1:28; then
A3: H+G=F by RLVECT_1:26;
    now let x be Element of X;
     f.x=h.x + g.x by A1,A3,Th15;
     hence f.x-g.x=h.x;
    end;
    hence for x be Element of X holds h.x = f.x - g.x;
   end;
   now assume
A4: for x be Element of X holds h.x = f.x - g.x;
    now let x be Element of X;
     h.x = f.x - g.x by A4;
     hence h.x + g.x= f.x;
    end; then
    F=H+G by A1,Th15; then
    F-G=H+(G-G) by RLVECT_1:def 6; then
    F-G=H+0.R_Normed_Algebra_of_ContinuousFunctions X by RLVECT_1:28;
    hence F-G=H by RLVECT_1:10;
   end;
   hence thesis by A2;
end;

theorem Th20:
for X be RealBanachSpace, Y be Subset of X, seq be sequence of X st
  Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm holds
    seq is convergent & lim seq in Y
proof
   let X be RealBanachSpace, Y be Subset of X, seq be sequence of X;
   assume
A1: Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm;
   hence seq is convergent by LOPBAN_1:def 16;
   hence thesis by A1,NFCONT_1:def 5;
end;

theorem Th21:
for Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X st
  Y = ContinuousFunctions X holds Y is closed
proof
   let Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
   assume A1: Y = ContinuousFunctions X;
   now let seq be sequence of
     R_Normed_Algebra_of_BoundedFunctions the carrier of X;
    assume A2: rng seq c= Y & seq is convergent;
    lim seq in BoundedFunctions the carrier of X; then
    consider f be Function of (the carrier of X),REAL such that
A3: f=lim seq & f|(the carrier of X) is bounded;
    now let z be set;
     assume z in BoundedFunctions (the carrier of X); then
     ex f be RealMap of X st f=z & f|(the carrier of X) is bounded;
     hence z in PFuncs(the carrier of X,REAL) by PARTFUN1:119;
    end; then
    BoundedFunctions (the carrier of X) c= PFuncs(the carrier of X,REAL)
      by TARSKI:def 3; then
    reconsider H = seq as Functional_Sequence of (the carrier of X),REAL
      by FUNCT_2:9;
A4: for p be Real st p>0 ex k be Element of NAT st
     for n be Element of NAT, x be set st
      n>=k & x in the carrier of X holds abs((H.n).x  - f.x) < p
    proof
     let p be Real;
     assume p>0; then
     consider k be Element of NAT such that
A5:  for n be Element of NAT st n >= k holds
        ||.seq.n - lim seq.|| < p by A2,NORMSP_1:def 11;
     take k;
     hereby let n be Element of NAT, x be set;
      assume A6: n>=k & x in the carrier of X; then
A7:  ||.seq.n - lim seq.|| < p by A5;
      seq.n - lim seq in BoundedFunctions the carrier of X; then
      consider g be RealMap of X such that
A8:   g=seq.n - lim seq & g|(the carrier of X) is bounded;
      seq.n in BoundedFunctions the carrier of X; then
      consider s be RealMap of X such that
A9:   s=seq.n & s|(the carrier of X) is bounded;
      reconsider x0 = x as Element of the carrier of X by A6;
A10:  g.x0= s.x0-f.x0 by A8,A9,A3,C0SP1:35;
      abs(g.x0) <= ||.seq.n - lim seq.|| by A8,C0SP1:27;
      hence abs((H.n).x  - f.x) < p by A10,A9,A7,XXREAL_0:2;
     end;
    end;
    f is continuous
    proof

     for x being Point of X,V being Subset of REAL st
      f.x in V & V is open holds
       ex W being Subset of X st x in W & W is open & f.:W c= V
     proof
      let x be Point of X,V be Subset of REAL;
      set r=f.x;
      assume f.x in V & V is open; then
      consider r0 being real number such that
A11:  0<r0 & ].r-r0,r+r0.[ c= V by RCOMP_1:40;
      consider k being Element of NAT such that
A12:   for n be Element of NAT,x be set st n>=k & x in the carrier of X holds
           abs((H.n).x  - f.x) < r0/3 by A4,A11,XREAL_1:224;
A13:  abs((H.k).x - f.x) < r0/3 by A12;
      k in NAT; then
      k in dom seq by NORMSP_1:17; then
      H.k in rng seq by FUNCT_1:def 5; then
      H.k in Y by A2; then
      consider h be continuous RealMap of X such that
A14:    H.k=h by A1;
      set r1 = h.x;
      set G1 = ]. r1-r0/3,r1+r0/3 .[;
A15:  r1<r1+r0/3 by A11,XREAL_1:31,224; then
      r1-r0/3<r1 by XREAL_1:21; then
      h.x in G1 by A15; then
      consider W1 being Subset of X such that
A16:   x in W1 & W1 is open & h.:W1 c= G1 by Th1;
      now let x0 be set;
       assume x0 in f.:W1; then
       consider z0 being set such that
A17:    z0 in dom f & z0 in W1 & f.z0=x0 by FUNCT_1:def 12;
       h.z0 in h.:W1 by A17,FUNCT_2:43; then
       h.x - r0/3 < h.z0 & h.z0 < h.x + r0/3 by A16,XXREAL_1:4; then
       h.x-r0/3 -h.x < h.z0-h.x & h.z0 - h.x < h.x + r0/3 -h.x
         by XREAL_1:11; then
A18:   abs(h.z0 - h.x) <= r0/3 by ABSVALUE:12;
A19:   abs(-(h.x - f.x)) < r0/3 by A13,A14,COMPLEX1:138;
       abs(h.z0 - f.z0) < r0/3 by A17,A12,A14; then
       abs(-(h.z0 - f.z0)) < r0/3 by COMPLEX1:138; then
       abs(f.z0 - h.z0)+abs(f.x - h.x) < r0/3 + r0/3 by A19,XREAL_1:10; then
A20:   abs(f.z0 - h.z0)+abs(f.x - h.x)+abs(h.z0  - h.x)
              < r0/3 + r0/3 + r0/3 by A18,XREAL_1:10;
       abs( f.z0 -f.x ) = abs((f.z0 - h.z0)- (f.x - h.x) +(h.z0-h.x)); then
A21:   abs( f.z0 -f.x ) <= abs((f.z0 - h.z0)- (f.x - h.x))
                                 +abs(h.z0-h.x) by COMPLEX1:142;
       abs((f.z0 - h.z0)- (f.x - h.x))
         <= abs(f.z0 - h.z0) + abs(f.x - h.x) by COMPLEX1:143; then
       abs((f.z0 - h.z0)- (f.x - h.x))+abs(h.z0-h.x)
         <= abs(f.z0 - h.z0) + abs(f.x - h.x) +abs(h.z0-h.x) by XREAL_1:8; then
       abs( f.z0 -f.x ) <= abs(f.z0 - h.z0)+abs(f.x - h.x)
                                 +abs(h.z0-h.x) by A21,XXREAL_0:2; then
       abs( f.z0 -f.x ) <r0 by A20,XXREAL_0:2; then
       -r0<f.z0 -f.x & f.z0 -f.x <r0 by SEQ_2:9; then
       -r0 + r < f.z0 -r + r & f.z0 - r + r <r0 + r by XREAL_1:8;
       hence x0 in ].r-r0,r+r0.[ by A17;
      end; then
      f.:W1 c= ].r-r0,r+r0.[ by TARSKI:def 3;
      hence ex W being Subset of X st x in W & W is open & f.:W c= V
         by A16,A11,XBOOLE_1:1;
     end;
     hence thesis by Th1;
    end;
    hence lim seq in Y by A3,A1;
   end;
   hence thesis by NFCONT_1:def 5;
end;

theorem Th22:
for seq be sequence of R_Normed_Algebra_of_ContinuousFunctions X st
 seq is Cauchy_sequence_by_Norm holds seq is convergent
proof
   let vseq be sequence of R_Normed_Algebra_of_ContinuousFunctions X;
   assume A1: vseq is Cauchy_sequence_by_Norm;
A2:for x being set st x in ContinuousFunctions X holds
     x in BoundedFunctions the carrier of X by Lm1; then
   ContinuousFunctions X c= BoundedFunctions the carrier of X
     by TARSKI:def 3; then
   rng vseq c= BoundedFunctions the carrier of X by XBOOLE_1:1; then
   reconsider vseq1=vseq as sequence of
     R_Normed_Algebra_of_BoundedFunctions the carrier of X by FUNCT_2:8;
   now let e be Real such that
A3: e >0;
    consider k be Element of NAT such that
A4:  for n,m be Element of NAT st n >= k & m >= k holds
      ||. vseq.n - vseq.m .|| < e by A1,A3,RSSPACE3:10;
    take k;
    now let n,m be Element of NAT;
     assume n >= k & m >= k; then
     ||. vseq.n - vseq.m .|| < e by A4;
     hence ||. vseq1.n - vseq1.m .|| < e by Lm9,Lm3;
    end;
    hence for n,m be Element of NAT st n >= k & m >= k holds
            ||. vseq1.n - vseq1.m .|| < e;
   end; then
A5:vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:10; then
A6:vseq1 is convergent by C0SP1:36;
   reconsider Y = ContinuousFunctions X as Subset of
     R_Normed_Algebra_of_BoundedFunctions the carrier of X by A2,TARSKI:def 3;
A7:rng vseq c= ContinuousFunctions X;
   Y is closed by Th21;then
   reconsider tv=lim vseq1 as Point of
     R_Normed_Algebra_of_ContinuousFunctions X by A7,A5,Th20;
   for e be Real st e > 0 ex k be Element of NAT st for n be Element of NAT st
     n >= k holds ||.vseq.n - tv.|| < e
   proof
    let e be Real;
    assume e > 0; then
    consider k be Element of NAT such that
A8:  for n be Element of NAT st n >= k holds
        ||.vseq1.n - lim vseq1.|| < e by A6,NORMSP_1:def 11;
    take k;
    now let n be Element of NAT;
     assume n >= k; then
     ||.vseq1.n-lim vseq1.|| < e by A8;
     hence ||.vseq.n-tv.|| < e by Lm9,Lm3;
    end;
    hence for n be Element of NAT st n >= k holds ||.vseq.n - tv.|| < e;
   end;
   hence thesis by NORMSP_1:def 9;
end;

registration let X;
  cluster R_Normed_Algebra_of_ContinuousFunctions X -> complete;
  coherence
  proof
   for seq be sequence of R_Normed_Algebra_of_ContinuousFunctions X st
    seq is Cauchy_sequence_by_Norm holds seq is convergent by Th22;
   hence thesis by LOPBAN_1:def 16;
 end;
end;

registration let X;
  cluster R_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like;
coherence
proof
   set B = R_Normed_Algebra_of_ContinuousFunctions X;
A1:now let f,g be Element of B;
    reconsider f1=f, g1=g as Point of
      R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A2: ||.f.|| =||.f1.|| & ||.g.|| =||.g1.|| & ||.f*g.|| =||.f1*g1.||
      by Lm6,Lm3;
    R_Normed_Algebra_of_BoundedFunctions the carrier of X is
      Banach_Algebra-like_1 by C0SP1:38;
    hence ||. f*g .|| <= ||.f.|| * ||.g.|| by A2,LOPBAN_2:def 9;
   end;
A3:  R_Normed_Algebra_of_BoundedFunctions the carrier of X
      is Banach_Algebra-like_2 by C0SP1:38;
A4:||. 1.B .||=||. 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X.||
      by Lm8,Lm3
   .= 1 by A3,LOPBAN_2:def 10;
A5:now let a be Real, f,g be Element of B;
    reconsider f1=f, g1=g as Point of
      R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A6: a*g1=a*g by Lm5;
A7: f*g=f1*g1 by Lm6;
A8: R_Normed_Algebra_of_BoundedFunctions the carrier of X is
      Banach_Algebra-like_3 by C0SP1:38;
    a*(f*g) =a*(f1*g1) by A7,Lm5; then
    a*(f*g) =f1*(a*g1) by A8,LOPBAN_2:def 11;
    hence a*(f*g) =f*(a*g) by A6,Lm6;
   end;
now let f,g,h be Element of B;
    reconsider f1=f, g1=g, h1=h as Point of
      R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A9: g+h = g1+h1 by Lm4;
A10: g*f = g1*f1 & h*f = h1*f1 by Lm6;
A11: R_Normed_Algebra_of_BoundedFunctions the carrier of X is
      left-distributive by C0SP1:38;
    thus (g+h)*f =(g1+h1)*f1 by Lm6,A9
                .= g1*f1 + h1*f1 by A11,VECTSP_1:def 12
                .= g*f + h*f by Lm4,A10;
   end;
   then B is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
     left-distributive left_unital complete Normed_Algebra
       by A1,A4,A5,LOPBAN_2:def 9,def 10,def 11,VECTSP_1:def 12;
   hence thesis;
end;
end;