:: C0SP2 semantic presentation

begin

definition
let X be 1-sorted ;
let y be real number ;
funcX --> y ->  RealMap of X equals :: C0SP2:def 1
 the carrier of X --> y;
coherence
 the carrier of X --> y is RealMap of X
proof
 y in REAL by XREAL_0:def_1;
then  the carrier of X --> y is RealMap of X by FUNCOP_1:45;
hence  the carrier of X --> y is RealMap of X ; ::_thesis: verum
end;
end;

:: deftheorem  defines --> C0SP2:def_1_:_
 for X being 1-sorted
for y being real number holds X --> y = the carrier of X --> y;

registration
let X be TopSpace;
let y be real number ;
clusterX --> y ->  continuous ;
coherence
 X --> y is continuous
proof
set f = X --> y;
set HX = [#] X;
let P1 be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not P1 is closed or (X --> y) " P1 is closed )
assume  P1 is closed ; ::_thesis: (X --> y) " P1 is closed
percases ( y in P1 or not y in P1 ) ;
suppose y in P1 ; ::_thesis: (X --> y) " P1 is closed
then  (X --> y) " P1 = [#] X by FUNCOP_1:14;
hence  (X --> y) " P1 is closed ; ::_thesis: verum
end;
suppose not y in P1 ; ::_thesis: (X --> y) " P1 is closed
then  (X --> y) " P1 = {} X by FUNCOP_1:16;
hence  (X --> y) " P1 is closed ; ::_thesis: verum
end;
end;
end;
end;

theorem Th1: :: C0SP2:1
for X being non empty TopSpace
for f being RealMap of X holds
( f is continuous iff for x being Point of X
for 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; ::_thesis: for f being RealMap of X holds
( f is continuous iff for x being Point of X
for 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 ) )
let f be RealMap of X; ::_thesis: ( f is continuous iff for x being Point of X
for 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 ) )
hereby  ::_thesis: ( ( for x being Point of X
for 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 ) ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for x being Point of X
for 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__::_thesis:_for_x_being_Point_of_X
for_V_being_Subset_of_REAL_st_f_._x_in_V_&_V_is_open_holds_
ex_W_being_Element_of_bool_the_carrier_of_X_st_
(_x_in_W_&_W_is_open_&_f_.:_W_c=_V_)
let x be Point of X; ::_thesis: for V being Subset of REAL st f . x in V & V is open holds
ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
let V be Subset of REAL; ::_thesis: ( f . x in V & V is open implies ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V ) )
set r = f . x;
assume  ( f . x in V & V is open ) ; ::_thesis: ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
then consider r0 being real number  such that
A2: ( 0 < r0 & ].((f . x) - r0),((f . x) + r0).[ c= V ) by RCOMP_1:19;
set S = ].((f . x) - r0),((f . x) + r0).[;
take W = f " ].((f . x) - r0),((f . x) + r0).[; ::_thesis: ( x in W & W is open & f .: W c= V )
 abs ((f . x) - (f . x)) < r0 by A2, COMPLEX1:44;
then  f . x in ].((f . x) - r0),((f . x) + r0).[ by RCOMP_1:1;
hence  x in W by FUNCT_2:38; ::_thesis: ( W is open & f .: W c= V )
thus  W is open by A1, PSCOMP_1:8; ::_thesis: f .: W c= V
 f .: (f " ].((f . x) - r0),((f . x) + r0).[) c= ].((f . x) - r0),((f . x) + r0).[ by FUNCT_1:75;
hence  f .: W c= V by A2, XBOOLE_1:1; ::_thesis: verum
end;
hence  for x being Point of X
for 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 ) ; ::_thesis: verum
end;
assume A3: for x being Point of X
for 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 ) ; ::_thesis: f is continuous
now__::_thesis:_for_Y_being_Subset_of_REAL_st_Y_is_closed_holds_
f_"_Y_is_closed
let Y be Subset of REAL; ::_thesis: ( Y is closed implies f " Y is closed )
assume  Y is closed ; ::_thesis: f " 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) ` holds
ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )
proof
let x be Point of X; ::_thesis: ( x in (f " Y) ` implies ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` ) )
assume  x in (f " Y) ` ; ::_thesis: ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )
then  x in f " (Y `) by FUNCT_2:100;
then  f . x in Y ` by FUNCT_2:38;
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 ; ::_thesis: ( W is a_neighborhood of x & W c= (f " Y) ` )
thus  W is a_neighborhood of x by A6, CONNSP_2:3; ::_thesis: W c= (f " Y) `
 f .: W c= Y ` by A5, A6, XBOOLE_1:1;
then A7: f " (f .: W) c= f " (Y `) by RELAT_1:143;
 W c= f " (f .: W) by FUNCT_2:42;
then  W c= f " (Y `) by A7, XBOOLE_1:1;
hence  W c= (f " Y) ` by FUNCT_2:100; ::_thesis: verum
end;
then  (f " Y) ` is open by CONNSP_2:7;
then  ((f " Y) `) ` is closed by TOPS_1:4;
hence  f " Y is closed ; ::_thesis: verum
end;
hence  f is continuous by PSCOMP_1:def_3; ::_thesis: verum
end;

definition
let X be non empty TopSpace;
func ContinuousFunctions X ->  Subset of (RAlgebra the carrier of X) equals :: C0SP2:def 2
 {  f where f is continuous RealMap of X : verum  }  ;
correctness
coherence
{  f where f is continuous RealMap of X : verum  }  is Subset of (RAlgebra the carrier of X);
proof
set A =  {  f where f is continuous RealMap of X : verum  }  ;
  {  f where f is continuous RealMap of X : verum  }  c= Funcs ( the carrier of X,REAL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  f where f is continuous RealMap of X : verum  }  or x in Funcs ( the carrier of X,REAL) )
assume  x in  {  f where f is continuous RealMap of X : verum  }  ; ::_thesis: x in Funcs ( the carrier of X,REAL)
then  ex f being continuous RealMap of X st x = f ;
hence  x in Funcs ( the carrier of X,REAL) by FUNCT_2:8; ::_thesis: verum
end;
hence   {  f where f is continuous RealMap of X : verum  }  is Subset of (RAlgebra the carrier of X) ; ::_thesis: verum
end;
end;

:: deftheorem  defines ContinuousFunctions C0SP2:def_2_:_
 for X being non empty TopSpace holds ContinuousFunctions X =  {  f where f is continuous RealMap of X : verum  }  ;

registration
let X be non empty TopSpace;
cluster ContinuousFunctions X ->  non empty ;
coherence
 not ContinuousFunctions X is empty
proof
 X --> 0 in  {  f where f is continuous RealMap of X : verum  }  ;
hence  not ContinuousFunctions X is empty ; ::_thesis: verum
end;
end;

registration
let X be non empty TopSpace;
cluster ContinuousFunctions X ->  multiplicatively-closed additively-linearly-closed ;
coherence
 ( ContinuousFunctions X is additively-linearly-closed & ContinuousFunctions X is multiplicatively-closed )
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 being Element of (RAlgebra the carrier of X) st v in ContinuousFunctions X & u in ContinuousFunctions X holds
v + u in ContinuousFunctions X
proof
let v, u be Element of (RAlgebra the carrier of X); ::_thesis: ( v in ContinuousFunctions X & u in ContinuousFunctions X implies v + u in ContinuousFunctions X )
assume A2: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; ::_thesis: v + u in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A3: v1 = v by A2;
consider u1 being continuous RealMap of X such that
A4: u1 = u by A2;
A5: ( v1 + u1 is Function of the carrier of X,REAL & v1 + u1 is continuous ) by NAGATA_1:22;
reconsider h = v + u as Element of Funcs ( the carrier of X,REAL) ;
A6: 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 A7: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of X by FUNCT_2:def_1;
 for x being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A3, A4, FUNCSDOM:1;
then  v + u = v1 + u1 by A7, A6, VALUED_1:def_1;
hence  v + u in ContinuousFunctions X by A5; ::_thesis: verum
end;
then A8: ContinuousFunctions X is add-closed by IDEAL_1:def_1;
 for v being Element of (RAlgebra the carrier of X) st v in ContinuousFunctions X holds
- v in ContinuousFunctions X
proof
let v be Element of (RAlgebra the carrier of X); ::_thesis: ( v in ContinuousFunctions X implies - v in ContinuousFunctions X )
assume A9: v in ContinuousFunctions X ; ::_thesis: - v in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A10: v1 = v by A9;
A11: - v1 is continuous RealMap of X by PSCOMP_1:9;
reconsider h = - v, v2 = v as Element of Funcs ( the carrier of X,REAL) ;
A12: h = (- 1) * v by A1, RLVECT_1:16;
A13: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= REAL ) by FUNCT_2:def_2;
A14: dom v1 = the carrier of X by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_-_(v1_._x)
let x be set ; ::_thesis: ( x in dom h implies h . x = - (v1 . x) )
assume  x in dom h ; ::_thesis: h . x = - (v1 . x)
then reconsider y = x as Element of the carrier of X ;
 h . x = (- 1) * (v2 . y) by A12, FUNCSDOM:4;
hence  h . x = - (v1 . x) by A10; ::_thesis: verum
end;
then  - v = - v1 by A14, A13, VALUED_1:9;
hence  - v in ContinuousFunctions X by A11; ::_thesis: verum
end;
then A15: ContinuousFunctions X is having-inverse by C0SP1:def_1;
 for a being Real
for u being Element of (RAlgebra the carrier of X) st u in ContinuousFunctions X holds
a * u in ContinuousFunctions X
proof
let a be Real; ::_thesis: for u being Element of (RAlgebra the carrier of X) st u in ContinuousFunctions X holds
a * u in ContinuousFunctions X
let u be Element of (RAlgebra the carrier of X); ::_thesis: ( u in ContinuousFunctions X implies a * u in ContinuousFunctions X )
assume A16: u in ContinuousFunctions X ; ::_thesis: a * u in ContinuousFunctions X
consider u1 being continuous RealMap of X such that
A17: u1 = u by A16;
A18: a (#) u1 is continuous RealMap of X
proof
reconsider U = u1 as continuous Function of X,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of X;
consider H being Function of X,R^1 such that
A19: for p being Point of X
for r1 being real number st U . p = r1 holds
H . p = a * r1 and
A20: H is continuous by JGRAPH_2:23;
reconsider h = H as RealMap of X by TOPMETR:17;
A21: dom h = the carrier of X by FUNCT_2:def_1
.= dom u1 by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = a * (u1 . c) by A19;
then  h = a (#) u1 by A21, VALUED_1:def_5;
hence  a (#) u1 is continuous RealMap of X by A20, JORDAN5A:27; ::_thesis: verum
end;
reconsider h = a * 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;
A23: dom u1 = the carrier of X by FUNCT_2:def_1;
 for x being set st x in dom h holds
h . x = a * (u1 . x) by A17, FUNCSDOM:4;
then  a * u = a (#) u1 by A23, A22, VALUED_1:def_5;
hence  a * u in ContinuousFunctions X by A18; ::_thesis: verum
end;
hence  ContinuousFunctions X is additively-linearly-closed by A8, A15, C0SP1:def_10; ::_thesis: ContinuousFunctions X is multiplicatively-closed
A24: for v, u being Element of (RAlgebra the carrier of X) st v in ContinuousFunctions X & u in ContinuousFunctions X holds
v * u in ContinuousFunctions X
proof
let v, u be Element of (RAlgebra the carrier of X); ::_thesis: ( v in ContinuousFunctions X & u in ContinuousFunctions X implies v * u in ContinuousFunctions X )
assume A25: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; ::_thesis: v * u in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A26: v1 = v by A25;
consider u1 being continuous RealMap of X such that
A27: u1 = u by A25;
A28: v1 (#) u1 is continuous RealMap of X
proof
reconsider V = v1, U = u1 as continuous Function of X,R^1 by JORDAN5A:27, TOPMETR:17;
consider H being Function of X,R^1 such that
A29: for p being Point of X
for r1, r2 being real number st V . p = r1 & U . p = r2 holds
H . p = r1 * r2 and
A30: H is continuous by JGRAPH_2:25;
reconsider h = H as RealMap of X by TOPMETR:17;
A31: dom h = the carrier of X /\ the carrier of X by FUNCT_2:def_1
.= the carrier of X /\ (dom u1) by FUNCT_2:def_1
.= (dom v1) /\ (dom u1) by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = (v1 . c) * (u1 . c) by A29;
then  h = v1 (#) u1 by A31, VALUED_1:def_4;
hence  v1 (#) u1 is continuous RealMap of X by A30, JORDAN5A:27; ::_thesis: verum
end;
reconsider h = v * u as Element of Funcs ( the carrier of X,REAL) ;
A32: 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 A33: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of X by FUNCT_2:def_1;
 for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A26, A27, FUNCSDOM:2;
then  v * u = v1 (#) u1 by A33, A32, VALUED_1:def_4;
hence  v * u in ContinuousFunctions X by A28; ::_thesis: verum
end;
reconsider g = RealFuncUnit the carrier of X as RealMap of X ;
 g = X --> 1 ;
then  1. (RAlgebra the carrier of X) in ContinuousFunctions X ;
hence  ContinuousFunctions X is multiplicatively-closed by A24, C0SP1:def_4; ::_thesis: verum
end;
end;

definition
let X be non empty TopSpace;
func R_Algebra_of_ContinuousFunctions X ->  AlgebraStr  equals :: C0SP2:def 3
 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
 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))) #) is AlgebraStr ;
end;

:: deftheorem  defines R_Algebra_of_ContinuousFunctions C0SP2:def_3_:_
 for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X = 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))) #);

theorem :: C0SP2:2
for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X is Subalgebra of RAlgebra the carrier of X by C0SP1:6;

registration
let X be non empty TopSpace;
cluster R_Algebra_of_ContinuousFunctions X ->  non empty strict ;
coherence
 ( R_Algebra_of_ContinuousFunctions X is strict & not R_Algebra_of_ContinuousFunctions X is empty ) ;
end;

registration
let X be non empty TopSpace;
cluster R_Algebra_of_ContinuousFunctions X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital associative commutative right-distributive right_unital vector-associative ;
coherence
 ( R_Algebra_of_ContinuousFunctions X is Abelian & R_Algebra_of_ContinuousFunctions X is add-associative & R_Algebra_of_ContinuousFunctions X is right_zeroed & R_Algebra_of_ContinuousFunctions X is right_complementable & R_Algebra_of_ContinuousFunctions X is vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is scalar-unital & R_Algebra_of_ContinuousFunctions X is commutative & R_Algebra_of_ContinuousFunctions X is associative & R_Algebra_of_ContinuousFunctions X is right_unital & R_Algebra_of_ContinuousFunctions X is right-distributive & R_Algebra_of_ContinuousFunctions X is vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is vector-associative )
proof
now__::_thesis:_for_v_being_VECTOR_of_(R_Algebra_of_ContinuousFunctions_X)_holds_1_*_v_=_v
let v be VECTOR of (R_Algebra_of_ContinuousFunctions X); ::_thesis: 1 * v = v
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:12; ::_thesis: verum
end;
hence  ( R_Algebra_of_ContinuousFunctions X is Abelian & R_Algebra_of_ContinuousFunctions X is add-associative & R_Algebra_of_ContinuousFunctions X is right_zeroed & R_Algebra_of_ContinuousFunctions X is right_complementable & R_Algebra_of_ContinuousFunctions X is vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is scalar-unital & R_Algebra_of_ContinuousFunctions X is commutative & R_Algebra_of_ContinuousFunctions X is associative & R_Algebra_of_ContinuousFunctions X is right_unital & R_Algebra_of_ContinuousFunctions X is right-distributive & R_Algebra_of_ContinuousFunctions X is vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is vector-associative ) by C0SP1:6, RLVECT_1:def_8; ::_thesis: verum
end;
end;

theorem Th3: :: C0SP2:3
for X being non empty TopSpace
for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )
proof
let X be non empty TopSpace; ::_thesis: for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )
let F, G, H be VECTOR of (R_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )
let f, g, h be RealMap of X; ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )
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  ::_thesis: ( ( for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) implies H = F + G )
assume A3: H = F + G ; ::_thesis: for x being Element of the carrier of X holds h . x = (f . x) + (g . x)
let x be Element of the carrier of X; ::_thesis: h . x = (f . x) + (g . x)
 h1 = f1 + g1 by A2, A3, C0SP1:8;
hence  h . x = (f . x) + (g . x) by A1, FUNCSDOM:1; ::_thesis: verum
end;
assume  for x being Element of X holds h . x = (f . x) + (g . x) ; ::_thesis: H = F + G
then  h1 = f1 + g1 by A1, FUNCSDOM:1;
hence  H = F + G by A2, C0SP1:8; ::_thesis: verum
end;

theorem Th4: :: C0SP2:4
for X being non empty TopSpace
for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X
for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof
let X be non empty TopSpace; ::_thesis: for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X
for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let F, G, H be VECTOR of (R_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being RealMap of X
for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let f, g, h be RealMap of X; ::_thesis: for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let a be Real; ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) )
assume A1: ( f = F & g = G ) ; ::_thesis: ( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
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  ::_thesis: ( ( for x being Element of X holds g . x = a * (f . x) ) implies G = a * F )
assume A3: G = a * F ; ::_thesis: for x being Element of the carrier of X holds g . x = a * (f . x)
let x be Element of the carrier of X; ::_thesis: g . x = a * (f . x)
 g1 = a * f1 by A2, A3, C0SP1:8;
hence  g . x = a * (f . x) by A1, FUNCSDOM:4; ::_thesis: verum
end;
assume  for x being Element of the carrier of X holds g . x = a * (f . x) ; ::_thesis: G = a * F
then  g1 = a * f1 by A1, FUNCSDOM:4;
hence  G = a * F by A2, C0SP1:8; ::_thesis: verum
end;

theorem Th5: :: C0SP2:5
for X being non empty TopSpace
for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )
proof
let X be non empty TopSpace; ::_thesis: for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )
let F, G, H be VECTOR of (R_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )
let f, g, h be RealMap of X; ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )
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  ::_thesis: ( ( for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) implies H = F * G )
assume A3: H = F * G ; ::_thesis: for x being Element of the carrier of X holds h . x = (f . x) * (g . x)
let x be Element of the carrier of X; ::_thesis: h . x = (f . x) * (g . x)
 h1 = f1 * g1 by A2, A3, C0SP1:8;
hence  h . x = (f . x) * (g . x) by A1, FUNCSDOM:2; ::_thesis: verum
end;
assume  for x being Element of X holds h . x = (f . x) * (g . x) ; ::_thesis: H = F * G
then  h1 = f1 * g1 by A1, FUNCSDOM:2;
hence  H = F * G by A2, C0SP1:8; ::_thesis: verum
end;

theorem Th6: :: C0SP2:6
for X being non empty TopSpace holds 0. (R_Algebra_of_ContinuousFunctions X) = X --> 0
proof
let X be non empty TopSpace; ::_thesis: 0. (R_Algebra_of_ContinuousFunctions X) = X --> 0
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  0. (R_Algebra_of_ContinuousFunctions X) = X --> 0 by A1, C0SP1:8; ::_thesis: verum
end;

theorem Th7: :: C0SP2:7
for X being non empty TopSpace holds 1_ (R_Algebra_of_ContinuousFunctions X) = X --> 1
proof
let X be non empty TopSpace; ::_thesis: 1_ (R_Algebra_of_ContinuousFunctions X) = X --> 1
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  1_ (R_Algebra_of_ContinuousFunctions X) = X --> 1 by A1, C0SP1:8; ::_thesis: verum
end;

theorem Th8: :: C0SP2:8
for A being Algebra
for A1, A2 being Subalgebra of A st the carrier of A1 c= the carrier of A2 holds
A1 is Subalgebra of A2
proof
let A be Algebra; ::_thesis: for A1, A2 being Subalgebra of A st the carrier of A1 c= the carrier of A2 holds
A1 is Subalgebra of A2
let A1, A2 be Subalgebra of A; ::_thesis: ( the carrier of A1 c= the carrier of A2 implies A1 is Subalgebra of A2 )
assume A1: the carrier of A1 c= the carrier of A2 ; ::_thesis: A1 is Subalgebra 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 = the addF of A || the carrier of A1 & the addF of A2 = the addF of A || the carrier of A2 & [: the carrier of A1, the carrier of A1:] c= [: the carrier of A2, the carrier of A2:] ) by A1, C0SP1:def_9, ZFMISC_1:96;
hence  the addF of A1 = the addF of A2 || the carrier of A1 by FUNCT_1:51; ::_thesis: verum
end;
A4: the multF of A1 = the multF of A2 || the carrier of A1
proof
 ( the multF of A1 = the multF of A || the carrier of A1 & the multF of A2 = the multF of A || the carrier of A2 & [: the carrier of A1, the carrier of A1:] c= [: the carrier of A2, the carrier of A2:] ) by A1, C0SP1:def_9, ZFMISC_1:96;
hence  the multF of A1 = the multF of A2 || the carrier of A1 by FUNCT_1:51; ::_thesis: verum
end;
 the Mult of A1 = the Mult of A2 | [:REAL, the carrier of A1:]
proof
 ( the Mult of A1 = the Mult of A | [:REAL, the carrier of A1:] & the Mult of A2 = the Mult of A | [:REAL, the carrier of A2:] & [:REAL, the carrier of A1:] c= [:REAL, the carrier of A2:] ) by A1, C0SP1:def_9, ZFMISC_1:96;
hence  the Mult of A1 = the Mult of A2 | [:REAL, the carrier of A1:] by FUNCT_1:51; ::_thesis: verum
end;
hence  A1 is Subalgebra of A2 by A1, A2, A3, A4, C0SP1:def_9; ::_thesis: verum
end;

Lm1:  for X being non empty compact TopSpace
for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X
proof
let X be non empty compact TopSpace; ::_thesis: for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X
let x be set ; ::_thesis: ( x in ContinuousFunctions X implies x in BoundedFunctions the carrier of X )
assume  x in ContinuousFunctions X ; ::_thesis: x in BoundedFunctions the carrier of X
then consider h being 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:70;
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:71;
 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:75;
hence  x in BoundedFunctions the carrier of X by A1; ::_thesis: verum
end;

theorem :: C0SP2:9
for X being non empty compact TopSpace holds R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X
proof
let X be non empty compact TopSpace; ::_thesis: R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X
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  the carrier of (R_Algebra_of_ContinuousFunctions X) c= the carrier of (R_Algebra_of_BoundedFunctions the carrier of X) by TARSKI:def_3; ::_thesis: verum
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  R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X by A1, A2, Th8; ::_thesis: verum
end;

definition
let X be non empty compact TopSpace;
func ContinuousFunctionsNorm X ->  Function of (ContinuousFunctions X),REAL equals :: C0SP2:def 4
(BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);
correctness
coherence
(BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of (ContinuousFunctions X),REAL;
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  (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of (ContinuousFunctions X),REAL by FUNCT_2:32; ::_thesis: verum
end;
end;

:: deftheorem  defines ContinuousFunctionsNorm C0SP2:def_4_:_
 for X being non empty compact TopSpace holds ContinuousFunctionsNorm X = (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);

definition
let X be non empty compact TopSpace;
func R_Normed_Algebra_of_ContinuousFunctions X ->  Normed_AlgebraStr  equals :: C0SP2:def 5
 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
coherence
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) #) is Normed_AlgebraStr ;
;
end;

:: deftheorem  defines R_Normed_Algebra_of_ContinuousFunctions C0SP2:def_5_:_
 for X being non empty compact TopSpace holds R_Normed_Algebra_of_ContinuousFunctions X = 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) #);

registration
let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->  non empty strict ;
correctness
coherence
( R_Normed_Algebra_of_ContinuousFunctions X is strict & not R_Normed_Algebra_of_ContinuousFunctions X is empty );
;
end;

Lm2: now__::_thesis:_for_X_being_non_empty_compact_TopSpace
for_x,_e_being_Element_of_(R_Normed_Algebra_of_ContinuousFunctions_X)_st_e_=_One__((ContinuousFunctions_X),(RAlgebra_the_carrier_of_X))_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let X be non empty compact TopSpace; ::_thesis: for x, e being Element of (R_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) holds
( x * e = x & e * x = x )
set F = R_Normed_Algebra_of_ContinuousFunctions X;
let x, e be Element of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) )
assume A1: e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) ; ::_thesis: ( x * e = x & e * x = x )
set X1 = ContinuousFunctions X;
reconsider f = x as Element of ContinuousFunctions X ;
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 [:(ContinuousFunctions X),(ContinuousFunctions X):] & [(1_ (RAlgebra the carrier of X)),f] in [:(ContinuousFunctions X),(ContinuousFunctions X):] ) by ZFMISC_1:87;
 x * e = (mult_ ((ContinuousFunctions X),(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) || (ContinuousFunctions X)) . (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:49;
hence  x * e = x by VECTSP_1:def_4; ::_thesis: e * x = x
 e * x = (mult_ ((ContinuousFunctions X),(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) || (ContinuousFunctions X)) . ((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:49;
hence  e * x = x by VECTSP_1:def_4; ::_thesis: verum
end;

registration
let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->  unital ;
correctness
coherence
R_Normed_Algebra_of_ContinuousFunctions X is unital ;
proof
reconsider e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) as Element of (R_Normed_Algebra_of_ContinuousFunctions X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm2; ::_thesis: verum
end;
end;

theorem Th10: :: C0SP2:10
for W being Normed_AlgebraStr
for V being Algebra st AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds
W is Algebra
proof
let W be Normed_AlgebraStr ; ::_thesis: for V being Algebra st AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds
W is Algebra
let V be Algebra; ::_thesis: ( AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V implies W is Algebra )
assume A1: AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V ; ::_thesis: W is Algebra
reconsider W = 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; ::_thesis: x + y = y + x
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; ::_thesis: verum
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; ::_thesis: (x + y) + z = x + (y + z)
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_3;
hence  (x + y) + z = x + (y + z) by A1; ::_thesis: verum
end;
A4: for x being VECTOR of W holds x + (0. W) = x
proof
let x be VECTOR of W; ::_thesis: x + (0. W) = x
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:4; ::_thesis: verum
end;
A5: for x being Element of W holds x is right_complementable
proof
let x be Element of W; ::_thesis: x is right_complementable
reconsider x1 = x as Element of V by A1;
consider v being 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  x is right_complementable by ALGSTR_0:def_11; ::_thesis: verum
end;
A7: for v, w being Element of W holds v * w = w * v
proof
let v, w be Element of W; ::_thesis: v * w = w * v
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; ::_thesis: verum
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; ::_thesis: (a * b) * x = a * (b * x)
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_3;
hence  (a * b) * x = a * (b * x) by A1; ::_thesis: verum
end;
A9: W is right_unital
proof
let x be Element of W; :: according to VECTSP_1:def_4 ::_thesis: x * (1. W) = x
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_4; ::_thesis: verum
end;
A10: W is right-distributive
proof
let x, y, z be Element of W; :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
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_2;
hence  x * (y + z) = (x * y) + (x * z) by A1; ::_thesis: verum
end;
 ( W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
thus  W is vector-distributive ::_thesis: ( W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
let a be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of W holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of W; ::_thesis: a * (x + y) = (a * x) + (a * y)
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_5;
hence  a * (x + y) = (a * x) + (a * y) by A1; ::_thesis: verum
end;
thus  W is scalar-distributive ::_thesis: ( W is scalar-associative & W is vector-associative )
proof
let a, b be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of W holds (a + b) * b1 = (a * b1) + (b * b1)
let x be Element of W; ::_thesis: (a + b) * x = (a * x) + (b * x)
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_6;
hence  (a + b) * x = (a * x) + (b * x) by A1; ::_thesis: verum
end;
thus  W is scalar-associative ::_thesis: W is vector-associative
proof
let a, b be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of W holds (a * b) * b1 = a * (b * b1)
let x be Element of W; ::_thesis: (a * b) * x = a * (b * x)
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_7;
hence  (a * b) * x = a * (b * x) by A1; ::_thesis: verum
end;
let x, y be Element of W; :: according to FUNCSDOM:def_9 ::_thesis: for b1 being Element of REAL holds b1 * (x * y) = (b1 * x) * y
let a be Real; ::_thesis: a * (x * y) = (a * x) * y
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_9;
hence  a * (x * y) = (a * x) * y by A1; ::_thesis: verum
end;
hence  W is Algebra by A2, A3, A4, A5, A7, A8, A9, A10, ALGSTR_0:def_16, GROUP_1:def_3, GROUP_1:def_12, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;

Lm3:  for X being non empty compact TopSpace
for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
||.x.|| = ||.y.||
by FUNCT_1:49;

Lm4:  for X being non empty compact TopSpace
for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
proof
let X be non empty compact TopSpace; ::_thesis: for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let x1, x2 be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let y1, y2 be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 + x2 = y1 + y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 + x2 = y1 + 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:49
.= ( the addF of (RAlgebra the carrier of X) || (BoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49
.= y1 + y2 by C0SP1:def_5 ; ::_thesis: verum
end;

Lm5:  for X being non empty compact TopSpace
for a being Real
for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
proof
let X be non empty compact TopSpace; ::_thesis: for a being Real
for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let a be Real; ::_thesis: for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let x be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let y be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; ::_thesis: a * x = a * 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:49
.= ( the Mult of (RAlgebra the carrier of X) | [:REAL,(BoundedFunctions the carrier of X):]) . [a,y] by A1, FUNCT_1:49
.= a * y by C0SP1:def_11 ; ::_thesis: verum
end;

Lm6:  for X being non empty compact TopSpace
for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2
proof
let X be non empty compact TopSpace; ::_thesis: for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2
let x1, x2 be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2
let y1, y2 be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 * x2 = y1 * y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 * x2 = y1 * 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:49
.= ( the multF of (RAlgebra the carrier of X) || (BoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49
.= y1 * y2 by C0SP1:def_6 ; ::_thesis: verum
end;

registration
let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ;
coherence
 ( R_Normed_Algebra_of_ContinuousFunctions X is Abelian & R_Normed_Algebra_of_ContinuousFunctions X is add-associative & R_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & R_Normed_Algebra_of_ContinuousFunctions X is right_complementable & R_Normed_Algebra_of_ContinuousFunctions X is commutative & R_Normed_Algebra_of_ContinuousFunctions X is associative & R_Normed_Algebra_of_ContinuousFunctions X is right_unital & R_Normed_Algebra_of_ContinuousFunctions X is right-distributive & R_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & R_Normed_Algebra_of_ContinuousFunctions X is vector-associative )
proof
 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1_ (R_Algebra_of_ContinuousFunctions X) ;
hence  ( R_Normed_Algebra_of_ContinuousFunctions X is Abelian & R_Normed_Algebra_of_ContinuousFunctions X is add-associative & R_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & R_Normed_Algebra_of_ContinuousFunctions X is right_complementable & R_Normed_Algebra_of_ContinuousFunctions X is commutative & R_Normed_Algebra_of_ContinuousFunctions X is associative & R_Normed_Algebra_of_ContinuousFunctions X is right_unital & R_Normed_Algebra_of_ContinuousFunctions X is right-distributive & R_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & R_Normed_Algebra_of_ContinuousFunctions X is vector-associative ) by Th10; ::_thesis: verum
end;
end;

theorem Th11: :: C0SP2:11
for X being non empty compact TopSpace
for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . (1,F) = F
proof
let X be non empty compact TopSpace; ::_thesis: for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . (1,F) = F
let F be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: (Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . (1,F) = F
set X1 = ContinuousFunctions X;
reconsider f1 = F as Element of ContinuousFunctions X ;
A1: [1,f1] in [:REAL,(ContinuousFunctions X):] by ZFMISC_1:87;
thus (Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . (1,F) = ( the Mult of (RAlgebra the carrier of X) | [:REAL,(ContinuousFunctions X):]) . (1,f1) by C0SP1:def_11
.= the Mult of (RAlgebra the carrier of X) . (1,f1) by A1, FUNCT_1:49
.= F by FUNCSDOM:12 ; ::_thesis: verum
end;

registration
let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->  vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( R_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & R_Normed_Algebra_of_ContinuousFunctions X is scalar-unital )
proof
 for v being VECTOR of (R_Normed_Algebra_of_ContinuousFunctions X) holds 1 * v = v by Th11;
hence  ( R_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & R_Normed_Algebra_of_ContinuousFunctions X is scalar-unital ) by RLVECT_1:def_8; ::_thesis: verum
end;
end;

theorem Th12: :: C0SP2:12
for X being non empty compact TopSpace holds X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X)
proof
let X be non empty compact TopSpace; ::_thesis: X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X)
 X --> 0 = 0. (R_Algebra_of_ContinuousFunctions X) by Th6;
hence  X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ; ::_thesis: verum
end;

Lm7:  for X being non empty compact TopSpace holds 0. (R_Normed_Algebra_of_ContinuousFunctions X) = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
proof
let X be non empty compact TopSpace; ::_thesis: 0. (R_Normed_Algebra_of_ContinuousFunctions X) = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
thus  0. (R_Normed_Algebra_of_ContinuousFunctions X) = X --> 0 by Th12
.= 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by C0SP1:25 ; ::_thesis: verum
end;

Lm8:  for X being non empty compact TopSpace holds 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
proof
let X be non empty compact TopSpace; ::_thesis: 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
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) ; ::_thesis: verum
end;

theorem :: C0SP2:13
for X being non empty compact TopSpace
for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||
proof
let X be non empty compact TopSpace; ::_thesis: for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||
let F be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 0 <= ||.F.||
reconsider F1 = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
 ||.F.|| = ||.F1.|| by FUNCT_1:49;
hence  0 <= ||.F.|| by C0SP1:27; ::_thesis: verum
end;

theorem :: C0SP2:14
for X being non empty compact TopSpace
for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) st F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) holds
0 = ||.F.||
proof
let X be non empty compact TopSpace; ::_thesis: for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) st F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) holds
0 = ||.F.||
let F be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies 0 = ||.F.|| )
assume A1: F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ; ::_thesis: 0 = ||.F.||
reconsider F1 = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A2: ||.F.|| = ||.F1.|| by FUNCT_1:49;
 F = X --> 0 by A1, Th12;
then  F1 = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by C0SP1:25;
hence  0 = ||.F.|| by A2, C0SP1:28; ::_thesis: verum
end;

theorem Th15: :: C0SP2:15
for X being non empty compact TopSpace
for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof
let X be non empty compact TopSpace; ::_thesis: for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
let F, G, H be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
let f, g, h be RealMap of X; ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (R_Algebra_of_ContinuousFunctions X) ;
 ( H = F + G iff h1 = f1 + g1 ) ;
hence  ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) ) by Th3; ::_thesis: verum
end;

theorem :: C0SP2:16
for a being Real
for X being non empty compact TopSpace
for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g being RealMap of X st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof
let a be Real; ::_thesis: for X being non empty compact TopSpace
for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g being RealMap of X st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let X be non empty compact TopSpace; ::_thesis: for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g being RealMap of X st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let F, G be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g being RealMap of X st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
let f, g be RealMap of X; ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) )
reconsider f1 = F, g1 = G as VECTOR of (R_Algebra_of_ContinuousFunctions X) ;
 ( G = a * F iff g1 = a * f1 ) ;
hence  ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) ) by Th4; ::_thesis: verum
end;

theorem :: C0SP2:17
for X being non empty compact TopSpace
for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
proof
let X be non empty compact TopSpace; ::_thesis: for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
let F, G, H be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
let f, g, h be RealMap of X; ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (R_Algebra_of_ContinuousFunctions X) ;
 ( H = F * G iff h1 = f1 * g1 ) ;
hence  ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) ) by Th5; ::_thesis: verum
end;

theorem Th18: :: C0SP2:18
for a being Real
for X being non empty compact TopSpace
for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
proof
let a be Real; ::_thesis: for X being non empty compact TopSpace
for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let X be non empty compact TopSpace; ::_thesis: for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
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:49;
A2: ||.G.|| = ||.G1.|| by FUNCT_1:49;
A3: ||.(F + G).|| = ||.(F1 + G1).|| by Lm4, Lm3;
 ( ||.F1.|| = 0 iff F1 = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by C0SP1:32;
hence  ( ||.F.|| = 0 iff F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) by Lm7, FUNCT_1:49; ::_thesis: ( ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
thus ||.(a * F).|| = ||.(a * F1).|| by Lm5, Lm3
.= (abs a) * ||.F1.|| by C0SP1:32
.= (abs a) * ||.F.|| by FUNCT_1:49 ; ::_thesis: ||.(F + G).|| <= ||.F.|| + ||.G.||
thus  ||.(F + G).|| <= ||.F.|| + ||.G.|| by A1, A2, A3, C0SP1:32; ::_thesis: verum
end;

registration
let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->  discerning reflexive RealNormSpace-like ;
coherence
 ( R_Normed_Algebra_of_ContinuousFunctions X is reflexive & R_Normed_Algebra_of_ContinuousFunctions X is discerning & R_Normed_Algebra_of_ContinuousFunctions X is RealNormSpace-like )
proof
set R = R_Normed_Algebra_of_ContinuousFunctions X;
thus  ||.(0. (R_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Th18; :: according to NORMSP_0:def_6 ::_thesis: ( R_Normed_Algebra_of_ContinuousFunctions X is discerning & R_Normed_Algebra_of_ContinuousFunctions X is RealNormSpace-like )
 for x, y being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( x = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th18;
hence  ( R_Normed_Algebra_of_ContinuousFunctions X is discerning & R_Normed_Algebra_of_ContinuousFunctions X is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum
end;
end;

Lm9:  for X being non empty compact TopSpace
for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
proof
let X be non empty compact TopSpace; ::_thesis: for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
let x1, x2 be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
let y1, y2 be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 - x2 = y1 - y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 - x2 = y1 - y2
- x2 = (- 1) * x2 by RLVECT_1:16
.= (- 1) * y2 by A1, Lm5
.= - y2 by RLVECT_1:16 ;
hence  x1 - x2 = y1 - y2 by A1, Lm4; ::_thesis: verum
end;

theorem :: C0SP2:19
for X being non empty compact TopSpace
for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
proof
let X be non empty compact TopSpace; ::_thesis: for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X)
for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
let F, G, H be Point of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for f, g, h being RealMap of X st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
let f, g, h be RealMap of X; ::_thesis: ( f = F & g = G & h = H implies ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
A2: now__::_thesis:_(_H_=_F_-_G_implies_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)
assume  H = F - G ; ::_thesis: for x being Element of X holds h . x = (f . x) - (g . x)
then  H + G = F - (G - G) by RLVECT_1:29;
then  H + G = F - (0. (R_Normed_Algebra_of_ContinuousFunctions X)) by RLVECT_1:15;
then A3: H + G = F by RLVECT_1:13;
now__::_thesis:_for_x_being_Element_of_X_holds_(f_._x)_-_(g_._x)_=_h_._x
let x be Element of X; ::_thesis: (f . x) - (g . x) = h . x
 f . x = (h . x) + (g . x) by A1, A3, Th15;
hence  (f . x) - (g . x) = h . x ; ::_thesis: verum
end;
hence  for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)_implies_F_-_G_=_H_)
assume A4: for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: F - G = H
now__::_thesis:_for_x_being_Element_of_X_holds_(h_._x)_+_(g_._x)_=_f_._x
let x be Element of X; ::_thesis: (h . x) + (g . x) = f . x
 h . x = (f . x) - (g . x) by A4;
hence  (h . x) + (g . x) = f . x ; ::_thesis: verum
end;
then  F = H + G by A1, Th15;
then  F - G = H + (G - G) by RLVECT_1:def_3;
then  F - G = H + (0. (R_Normed_Algebra_of_ContinuousFunctions X)) by RLVECT_1:15;
hence  F - G = H by RLVECT_1:4; ::_thesis: verum
end;
hence  ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) by A2; ::_thesis: verum
end;

theorem Th20: :: C0SP2:20
for X being RealBanachSpace
for Y being Subset of X
for seq being 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; ::_thesis: for Y being Subset of X
for seq being 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 )
let Y be Subset of X; ::_thesis: for seq being 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 )
let seq be sequence of X; ::_thesis: ( Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm implies ( seq is convergent & lim seq in Y ) )
assume A1: ( Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm ) ; ::_thesis: ( seq is convergent & lim seq in Y )
hence  seq is convergent by LOPBAN_1:def_15; ::_thesis: lim seq in Y
hence  lim seq in Y by A1, NFCONT_1:def_3; ::_thesis: verum
end;

theorem Th21: :: C0SP2:21
for X being non empty compact TopSpace
for Y being Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = ContinuousFunctions X holds
Y is closed
proof
let X be non empty compact TopSpace; ::_thesis: for Y being Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = ContinuousFunctions X holds
Y is closed
let Y be Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( Y = ContinuousFunctions X implies Y is closed )
assume A1: Y = ContinuousFunctions X ; ::_thesis: Y is closed
now__::_thesis:_for_seq_being_sequence_of_(R_Normed_Algebra_of_BoundedFunctions_the_carrier_of_X)_st_rng_seq_c=_Y_&_seq_is_convergent_holds_
lim_seq_in_Y
let seq be sequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( rng seq c= Y & seq is convergent implies lim seq in Y )
assume A2: ( rng seq c= Y & seq is convergent ) ; ::_thesis: lim seq in Y
 lim seq in BoundedFunctions the carrier of X ;
then consider f being Function of the carrier of X,REAL such that
A3: ( f = lim seq & f | the carrier of X is bounded ) ;
now__::_thesis:_for_z_being_set_st_z_in_BoundedFunctions_the_carrier_of_X_holds_
z_in_PFuncs_(_the_carrier_of_X,REAL)
let z be set ; ::_thesis: ( z in BoundedFunctions the carrier of X implies z in PFuncs ( the carrier of X,REAL) )
assume  z in BoundedFunctions the carrier of X ; ::_thesis: z in PFuncs ( the carrier of X,REAL)
then  ex f being RealMap of X st
( f = z & f | the carrier of X is bounded ) ;
hence  z in PFuncs ( the carrier of X,REAL) by PARTFUN1:45; ::_thesis: verum
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:7;
A4: for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
proof
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p )
assume  p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
then consider k being Element of NAT  such that
A5: for n being Element of NAT st n >= k holds
||.((seq . n) - (lim seq)).|| < p by A2, NORMSP_1:def_7;
take  k ; ::_thesis: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
hereby  ::_thesis: verum
let n be Element of NAT ; ::_thesis: for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
let x be set ; ::_thesis: ( n >= k & x in the carrier of X implies abs (((H . n) . x) - (f . x)) < p )
assume A6: ( n >= k & x in the carrier of X ) ; ::_thesis: abs (((H . n) . x) - (f . x)) < p
then A7: ||.((seq . n) - (lim seq)).|| < p by A5;
 (seq . n) - (lim seq) in BoundedFunctions the carrier of X ;
then consider g being 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 being 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:34;
 abs (g . x0) <= ||.((seq . n) - (lim seq)).|| by A8, C0SP1:26;
hence  abs (((H . n) . x) - (f . x)) < p by A10, A9, A7, XXREAL_0:2; ::_thesis: verum
end;
end;
 f is continuous
proof
 for x being Point of X
for 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; ::_thesis: for 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 )
let V be Subset of REAL; ::_thesis: ( f . x in V & V is open implies ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
set r = f . x;
assume  ( f . x in V & V is open ) ; ::_thesis: ex W being Subset of X st
( x in W & W is open & f .: W c= V )
then consider r0 being real number  such that
A11: ( 0 < r0 & ].((f . x) - r0),((f . x) + r0).[ c= V ) by RCOMP_1:19;
consider k being Element of NAT  such that
A12: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < r0 / 3 by A4, A11, XREAL_1:222;
A13: abs (((H . k) . x) - (f . x)) < r0 / 3 by A12;
 k in NAT ;
then  k in dom seq by NORMSP_1:12;
then  H . k in rng seq by FUNCT_1:def_3;
then  H . k in Y by A2;
then consider h being continuous RealMap of X such that
A14: H . k = h by A1;
set r1 = h . x;
set G1 = ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[;
A15: h . x < (h . x) + (r0 / 3) by A11, XREAL_1:29, XREAL_1:222;
then  (h . x) - (r0 / 3) < h . x by XREAL_1:19;
then  h . x in ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ by A15;
then consider W1 being Subset of X such that
A16: ( x in W1 & W1 is open & h .: W1 c= ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ ) by Th1;
now__::_thesis:_for_x0_being_set_st_x0_in_f_.:_W1_holds_
x0_in_].((f_._x)_-_r0),((f_._x)_+_r0).[
let x0 be set ; ::_thesis: ( x0 in f .: W1 implies x0 in ].((f . x) - r0),((f . x) + r0).[ )
assume  x0 in f .: W1 ; ::_thesis: x0 in ].((f . x) - r0),((f . x) + r0).[
then consider z0 being set  such that
A17: ( z0 in dom f & z0 in W1 & f . z0 = x0 ) by FUNCT_1:def_6;
 h . z0 in h .: W1 by A17, FUNCT_2:35;
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:9;
then A18: abs ((h . z0) - (h . x)) <= r0 / 3 by ABSVALUE:5;
A19: abs (- ((h . x) - (f . x))) < r0 / 3 by A13, A14, COMPLEX1:52;
 abs ((h . z0) - (f . z0)) < r0 / 3 by A17, A12, A14;
then  abs (- ((h . z0) - (f . z0))) < r0 / 3 by COMPLEX1:52;
then  (abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x))) < (r0 / 3) + (r0 / 3) by A19, XREAL_1:8;
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:8;
 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:56;
 abs (((f . z0) - (h . z0)) - ((f . x) - (h . x))) <= (abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x))) by COMPLEX1:57;
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:6;
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:1;
then  ( (- r0) + (f . x) < ((f . z0) - (f . x)) + (f . x) & ((f . z0) - (f . x)) + (f . x) < r0 + (f . x) ) by XREAL_1:6;
hence  x0 in ].((f . x) - r0),((f . x) + r0).[ by A17; ::_thesis: verum
end;
then  f .: W1 c= ].((f . x) - r0),((f . x) + 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; ::_thesis: verum
end;
hence  f is continuous by Th1; ::_thesis: verum
end;
hence  lim seq in Y by A3, A1; ::_thesis: verum
end;
hence  Y is closed by NFCONT_1:def_3; ::_thesis: verum
end;

theorem Th22: :: C0SP2:22
for X being non empty compact TopSpace
for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X be non empty compact TopSpace; ::_thesis: for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
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:6;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((vseq1_._n)_-_(vseq1_._m)).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume A3: e > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
consider k being Element of NAT  such that
A4: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A3, RSSPACE3:8;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((vseq1_._n)_-_(vseq1_._m)).||_<_e
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume  ( n >= k & m >= k ) ; ::_thesis: ||.((vseq1 . n) - (vseq1 . m)).|| < e
then  ||.((vseq . n) - (vseq . m)).|| < e by A4;
hence  ||.((vseq1 . n) - (vseq1 . m)).|| < e by Lm9, Lm3; ::_thesis: verum
end;
hence  for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e ; ::_thesis: verum
end;
then A5: vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:8;
then A6: vseq1 is convergent by C0SP1:35;
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 being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e )
assume  e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e
then consider k being Element of NAT  such that
A8: for n being Element of NAT st n >= k holds
||.((vseq1 . n) - (lim vseq1)).|| < e by A6, NORMSP_1:def_7;
take  k ; ::_thesis: for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
||.((vseq_._n)_-_tv).||_<_e
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| < e )
assume  n >= k ; ::_thesis: ||.((vseq . n) - tv).|| < e
then  ||.((vseq1 . n) - (lim vseq1)).|| < e by A8;
hence  ||.((vseq . n) - tv).|| < e by Lm9, Lm3; ::_thesis: verum
end;
hence  for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e ; ::_thesis: verum
end;
hence  vseq is convergent by NORMSP_1:def_6; ::_thesis: verum
end;

registration
let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->  complete ;
coherence
 R_Normed_Algebra_of_ContinuousFunctions X is complete
proof
 for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th22;
hence  R_Normed_Algebra_of_ContinuousFunctions X is complete by LOPBAN_1:def_15; ::_thesis: verum
end;
end;

registration
let X be non empty compact TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->  Banach_Algebra-like ;
coherence
 R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like
proof
set B = R_Normed_Algebra_of_ContinuousFunctions X;
A1: now__::_thesis:_for_f,_g_being_Element_of_(R_Normed_Algebra_of_ContinuousFunctions_X)_holds_||.(f_*_g).||_<=_||.f.||_*_||.g.||
let f, g be Element of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
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:37;
hence  ||.(f * g).|| <= ||.f.|| * ||.g.|| by A2, LOPBAN_2:def_9; ::_thesis: verum
end;
A3: R_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_2 by C0SP1:37;
A4: ||.(1. (R_Normed_Algebra_of_ContinuousFunctions X)).|| = ||.(1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)).|| by Lm8, Lm3
.= 1 by A3, LOPBAN_2:def_10 ;
A5: now__::_thesis:_for_a_being_Real
for_f,_g_being_Element_of_(R_Normed_Algebra_of_ContinuousFunctions_X)_holds_a_*_(f_*_g)_=_f_*_(a_*_g)
let a be Real; ::_thesis: for f, g being Element of (R_Normed_Algebra_of_ContinuousFunctions X) holds a * (f * g) = f * (a * g)
let f, g be Element of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: a * (f * g) = f * (a * g)
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:37;
 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; ::_thesis: verum
end;
now__::_thesis:_for_f,_g,_h_being_Element_of_(R_Normed_Algebra_of_ContinuousFunctions_X)_holds_(g_+_h)_*_f_=_(g_*_f)_+_(h_*_f)
let f, g, h be Element of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: (g + h) * f = (g * f) + (h * f)
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:37;
thus (g + h) * f = (g1 + h1) * f1 by Lm6, A9
.= (g1 * f1) + (h1 * f1) by A11, VECTSP_1:def_3
.= (g * f) + (h * f) by Lm4, A10 ; ::_thesis: verum
end;
then  R_Normed_Algebra_of_ContinuousFunctions X is left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Algebra by A1, A4, A5, LOPBAN_2:def_9, LOPBAN_2:def_10, LOPBAN_2:def_11, VECTSP_1:def_3;
hence  R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like ; ::_thesis: verum
end;
end;

begin

theorem Th23: :: C0SP2:23
for X being non empty TopSpace
for f, g being RealMap of X holds support (f + g) c= (support f) \/ (support g)
proof
let X be non empty TopSpace; ::_thesis: for f, g being RealMap of X holds support (f + g) c= (support f) \/ (support g)
let f, g be RealMap of X; ::_thesis: support (f + g) c= (support f) \/ (support g)
set CX = the carrier of X;
reconsider h = f + g as RealMap of X ;
A1: ( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_(_the_carrier_of_X_\_(support_f))_/\_(_the_carrier_of_X_\_(support_g))_holds_
x_in_the_carrier_of_X_\_(support_(f_+_g))
let x be set ; ::_thesis: ( x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) implies x in the carrier of X \ (support (f + g)) )
assume A2: x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) ; ::_thesis: x in the carrier of X \ (support (f + g))
then  ( x in the carrier of X \ (support f) & x in the carrier of X \ (support g) ) by XBOOLE_0:def_4;
then  ( x in the carrier of X & not x in support f & x in the carrier of X & not x in support g ) by XBOOLE_0:def_5;
then A3: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def_7;
A4: (f + g) . x = 0 + 0 by A3, VALUED_1:1;
 not x in support (f + g) by A4, PRE_POLY:def_7;
hence  x in the carrier of X \ (support (f + g)) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
then  ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) c= the carrier of X \ (support (f + g)) by TARSKI:def_3;
then  the carrier of X \ ((support f) \/ (support g)) c= the carrier of X \ (support (f + g)) by XBOOLE_1:53;
then  the carrier of X \ ( the carrier of X \ (support (f + g))) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:34;
then  the carrier of X /\ (support (f + g)) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:48;
then  the carrier of X /\ (support (f + g)) c= the carrier of X /\ ((support f) \/ (support g)) by XBOOLE_1:48;
then  support (f + g) c= the carrier of X /\ ((support f) \/ (support g)) by A1, PRE_POLY:37, XBOOLE_1:28;
then  support (f + g) c= ( the carrier of X /\ (support f)) \/ ( the carrier of X /\ (support g)) by XBOOLE_1:23;
then  support (f + g) c= (support f) \/ ( the carrier of X /\ (support g)) by A1, PRE_POLY:37, XBOOLE_1:28;
hence  support (f + g) c= (support f) \/ (support g) by A1, PRE_POLY:37, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th24: :: C0SP2:24
for X being non empty TopSpace
for a being Real
for f being RealMap of X holds support (a (#) f) c= support f
proof
let X be non empty TopSpace; ::_thesis: for a being Real
for f being RealMap of X holds support (a (#) f) c= support f
let a be Real; ::_thesis: for f being RealMap of X holds support (a (#) f) c= support f
let f be RealMap of X; ::_thesis: support (a (#) f) c= support f
set CX = the carrier of X;
reconsider h = a (#) f as RealMap of X ;
now__::_thesis:_for_x_being_set_st_x_in_support_(a_(#)_f)_holds_
x_in_support_f
let x be set ; ::_thesis: ( x in support (a (#) f) implies x in support f )
assume  x in support (a (#) f) ; ::_thesis: x in support f
then  (a (#) f) . x <> 0 by PRE_POLY:def_7;
then A1: a * (f . x) <> 0 by VALUED_1:6;
 f . x <> 0 by A1;
hence  x in support f by PRE_POLY:def_7; ::_thesis: verum
end;
hence  support (a (#) f) c= support f by TARSKI:def_3; ::_thesis: verum
end;

theorem :: C0SP2:25
for X being non empty TopSpace
for f, g being RealMap of X holds support (f (#) g) c= (support f) \/ (support g)
proof
let X be non empty TopSpace; ::_thesis: for f, g being RealMap of X holds support (f (#) g) c= (support f) \/ (support g)
let f, g be RealMap of X; ::_thesis: support (f (#) g) c= (support f) \/ (support g)
set CX = the carrier of X;
reconsider h = f (#) g as RealMap of X ;
A1: ( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_(_the_carrier_of_X_\_(support_f))_/\_(_the_carrier_of_X_\_(support_g))_holds_
x_in_the_carrier_of_X_\_(support_(f_(#)_g))
let x be set ; ::_thesis: ( x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) implies x in the carrier of X \ (support (f (#) g)) )
assume A2: x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) ; ::_thesis: x in the carrier of X \ (support (f (#) g))
then  ( x in the carrier of X \ (support f) & x in the carrier of X \ (support g) ) by XBOOLE_0:def_4;
then  ( x in the carrier of X & not x in support f & x in the carrier of X & not x in support g ) by XBOOLE_0:def_5;
then A3: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def_7;
A4: (f (#) g) . x = 0 * 0 by A3, VALUED_1:5;
 not x in support (f (#) g) by A4, PRE_POLY:def_7;
hence  x in the carrier of X \ (support (f (#) g)) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
then  ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) c= the carrier of X \ (support (f (#) g)) by TARSKI:def_3;
then  the carrier of X \ ((support f) \/ (support g)) c= the carrier of X \ (support (f (#) g)) by XBOOLE_1:53;
then  the carrier of X \ ( the carrier of X \ (support (f (#) g))) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:34;
then  the carrier of X /\ (support (f (#) g)) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:48;
then  the carrier of X /\ (support (f (#) g)) c= the carrier of X /\ ((support f) \/ (support g)) by XBOOLE_1:48;
then  support (f (#) g) c= the carrier of X /\ ((support f) \/ (support g)) by A1, PRE_POLY:37, XBOOLE_1:28;
then  support (f (#) g) c= ( the carrier of X /\ (support f)) \/ ( the carrier of X /\ (support g)) by XBOOLE_1:23;
then  support (f (#) g) c= (support f) \/ ( the carrier of X /\ (support g)) by A1, PRE_POLY:37, XBOOLE_1:28;
hence  support (f (#) g) c= (support f) \/ (support g) by A1, PRE_POLY:37, XBOOLE_1:28; ::_thesis: verum
end;

begin

definition
let X be non empty TopSpace;
func C_0_Functions X ->  non empty Subset of (RealVectSpace the carrier of X) equals :: C0SP2:def 6
 {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  ;
correctness
coherence
{  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  is non empty Subset of (RealVectSpace the carrier of X);
proof
A1:  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  c= Funcs ( the carrier of X,REAL)
proof
 for x being set st x in  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  holds
x in Funcs ( the carrier of X,REAL)
proof
let x be set ; ::_thesis: ( x in  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  implies x in Funcs ( the carrier of X,REAL) )
assume  x in  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  ; ::_thesis: x in Funcs ( the carrier of X,REAL)
then  ex f being RealMap of X st
( x = f & f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) ;
hence  x in Funcs ( the carrier of X,REAL) by FUNCT_2:8; ::_thesis: verum
end;
hence   {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  c= Funcs ( the carrier of X,REAL) by TARSKI:def_3; ::_thesis: verum
end;
 not  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  is empty
proof
set g = the carrier of X --> 0;
reconsider g = the carrier of X --> 0 as RealMap of X by FUNCOP_1:46;
A2: g is continuous
proof
 for P being Subset of REAL st P is closed holds
g " P is closed
proof
let P be Subset of REAL; ::_thesis: ( P is closed implies g " P is closed )
assume  P is closed ; ::_thesis: g " P is closed
set F = the carrier of X --> 0;
set H = the carrier of X;
set HX = [#] X;
percases ( 0 in P or not 0 in P ) ;
suppose 0 in P ; ::_thesis: g " P is closed
then  g " P = [#] X by FUNCOP_1:14;
hence  g " P is closed ; ::_thesis: verum
end;
suppose not 0 in P ; ::_thesis: g " P is closed
then  ( the carrier of X --> 0) " P = {} X by FUNCOP_1:16;
hence  g " P is closed ; ::_thesis: verum
end;
end;
end;
hence  g is continuous by PSCOMP_1:def_3; ::_thesis: verum
end;
A3: ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support g holds
Cl A is Subset of Y ) )
proof
set S = the non empty compact Subset of X;
A4: for A being Subset of X st A = support g holds
Cl A is Subset of the non empty compact Subset of X
proof
let A be Subset of X; ::_thesis: ( A = support g implies Cl A is Subset of the non empty compact Subset of X )
assume A5: A = support g ; ::_thesis: Cl A is Subset of the non empty compact Subset of X
A6: A = {}
proof
assume A7: not A = {} ; ::_thesis: contradiction
set p = the Element of support g;
A8: the Element of support g in A by A7, A5;
 g . the Element of support g <> 0 by A5, A7, PRE_POLY:def_7;
hence  contradiction by A8, FUNCOP_1:7; ::_thesis: verum
end;
 Cl A = {} X by A6, PRE_TOPC:22;
hence  Cl A is Subset of the non empty compact Subset of X by XBOOLE_1:2; ::_thesis: verum
end;
thus  ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support g holds
Cl A is Subset of Y ) ) by A4; ::_thesis: verum
end;
 g in  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  by A2, A3;
hence  not  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  is empty ; ::_thesis: verum
end;
hence   {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  is non empty Subset of (RealVectSpace the carrier of X) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines C_0_Functions C0SP2:def_6_:_
 for X being non empty TopSpace holds C_0_Functions X =  {  f where f is RealMap of X : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )  }  ;

theorem :: C0SP2:26
for X being non empty TopSpace holds C_0_Functions X is non empty Subset of (RAlgebra the carrier of X) ;

Lm10:  for X being non empty TopSpace
for v, u being Element of (RAlgebra the carrier of X) st v in C_0_Functions X & u in C_0_Functions X holds
v + u in C_0_Functions X
proof
let X be non empty TopSpace; ::_thesis: for v, u being Element of (RAlgebra the carrier of X) st v in C_0_Functions X & u in C_0_Functions X holds
v + u in C_0_Functions X
set W = C_0_Functions X;
set V = RAlgebra the carrier of X;
let u, v be Element of (RAlgebra the carrier of X); ::_thesis: ( u in C_0_Functions X & v in C_0_Functions X implies u + v in C_0_Functions X )
assume A1: ( u in C_0_Functions X & v in C_0_Functions X ) ; ::_thesis: u + v in C_0_Functions X
consider u1 being RealMap of X such that
A2: ( u1 = u & u1 is continuous & ex Y1 being non empty Subset of X st
( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) ) by A1;
consider Y1 being non empty Subset of X such that
A3: ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) by A2;
consider v1 being RealMap of X such that
A4: ( v1 = v & v1 is continuous & ex Y2 being non empty Subset of X st
( Y2 is compact & ( for A2 being Subset of X st A2 = support v1 holds
Cl A2 is Subset of Y2 ) ) ) by A1;
consider Y2 being non empty Subset of X such that
A5: ( Y2 is compact & ( for A2 being Subset of X st A2 = support v1 holds
Cl A2 is Subset of Y2 ) ) by A4;
A6: u in ContinuousFunctions X by A2;
A7: v in ContinuousFunctions X by A4;
 v + u in ContinuousFunctions X by A6, A7, IDEAL_1:def_1;
then consider fvu being continuous RealMap of X such that
A8: v + u = fvu ;
A9: Y1 \/ Y2 is compact by A3, A5, COMPTS_1:10;
A10: ( dom u1 = the carrier of X & dom v1 = the carrier of X ) by FUNCT_2:def_1;
reconsider A1 = support u1, A2 = support v1 as Subset of X by A10, PRE_POLY:37;
A11: (dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def_1
.= the carrier of X /\ the carrier of X by FUNCT_2:def_1
.= the carrier of X ;
A12: dom (v1 + u1) = (dom v1) /\ (dom u1) by VALUED_1:def_1;
reconsider A1 = support u1, A2 = support v1 as Subset of X by A10, PRE_POLY:37;
reconsider A3 = support (v1 + u1) as Subset of X by A12, A11, PRE_POLY:37;
 Cl A3 c= Cl (A2 \/ A1) by Th23, PRE_TOPC:19;
then A13: Cl A3 c= (Cl A2) \/ (Cl A1) by PRE_TOPC:20;
A14: Cl A1 is Subset of Y1 by A3;
 Cl A2 is Subset of Y2 by A5;
then  (Cl A2) \/ (Cl A1) c= Y2 \/ Y1 by A14, XBOOLE_1:13;
then A15: for A3 being Subset of X st A3 = support (v1 + u1) holds
Cl A3 is Subset of (Y2 \/ Y1) by A13, XBOOLE_1:1;
reconsider vv1 = v as Element of Funcs ( the carrier of X,REAL) ;
reconsider uu1 = u as Element of Funcs ( the carrier of X,REAL) ;
reconsider fvu1 = v + u as Element of Funcs ( the carrier of X,REAL) ;
A16: dom fvu1 = the carrier of X by FUNCT_2:def_1;
 for c being set st c in dom fvu1 holds
fvu1 . c = (v1 . c) + (u1 . c) by A2, A4, FUNCSDOM:1;
then  fvu1 = v1 + u1 by A16, A11, VALUED_1:def_1;
hence  u + v in C_0_Functions X by A8, A9, A15; ::_thesis: verum
end;

Lm11:  for X being non empty TopSpace
for a being Real
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
a * u in C_0_Functions X
proof
let X be non empty TopSpace; ::_thesis: for a being Real
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
a * u in C_0_Functions X
set W = C_0_Functions X;
set V = RAlgebra the carrier of X;
let a be Real; ::_thesis: for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
a * u in C_0_Functions X
let u be Element of (RAlgebra the carrier of X); ::_thesis: ( u in C_0_Functions X implies a * u in C_0_Functions X )
assume A1: u in C_0_Functions X ; ::_thesis: a * u in C_0_Functions X
consider u1 being RealMap of X such that
A2: ( u1 = u & u1 is continuous & ex Y1 being non empty Subset of X st
( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) ) by A1;
consider Y1 being non empty Subset of X such that
A3: ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) by A2;
A4: u in ContinuousFunctions X by A2;
 a * u in ContinuousFunctions X by A4, C0SP1:def_10;
then consider fau being continuous RealMap of X such that
A5: fau = a * u ;
A6: dom u1 = the carrier of X by FUNCT_2:def_1;
then reconsider A1 = support u1 as Subset of X by PRE_POLY:37;
A7: dom u1 = the carrier of X by FUNCT_2:def_1;
A8: dom (a (#) u1) = dom u1 by VALUED_1:def_5;
reconsider A1 = support u1 as Subset of X by A6, PRE_POLY:37;
reconsider A3 = support (a (#) u1) as Subset of X by A8, A7, PRE_POLY:37;
A9: Cl A1 is Subset of Y1 by A3;
 Cl A3 c= Cl A1 by Th24, PRE_TOPC:19;
then A10: for A3 being Subset of X st A3 = support (a (#) u1) holds
Cl A3 is Subset of Y1 by A9, XBOOLE_1:1;
reconsider uu1 = u as Element of Funcs ( the carrier of X,REAL) ;
reconsider fau1 = a * u as Element of Funcs ( the carrier of X,REAL) ;
A11: dom fau1 = the carrier of X by FUNCT_2:def_1;
A12: dom u1 = the carrier of X by FUNCT_2:def_1;
 for c being set st c in dom fau1 holds
fau1 . c = a * (u1 . c) by A2, FUNCSDOM:4;
then  fau1 = a (#) u1 by A11, A12, VALUED_1:def_5;
hence  a * u in C_0_Functions X by A3, A10, A5; ::_thesis: verum
end;

Lm12:  for X being non empty TopSpace
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
- u in C_0_Functions X
proof
let X be non empty TopSpace; ::_thesis: for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
- u in C_0_Functions X
set W = C_0_Functions X;
set V = RAlgebra the carrier of X;
let u be Element of (RAlgebra the carrier of X); ::_thesis: ( u in C_0_Functions X implies - u in C_0_Functions X )
assume A1: u in C_0_Functions X ; ::_thesis: - u in C_0_Functions X
set a = - 1;
 RAlgebra the carrier of X is RealLinearSpace by C0SP1:7;
then  - u = (- 1) * u by RLVECT_1:16;
hence  - u in C_0_Functions X by Lm11, A1; ::_thesis: verum
end;

theorem :: C0SP2:27
for X being non empty TopSpace
for W being non empty Subset of (RAlgebra the carrier of X) st W = C_0_Functions X holds
W is additively-linearly-closed
proof
let X be non empty TopSpace; ::_thesis: for W being non empty Subset of (RAlgebra the carrier of X) st W = C_0_Functions X holds
W is additively-linearly-closed
let W be non empty Subset of (RAlgebra the carrier of X); ::_thesis: ( W = C_0_Functions X implies W is additively-linearly-closed )
assume A1: W = C_0_Functions X ; ::_thesis: W is additively-linearly-closed
set V = RAlgebra the carrier of X;
 for v, u being Element of (RAlgebra the carrier of X) st v in W & u in W holds
v + u in W by A1, Lm10;
then A2: W is add-closed by IDEAL_1:def_1;
 for v being Element of (RAlgebra the carrier of X) st v in W holds
- v in W by A1, Lm12;
then A3: W is having-inverse by C0SP1:def_1;
 for a being Real
for u being Element of (RAlgebra the carrier of X) st u in W holds
a * u in W by A1, Lm11;
hence  W is additively-linearly-closed by A2, A3, C0SP1:def_10; ::_thesis: verum
end;

theorem Th28: :: C0SP2:28
for X being non empty TopSpace holds C_0_Functions X is linearly-closed
proof
let X be non empty TopSpace; ::_thesis: C_0_Functions X is linearly-closed
set Y = C_0_Functions X;
set V = RealVectSpace the carrier of X;
A1: for v, u being VECTOR of (RealVectSpace the carrier of X) st v in C_0_Functions X & u in C_0_Functions X holds
v + u in C_0_Functions X
proof
let v, u be VECTOR of (RealVectSpace the carrier of X); ::_thesis: ( v in C_0_Functions X & u in C_0_Functions X implies v + u in C_0_Functions X )
assume A2: ( v in C_0_Functions X & u in C_0_Functions X ) ; ::_thesis: v + u in C_0_Functions X
reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,REAL) ;
reconsider v2 = v, u2 = u as VECTOR of (RAlgebra the carrier of X) ;
 v2 + u2 in C_0_Functions X by A2, Lm10;
hence  v + u in C_0_Functions X ; ::_thesis: verum
end;
 for a being Real
for v being Element of (RealVectSpace the carrier of X) st v in C_0_Functions X holds
a * v in C_0_Functions X
proof
let a be Real; ::_thesis: for v being Element of (RealVectSpace the carrier of X) st v in C_0_Functions X holds
a * v in C_0_Functions X
let v be VECTOR of (RealVectSpace the carrier of X); ::_thesis: ( v in C_0_Functions X implies a * v in C_0_Functions X )
assume A3: v in C_0_Functions X ; ::_thesis: a * v in C_0_Functions X
reconsider v1 = v as Element of Funcs ( the carrier of X,REAL) ;
reconsider v2 = v as VECTOR of (RAlgebra the carrier of X) ;
 a * v2 in C_0_Functions X by A3, Lm11;
hence  a * v in C_0_Functions X ; ::_thesis: verum
end;
hence  C_0_Functions X is linearly-closed by A1, RLSUB_1:def_1; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster C_0_Functions X ->  non empty linearly-closed ;
correctness
coherence
( not C_0_Functions X is empty & C_0_Functions X is linearly-closed );
by Th28;
end;

definition
let X be non empty TopSpace;
func R_VectorSpace_of_C_0_Functions X ->  RealLinearSpace equals :: C0SP2:def 7
 RLSStruct(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))) #);
correctness
coherence
RLSStruct(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))) #) is RealLinearSpace;
by RSSPACE:11;
end;

:: deftheorem  defines R_VectorSpace_of_C_0_Functions C0SP2:def_7_:_
 for X being non empty TopSpace holds R_VectorSpace_of_C_0_Functions X = RLSStruct(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))) #);

theorem :: C0SP2:29
for X being non empty TopSpace holds R_VectorSpace_of_C_0_Functions X is Subspace of RealVectSpace the carrier of X by RSSPACE:11;

theorem Th30: :: C0SP2:30
for X being non empty TopSpace
for x being set st x in C_0_Functions X holds
x in BoundedFunctions the carrier of X
proof
let X be non empty TopSpace; ::_thesis: for x being set st x in C_0_Functions X holds
x in BoundedFunctions the carrier of X
let x be set ; ::_thesis: ( x in C_0_Functions X implies x in BoundedFunctions the carrier of X )
assume A1: x in C_0_Functions X ; ::_thesis: x in BoundedFunctions the carrier of X
consider f being RealMap of X such that
A2: ( f = x & f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) by A1;
consider Y being non empty Subset of X such that
A3: ( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) by A2;
 dom f = the carrier of X by FUNCT_2:def_1;
then reconsider A = support f as Subset of X by PRE_POLY:37;
reconsider Y1 = f .: Y as non empty real-bounded Subset of REAL by A2, A3, JORDAN_A:1, RCOMP_1:10;
A4: Y1 c= [.(inf Y1),(sup Y1).] by XXREAL_2:69;
reconsider r1 = inf Y1, r2 = sup Y1 as real number ;
consider r being real number  such that
A5: r = ((abs r1) + (abs r2)) + 1 ;
 for p being Element of Y holds
( r > 0 & - r < f . p & f . p < r )
proof
let p be Element of Y; ::_thesis: ( r > 0 & - r < f . p & f . p < r )
 f . p in Y1 by FUNCT_2:35;
then  f . p in [.r1,r2.] by A4;
then consider r3 being Element of REAL  such that
A6: ( r3 = f . p & r1 <= r3 & r3 <= r2 ) ;
A7: ( abs r1 >= 0 & abs r2 >= 0 ) by COMPLEX1:46;
 - (abs r1) <= r1 by ABSVALUE:4;
then  (- (abs r1)) - (abs r2) <= r1 - 0 by A7, XREAL_1:13;
then  ((- (abs r1)) - (abs r2)) - 1 < r1 - 0 by XREAL_1:15;
then A8: - r < r1 by A5;
 r2 <= abs r2 by ABSVALUE:4;
then  r2 + 0 <= (abs r2) + (abs r1) by A7, XREAL_1:7;
then  r2 < r by A5, XREAL_1:8;
hence  ( r > 0 & - r < f . p & f . p < r ) by A6, A8, XXREAL_0:2; ::_thesis: verum
end;
then consider r being real number  such that
A9: for p being Element of Y holds
( r > 0 & - r < f . p & f . p < r ) ;
 for x being Point of X holds
( - r < f . x & f . x < r )
proof
let x be Point of X; ::_thesis: ( - r < f . x & f . x < r )
percases ( x in the carrier of X \ Y or x in Y ) by XBOOLE_0:def_5;
supposeA10: x in the carrier of X \ Y ; ::_thesis: ( - r < f . x & f . x < r )
A11: Cl A is Subset of Y by A3;
 support f c= Cl A by PRE_TOPC:18;
then  support f c= Y by A11, XBOOLE_1:1;
then  not x in support f by A10, XBOOLE_0:def_5;
then A12: f . x = 0 by PRE_POLY:def_7;
 (- 1) * r < (- 1) * 0 by A9, XREAL_1:69;
hence  ( - r < f . x & f . x < r ) by A12; ::_thesis: verum
end;
suppose x in Y ; ::_thesis: ( - r < f . x & f . x < r )
hence  ( - r < f . x & f . x < r ) by A9; ::_thesis: verum
end;
end;
end;
then consider s1 being real number  such that
A13: for x being Point of X holds
( - s1 < f . x & f . x < s1 ) ;
 for y being set st y in the carrier of X /\ (dom f) holds
f . y <= s1 by A13;
then A14: f | the carrier of X is bounded_above by RFUNCT_1:70;
 for y being set st y in the carrier of X /\ (dom f) holds
- s1 <= f . y by A13;
then A15: f | the carrier of X is bounded_below by RFUNCT_1:71;
 the carrier of X /\ the carrier of X = the carrier of X ;
then  f | the carrier of X is bounded by A14, A15, RFUNCT_1:75;
hence  x in BoundedFunctions the carrier of X by A2; ::_thesis: verum
end;

definition
let X be non empty TopSpace;
func C_0_FunctionsNorm X ->  Function of (C_0_Functions X),REAL equals :: C0SP2:def 8
(BoundedFunctionsNorm the carrier of X) | (C_0_Functions X);
correctness
coherence
(BoundedFunctionsNorm the carrier of X) | (C_0_Functions X) is Function of (C_0_Functions X),REAL;
proof
 for x being set st x in C_0_Functions X holds
x in BoundedFunctions the carrier of X by Th30;
then  C_0_Functions X c= BoundedFunctions the carrier of X by TARSKI:def_3;
hence  (BoundedFunctionsNorm the carrier of X) | (C_0_Functions X) is Function of (C_0_Functions X),REAL by FUNCT_2:32; ::_thesis: verum
end;
end;

:: deftheorem  defines C_0_FunctionsNorm C0SP2:def_8_:_
 for X being non empty TopSpace holds C_0_FunctionsNorm X = (BoundedFunctionsNorm the carrier of X) | (C_0_Functions X);

definition
let X be non empty TopSpace;
func R_Normed_Space_of_C_0_Functions X ->  non empty NORMSTR  equals :: C0SP2:def 9
 NORMSTR(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(C_0_FunctionsNorm X) #);
correctness
coherence
NORMSTR(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(C_0_FunctionsNorm X) #) is non empty NORMSTR ;
;
end;

:: deftheorem  defines R_Normed_Space_of_C_0_Functions C0SP2:def_9_:_
 for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X = NORMSTR(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(C_0_FunctionsNorm X) #);

registration
let X be non empty TopSpace;
cluster R_Normed_Space_of_C_0_Functions X ->  non empty strict ;
correctness
coherence
( R_Normed_Space_of_C_0_Functions X is strict & not R_Normed_Space_of_C_0_Functions X is empty );
;
end;

theorem :: C0SP2:31
for X being non empty TopSpace
for x being set st x in C_0_Functions X holds
x in ContinuousFunctions X
proof
let X be non empty TopSpace; ::_thesis: for x being set st x in C_0_Functions X holds
x in ContinuousFunctions X
let x be set ; ::_thesis: ( x in C_0_Functions X implies x in ContinuousFunctions X )
assume A1: x in C_0_Functions X ; ::_thesis: x in ContinuousFunctions X
consider f being RealMap of X such that
A2: ( f = x & f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) by A1;
thus  x in ContinuousFunctions X by A2; ::_thesis: verum
end;

theorem Th32: :: C0SP2:32
for X being non empty TopSpace holds 0. (R_VectorSpace_of_C_0_Functions X) = X --> 0
proof
let X be non empty TopSpace; ::_thesis: 0. (R_VectorSpace_of_C_0_Functions X) = X --> 0
A1: R_VectorSpace_of_C_0_Functions X is Subspace of RealVectSpace the carrier of X by RSSPACE:11;
 0. (RealVectSpace the carrier of X) = X --> 0 ;
hence  0. (R_VectorSpace_of_C_0_Functions X) = X --> 0 by A1, RLSUB_1:11; ::_thesis: verum
end;

theorem Th33: :: C0SP2:33
for X being non empty TopSpace holds 0. (R_Normed_Space_of_C_0_Functions X) = X --> 0
proof
let X be non empty TopSpace; ::_thesis: 0. (R_Normed_Space_of_C_0_Functions X) = X --> 0
0. (R_Normed_Space_of_C_0_Functions X) = 0. (R_VectorSpace_of_C_0_Functions X)
.= X --> 0 by Th32 ;
hence  0. (R_Normed_Space_of_C_0_Functions X) = X --> 0 ; ::_thesis: verum
end;

Lm13:  for X being non empty TopSpace
for x1, x2 being Point of (R_Normed_Space_of_C_0_Functions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
proof
let X be non empty TopSpace; ::_thesis: for x1, x2 being Point of (R_Normed_Space_of_C_0_Functions X)
for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let x1, x2 be Point of (R_Normed_Space_of_C_0_Functions X); ::_thesis: for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
let y1, y2 be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 + x2 = y1 + y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 + x2 = y1 + y2
thus x1 + x2 = ( the addF of (RealVectSpace the carrier of X) || (C_0_Functions X)) . [x1,x2] by RSSPACE:def_8
.= the addF of (RAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49
.= ( the addF of (RAlgebra the carrier of X) || (BoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49
.= y1 + y2 by C0SP1:def_5 ; ::_thesis: verum
end;

Lm14:  for X being non empty TopSpace
for a being Real
for x being Point of (R_Normed_Space_of_C_0_Functions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
proof
let X be non empty TopSpace; ::_thesis: for a being Real
for x being Point of (R_Normed_Space_of_C_0_Functions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let a be Real; ::_thesis: for x being Point of (R_Normed_Space_of_C_0_Functions X)
for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let x be Point of (R_Normed_Space_of_C_0_Functions X); ::_thesis: for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let y be Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; ::_thesis: a * x = a * y
thus a * x = ( the Mult of (RAlgebra the carrier of X) | [:REAL,(C_0_Functions X):]) . [a,x] by RSSPACE:def_9
.= the Mult of (RAlgebra the carrier of X) . [a,x] by FUNCT_1:49
.= ( the Mult of (RAlgebra the carrier of X) | [:REAL,(BoundedFunctions the carrier of X):]) . [a,y] by A1, FUNCT_1:49
.= a * y by C0SP1:def_11 ; ::_thesis: verum
end;

theorem Th34: :: C0SP2:34
for a being Real
for X being non empty TopSpace
for F, G being Point of (R_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
proof
let a be Real; ::_thesis: for X being non empty TopSpace
for F, G being Point of (R_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let X be non empty TopSpace; ::_thesis: for F, G being Point of (R_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_Normed_Space_of_C_0_Functions X); ::_thesis: ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
A1: ( ||.F.|| = 0 iff F = 0. (R_Normed_Space_of_C_0_Functions X) )
proof
reconsider FB = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;
A2: 0. (R_Normed_Space_of_C_0_Functions X) = X --> 0 by Th33;
 ( ||.FB.|| = 0 iff FB = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by C0SP1:32;
hence  ( ||.F.|| = 0 iff F = 0. (R_Normed_Space_of_C_0_Functions X) ) by A2, C0SP1:25, FUNCT_1:49; ::_thesis: verum
end;
A3: ||.(a * F).|| = (abs a) * ||.F.||
proof
reconsider FB = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;
A4: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A5: a * FB = a * F by Lm14;
reconsider aFB = a * FB as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = a * F as Point of (R_Normed_Space_of_C_0_Functions X) ;
 ||.aFB.|| = ||.aF.|| by A5, FUNCT_1:49;
hence  ||.(a * F).|| = (abs a) * ||.F.|| by A4, C0SP1:32; ::_thesis: verum
end;
 ||.(F + G).|| <= ||.F.|| + ||.G.||
proof
reconsider FB = F, GB = G as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th30;
A6: ( ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| ) by FUNCT_1:49;
 FB + GB = F + G by Lm13;
then A7: ||.(FB + GB).|| = ||.(F + G).|| by FUNCT_1:49;
reconsider aFB = FB + GB as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = F, aG = G as Point of (R_Normed_Space_of_C_0_Functions X) ;
thus  ||.(F + G).|| <= ||.F.|| + ||.G.|| by A7, A6, C0SP1:32; ::_thesis: verum
end;
hence  ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A3; ::_thesis: verum
end;

theorem Th35: :: C0SP2:35
for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X is RealNormSpace-like
proof
let X be non empty TopSpace; ::_thesis: R_Normed_Space_of_C_0_Functions X is RealNormSpace-like
 for x, y being Point of (R_Normed_Space_of_C_0_Functions X)
for a being Real holds
( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th34;
hence  R_Normed_Space_of_C_0_Functions X is RealNormSpace-like by NORMSP_1:def_1; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster R_Normed_Space_of_C_0_Functions X ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
 ( R_Normed_Space_of_C_0_Functions X is reflexive & R_Normed_Space_of_C_0_Functions X is discerning & R_Normed_Space_of_C_0_Functions X is RealNormSpace-like & R_Normed_Space_of_C_0_Functions X is vector-distributive & R_Normed_Space_of_C_0_Functions X is scalar-distributive & R_Normed_Space_of_C_0_Functions X is scalar-associative & R_Normed_Space_of_C_0_Functions X is scalar-unital & R_Normed_Space_of_C_0_Functions X is Abelian & R_Normed_Space_of_C_0_Functions X is add-associative & R_Normed_Space_of_C_0_Functions X is right_zeroed & R_Normed_Space_of_C_0_Functions X is right_complementable )
proof
A1: R_VectorSpace_of_C_0_Functions X is RealLinearSpace ;
A2: for x being Point of (R_Normed_Space_of_C_0_Functions X) st ||.x.|| = 0 holds
x = 0. (R_Normed_Space_of_C_0_Functions X) by Th34;
 ||.(0. (R_Normed_Space_of_C_0_Functions X)).|| = 0 by Th34;
hence  ( R_Normed_Space_of_C_0_Functions X is reflexive & R_Normed_Space_of_C_0_Functions X is discerning & R_Normed_Space_of_C_0_Functions X is RealNormSpace-like & R_Normed_Space_of_C_0_Functions X is vector-distributive & R_Normed_Space_of_C_0_Functions X is scalar-distributive & R_Normed_Space_of_C_0_Functions X is scalar-associative & R_Normed_Space_of_C_0_Functions X is scalar-unital & R_Normed_Space_of_C_0_Functions X is Abelian & R_Normed_Space_of_C_0_Functions X is add-associative & R_Normed_Space_of_C_0_Functions X is right_zeroed & R_Normed_Space_of_C_0_Functions X is right_complementable ) by A1, A2, Th35, NORMSP_0:def_5, NORMSP_0:def_6, RSSPACE3:2; ::_thesis: verum
end;
end;

theorem :: C0SP2:36
for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X is RealNormSpace ;