:: Banach Algebra of Bounded Functionals
:: by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;
attr V1 is having-inverse means :Rdef210b: :: C0SP1:def 1
for v being Element of V st v in V1 holds
- v in V1;

end;

:: deftheorem Rdef210b defines having-inverse C0SP1:def 1 :

for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is having-inverse iff for v being Element of V st v in V1 holds
- v in V1 );

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;
attr V1 is additively-closed means :Rdef210: :: C0SP1:def 2
( V1 is add-closed & V1 is having-inverse );

end;

:: deftheorem Rdef210 defines additively-closed C0SP1:def 2 :

for V being non empty addLoopStr
for V1 being Subset of V holds
( V1 is additively-closed iff ( V1 is add-closed & V1 is having-inverse ) );

Cor1: for V being non empty addLoopStr holds [#] V is add-closed

proof end;

Cor2: for V being non empty addLoopStr holds [#] V is having-inverse

proof end;

registration

let V be non empty addLoopStr ;
cluster [#] V -> add-closed having-inverse ;
correctness
coherence
( [#] V is add-closed & [#] V is having-inverse );
by Cor1, Cor2;

end;

registration

let V be non empty doubleLoopStr ;
cluster additively-closed -> add-closed having-inverse Element of bool the carrier of V;
coherence
for b₁ being Subset of V st b₁ is additively-closed holds
( b₁ is add-closed & b₁ is having-inverse ) by Rdef210;
cluster add-closed having-inverse -> additively-closed Element of bool the carrier of V;
coherence
for b₁ being Subset of V st b₁ is add-closed & b₁ is having-inverse holds
b₁ is additively-closed by Rdef210;

end;

registration

let V be non empty addLoopStr ;
cluster non empty add-closed having-inverse Element of bool the carrier of V;
correctness
existence
ex b₁ being Subset of V st
( b₁ is add-closed & b₁ is having-inverse & not b₁ is empty );

proof end;

end;

definition

let V be Ring;
mode Subring of V -> Ring means :DefSubRing: :: C0SP1:def 3
( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & 1. it = 1. V & 0. it = 0. V );
existence
ex b₁ being Ring st
( the carrier of b₁ c= the carrier of V & the addF of b₁ = the addF of V || the carrier of b₁ & the multF of b₁ = the multF of V || the carrier of b₁ & 1. b₁ = 1. V & 0. b₁ = 0. V )

proof end;

end;

:: deftheorem DefSubRing defines Subring C0SP1:def 3 :

for V, b₂ being Ring holds
( b₂ is Subring of V iff ( the carrier of b₂ c= the carrier of V & the addF of b₂ = the addF of V || the carrier of b₂ & the multF of b₂ = the multF of V || the carrier of b₂ & 1. b₂ = 1. V & 0. b₂ = 0. V ) );

theorem Th01: :: C0SP1:1

for X being non empty set
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V

proof end;

registration

let V be Ring;
cluster strict Subring of V;
existence
ex b₁ being Subring of V st b₁ is strict

proof end;

end;

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
attr V1 is multiplicatively-closed means :Rdef200: :: C0SP1:def 4
( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds
v * u in V1 ) );

end;

:: deftheorem Rdef200 defines multiplicatively-closed C0SP1:def 4 :

for V being non empty multLoopStr_0
for V1 being Subset of V holds
( V1 is multiplicatively-closed iff ( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds
v * u in V1 ) ) );

definition

let V be non empty addLoopStr ;
let V1 be Subset of V;
assume A1: ( V1 is add-closed & not V1 is empty ) ;
func Add_ V1,V -> BinOp of V1 equals :Rdef211: :: C0SP1:def 5
the addF of V || V1;
correctness
coherence
the addF of V || V1 is BinOp of V1;

proof end;

end;

:: deftheorem Rdef211 defines Add_ C0SP1:def 5 :

for V being non empty addLoopStr
for V1 being Subset of V st V1 is add-closed & not V1 is empty holds
Add_ V1,V = the addF of V || V1;

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;
func mult_ V1,V -> BinOp of V1 equals :Rdef220: :: C0SP1:def 6
the multF of V || V1;
correctness
coherence
the multF of V || V1 is BinOp of V1;

proof end;

end;

:: deftheorem Rdef220 defines mult_ C0SP1:def 6 :

for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
mult_ V1,V = the multF of V || V1;

definition

let V be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V1 be Subset of V;
assume A1: ( V1 is add-closed & V1 is having-inverse & not V1 is empty ) ;
func Zero_ V1,V -> Element of V1 equals :Rdef213: :: C0SP1:def 7
0. V;
correctness
coherence
0. V is Element of V1;

proof end;

end;

:: deftheorem Rdef213 defines Zero_ C0SP1:def 7 :

for V being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V1 being Subset of V st V1 is add-closed & V1 is having-inverse & not V1 is empty holds
Zero_ V1,V = 0. V;

definition

let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
assume A1: ( V1 is multiplicatively-closed & not V1 is empty ) ;
func One_ V1,V -> Element of V1 equals :Rdef214: :: C0SP1:def 8
1. V;
correctness
coherence
1. V is Element of V1;
by A1, Rdef200;

end;

:: deftheorem Rdef214 defines One_ C0SP1:def 8 :

for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
One_ V1,V = 1. V;

theorem :: C0SP1:2

for V being Ring
for V1 being Subset of V st V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty holds
doubleLoopStr(# V1,(Add_ V1,V),(mult_ V1,V),(One_ V1,V),(Zero_ V1,V) #) is Ring

proof end;

definition

let V be Algebra;
mode Subalgebra of V -> Algebra means :DefSubAlg: :: C0SP1:def 9
( the carrier of it c= the carrier of V & the addF of it = the addF of V || the carrier of it & the multF of it = the multF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL ,the carrier of it:] & 1. it = 1. V & 0. it = 0. V );
existence
ex b₁ being Algebra st
( the carrier of b₁ c= the carrier of V & the addF of b₁ = the addF of V || the carrier of b₁ & the multF of b₁ = the multF of V || the carrier of b₁ & the Mult of b₁ = the Mult of V | [:REAL ,the carrier of b₁:] & 1. b₁ = 1. V & 0. b₁ = 0. V )

proof end;

end;

:: deftheorem DefSubAlg defines Subalgebra C0SP1:def 9 :

for V, b₂ being Algebra holds
( b₂ is Subalgebra of V iff ( the carrier of b₂ c= the carrier of V & the addF of b₂ = the addF of V || the carrier of b₂ & the multF of b₂ = the multF of V || the carrier of b₂ & the Mult of b₂ = the Mult of V | [:REAL ,the carrier of b₂:] & 1. b₂ = 1. V & 0. b₂ = 0. V ) );

theorem Th02: :: C0SP1:3

for X being non empty set
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL ,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V

proof end;

registration

let V be Algebra;
cluster strict Subalgebra of V;
existence
ex b₁ being Subalgebra of V st b₁ is strict

proof end;

end;

definition

let V be Algebra;
let V1 be Subset of V;
attr V1 is additively-linearly-closed means :def210: :: C0SP1:def 10
( V1 is add-closed & V1 is having-inverse & ( for a being Real
for v being Element of V st v in V1 holds
a * v in V1 ) );

end;

:: deftheorem def210 defines additively-linearly-closed C0SP1:def 10 :

for V being Algebra
for V1 being Subset of V holds
( V1 is additively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Real
for v being Element of V st v in V1 holds
a * v in V1 ) ) );

registration

let V be Algebra;
cluster additively-linearly-closed -> additively-closed Element of bool the carrier of V;
coherence
for b₁ being Subset of V st b₁ is additively-linearly-closed holds
b₁ is additively-closed

proof end;

end;

definition

let V be Algebra;
let V1 be Subset of V;
assume A1: ( V1 is additively-linearly-closed & not V1 is empty ) ;
func Mult_ V1,V -> Function of [:REAL ,V1:],V1 equals :def212: :: C0SP1:def 11
the Mult of V | [:REAL ,V1:];
correctness
coherence
the Mult of V | [:REAL ,V1:] is Function of [:REAL ,V1:],V1;

proof end;

end;

:: deftheorem def212 defines Mult_ C0SP1:def 11 :

for V being Algebra
for V1 being Subset of V st V1 is additively-linearly-closed & not V1 is empty holds
Mult_ V1,V = the Mult of V | [:REAL ,V1:];

definition

let V be non empty RLSStruct ;
attr V is scalar-mult-cancelable means :DefSMC: :: C0SP1:def 12
for a being Real
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V );

end;

:: deftheorem DefSMC defines scalar-mult-cancelable C0SP1:def 12 :

for V being non empty RLSStruct holds
( V is scalar-mult-cancelable iff for a being Real
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V ) );

theorem RLVECT123: :: C0SP1:4

for V being non empty right_complementable add-associative right_zeroed Algebra-like AlgebraStr
for a being Real holds a * (0. V) = 0. V

proof end;

theorem :: C0SP1:5

for V being non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr st V is scalar-mult-cancelable holds
V is RealLinearSpace

proof end;

LmAlgebra: for V being non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds
V is RealLinearSpace

proof end;

theorem Th03: :: C0SP1:6

for V being Algebra
for V1 being Subset of V st V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty holds
AlgebraStr(# V1,(mult_ V1,V),(Add_ V1,V),(Mult_ V1,V),(One_ V1,V),(Zero_ V1,V) #) is Subalgebra of V

proof end;

registration

let X be non empty set ;
cluster RAlgebra X -> right_complementable Abelian add-associative right_zeroed Algebra-like associative commutative right-distributive right_unital ;
correctness
coherence
( RAlgebra X is Abelian & RAlgebra X is add-associative & RAlgebra X is right_zeroed & RAlgebra X is right_complementable & RAlgebra X is commutative & RAlgebra X is associative & RAlgebra X is right_unital & RAlgebra X is right-distributive & RAlgebra X is Algebra-like );
by FUNCSDOM:50;

end;

theorem LmAlgebra2: :: C0SP1:7

for X being non empty set holds RAlgebra X is RealLinearSpace

proof end;

theorem RLSUB121: :: C0SP1:8

for V being Algebra
for V1 being Subalgebra of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & ( for v1 being Element of V1
for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

proof end;

definition

let X be non empty set ;
func BoundedFunctions X -> non empty Subset of (RAlgebra X) equals :: C0SP1:def 13
{ f where f is Function of X, REAL : f | X is bounded } ;
correctness
coherence
{ f where f is Function of X, REAL : f | X is bounded } is non empty Subset of (RAlgebra X);

proof end;

end;

:: deftheorem defines BoundedFunctions C0SP1:def 13 :

for X being non empty set holds BoundedFunctions X = { f where f is Function of X, REAL : f | X is bounded } ;

theorem ThB7: :: C0SP1:9

for X being non empty set holds
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )

proof end;

registration

let X be non empty set ;
cluster BoundedFunctions X -> non empty multiplicatively-closed additively-linearly-closed ;
coherence
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed ) by ThB7;

end;

theorem :: C0SP1:10

for X being non empty set holds AlgebraStr(# (BoundedFunctions X),(mult_ (BoundedFunctions X),(RAlgebra X)),(Add_ (BoundedFunctions X),(RAlgebra X)),(Mult_ (BoundedFunctions X),(RAlgebra X)),(One_ (BoundedFunctions X),(RAlgebra X)),(Zero_ (BoundedFunctions X),(RAlgebra X)) #) is Subalgebra of RAlgebra X by Th03;

definition

let X be non empty set ;
func R_Algebra_of_BoundedFunctions X -> Algebra equals :: C0SP1:def 14
AlgebraStr(# (BoundedFunctions X),(mult_ (BoundedFunctions X),(RAlgebra X)),(Add_ (BoundedFunctions X),(RAlgebra X)),(Mult_ (BoundedFunctions X),(RAlgebra X)),(One_ (BoundedFunctions X),(RAlgebra X)),(Zero_ (BoundedFunctions X),(RAlgebra X)) #);
coherence
AlgebraStr(# (BoundedFunctions X),(mult_ (BoundedFunctions X),(RAlgebra X)),(Add_ (BoundedFunctions X),(RAlgebra X)),(Mult_ (BoundedFunctions X),(RAlgebra X)),(One_ (BoundedFunctions X),(RAlgebra X)),(Zero_ (BoundedFunctions X),(RAlgebra X)) #) is Algebra by Th03;

end;

:: deftheorem defines R_Algebra_of_BoundedFunctions C0SP1:def 14 :

for X being non empty set holds R_Algebra_of_BoundedFunctions X = AlgebraStr(# (BoundedFunctions X),(mult_ (BoundedFunctions X),(RAlgebra X)),(Add_ (BoundedFunctions X),(RAlgebra X)),(Mult_ (BoundedFunctions X),(RAlgebra X)),(One_ (BoundedFunctions X),(RAlgebra X)),(Zero_ (BoundedFunctions X),(RAlgebra X)) #);

theorem :: C0SP1:11

for X being non empty set holds R_Algebra_of_BoundedFunctions X is RealLinearSpace

proof end;

theorem ThB10: :: C0SP1:12

for X being non empty set
for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X, REAL 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 end;

theorem ThB11: :: C0SP1:13

for X being non empty set
for a being Real
for F, G being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g being Function of X, REAL st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem ThB12: :: C0SP1:14

for X being non empty set
for F, G, H being VECTOR of (R_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X, REAL 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 end;

theorem ThB12Zero: :: C0SP1:15

for X being non empty set holds 0. (R_Algebra_of_BoundedFunctions X) = X --> 0

proof end;

theorem ThB12One: :: C0SP1:16

for X being non empty set holds 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1

proof end;

definition

let X be non empty set ;
let F be set ;
assume A1: F in BoundedFunctions X ;
func modetrans F,X -> Function of X, REAL means :DefB7: :: C0SP1:def 15
( it = F & it | X is bounded );
correctness
existence
ex b₁ being Function of X, REAL st
( b₁ = F & b₁ | X is bounded );
uniqueness
for b₁, b₂ being Function of X, REAL st b₁ = F & b₁ | X is bounded & b₂ = F & b₂ | X is bounded holds
b₁ = b₂;
by A1;

end;

:: deftheorem DefB7 defines modetrans C0SP1:def 15 :

for X being non empty set
for F being set st F in BoundedFunctions X holds
for b₃ being Function of X, REAL holds
( b₃ = modetrans F,X iff ( b₃ = F & b₃ | X is bounded ) );

definition

let X be non empty set ;
let f be Function of X, REAL ;
func PreNorms f -> non empty Subset of REAL equals :: C0SP1:def 16
{ (abs (f . x)) where x is Element of X : verum } ;
coherence
{ (abs (f . x)) where x is Element of X : verum } is non empty Subset of REAL

proof end;

end;

:: deftheorem defines PreNorms C0SP1:def 16 :

for X being non empty set
for f being Function of X, REAL holds PreNorms f = { (abs (f . x)) where x is Element of X : verum } ;

theorem ThB13: :: C0SP1:17

for X being non empty set
for f being Function of X, REAL st f | X is bounded holds
( not PreNorms f is empty & PreNorms f is bounded_above )

proof end;

theorem :: C0SP1:18

for X being non empty set
for f being Function of X, REAL holds
( f | X is bounded iff PreNorms f is bounded_above )

proof end;

theorem ThB15: :: C0SP1:19

for X being non empty set ex NORM being Function of BoundedFunctions X, REAL st
for F being set st F in BoundedFunctions X holds
NORM . F = sup (PreNorms (modetrans F,X))

proof end;

definition

let X be non empty set ;
func BoundedFunctionsNorm X -> Function of BoundedFunctions X, REAL means :DefB9: :: C0SP1:def 17
for x being set st x in BoundedFunctions X holds
it . x = sup (PreNorms (modetrans x,X));
existence
ex b₁ being Function of BoundedFunctions X, REAL st
for x being set st x in BoundedFunctions X holds
b₁ . x = sup (PreNorms (modetrans x,X)) by ThB15;
uniqueness
for b₁, b₂ being Function of BoundedFunctions X, REAL st ( for x being set st x in BoundedFunctions X holds
b₁ . x = sup (PreNorms (modetrans x,X)) ) & ( for x being set st x in BoundedFunctions X holds
b₂ . x = sup (PreNorms (modetrans x,X)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefB9 defines BoundedFunctionsNorm C0SP1:def 17 :

for X being non empty set
for b₂ being Function of BoundedFunctions X, REAL holds
( b₂ = BoundedFunctionsNorm X iff for x being set st x in BoundedFunctions X holds
b₂ . x = sup (PreNorms (modetrans x,X)) );

theorem ThB16: :: C0SP1:20

for X being non empty set
for f being Function of X, REAL st f | X is bounded holds
modetrans f,X = f

proof end;

theorem ThB17: :: C0SP1:21

for X being non empty set
for f being Function of X, REAL st f | X is bounded holds
(BoundedFunctionsNorm X) . f = sup (PreNorms f)

proof end;

definition

let X be non empty set ;
func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals :: C0SP1:def 18
Normed_AlgebraStr(# (BoundedFunctions X),(mult_ (BoundedFunctions X),(RAlgebra X)),(Add_ (BoundedFunctions X),(RAlgebra X)),(Mult_ (BoundedFunctions X),(RAlgebra X)),(One_ (BoundedFunctions X),(RAlgebra X)),(Zero_ (BoundedFunctions X),(RAlgebra X)),(BoundedFunctionsNorm X) #);
correctness
coherence
Normed_AlgebraStr(# (BoundedFunctions X),(mult_ (BoundedFunctions X),(RAlgebra X)),(Add_ (BoundedFunctions X),(RAlgebra X)),(Mult_ (BoundedFunctions X),(RAlgebra X)),(One_ (BoundedFunctions X),(RAlgebra X)),(Zero_ (BoundedFunctions X),(RAlgebra X)),(BoundedFunctionsNorm X) #) is Normed_AlgebraStr ;
;

end;

:: deftheorem defines R_Normed_Algebra_of_BoundedFunctions C0SP1:def 18 :

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X = Normed_AlgebraStr(# (BoundedFunctions X),(mult_ (BoundedFunctions X),(RAlgebra X)),(Add_ (BoundedFunctions X),(RAlgebra X)),(Mult_ (BoundedFunctions X),(RAlgebra X)),(One_ (BoundedFunctions X),(RAlgebra X)),(Zero_ (BoundedFunctions X),(RAlgebra X)),(BoundedFunctionsNorm X) #);

registration

let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> non empty ;
correctness
coherence
not R_Normed_Algebra_of_BoundedFunctions X is empty;
;

end;

UNITAL: now

let X be non empty set ; :: thesis: for x, e being Element of (R_Normed_Algebra_of_BoundedFunctions X) st e = One_ (BoundedFunctions X),(RAlgebra X) holds
( x * e = x & e * x = x )
set F = R_Normed_Algebra_of_BoundedFunctions X;
let x, e be Element of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( e = One_ (BoundedFunctions X),(RAlgebra X) implies ( x * e = x & e * x = x ) )
assume A1: e = One_ (BoundedFunctions X),(RAlgebra X) ; :: thesis: ( x * e = x & e * x = x )
set X1 = BoundedFunctions X;
reconsider f = x as Element of BoundedFunctions X ;
1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X) by ThB12One;
then P5: ( [f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):] & [(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):] ) by ZFMISC_1:106;
x * e = (mult_ (BoundedFunctions X),(RAlgebra X)) . f,(1_ (RAlgebra X)) by A1, Rdef214;
then x * e = (the multF of (RAlgebra X) || (BoundedFunctions X)) . f,(1_ (RAlgebra X)) by Rdef220;
then x * e = f * (1_ (RAlgebra X)) by P5, FUNCT_1:72;
hence x * e = x by FUNCSDOM:49; :: thesis: e * x = x
e * x = (mult_ (BoundedFunctions X),(RAlgebra X)) . (1_ (RAlgebra X)),f by A1, Rdef214;
then e * x = (the multF of (RAlgebra X) || (BoundedFunctions X)) . (1_ (RAlgebra X)),f by Rdef220;
then e * x = (1_ (RAlgebra X)) * f by P5, FUNCT_1:72;
hence e * x = x by FUNCSDOM:49; :: thesis: verum

end;

registration

let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> unital ;
correctness
coherence
R_Normed_Algebra_of_BoundedFunctions X is unital;

proof end;

end;

theorem RSSPACE34: :: C0SP1:22

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 U3 of W,the U2 of W #) = V & 1. V = 1. W holds
W is Algebra

proof end;

theorem LmAlgebra4: :: C0SP1:23

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Algebra

proof end;

theorem FUNCSDOM23: :: C0SP1:24

for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ (BoundedFunctions X),(RAlgebra X)) . 1,F = F

proof end;

theorem LmAlgebra5: :: C0SP1:25

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace

proof end;

theorem ThB18: :: C0SP1:26

for X being non empty set holds X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X)

proof end;

theorem ThB19: :: C0SP1:27

for X being non empty set
for x being Element of X
for f being Function of X, REAL
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
abs (f . x) <= ||.F.||

proof end;

theorem :: C0SP1:28

for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||

proof end;

theorem ThB21: :: C0SP1:29

for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||

proof end;

theorem ThB22: :: C0SP1:30

for X being non empty set
for f, g, h being Function of X, REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions 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 end;

theorem ThB23: :: C0SP1:31

for X being non empty set
for a being Real
for f, g being Function of X, REAL
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem ThB23a: :: C0SP1:32

for X being non empty set
for f, g, h being Function of X, REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions 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 end;

theorem ThB24: :: C0SP1:33

for X being non empty set
for a being Real
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

theorem ThB25: :: C0SP1:34

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like

proof end;

registration

let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like RealNormSpace-like ;
coherence
( R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like & R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace-like & R_Normed_Algebra_of_BoundedFunctions X is Abelian & R_Normed_Algebra_of_BoundedFunctions X is add-associative & R_Normed_Algebra_of_BoundedFunctions X is right_zeroed & R_Normed_Algebra_of_BoundedFunctions X is right_complementable ) by ThB25, LmAlgebra5;

end;

theorem ThB27: :: C0SP1:35

for X being non empty set
for f, g, h being Function of X, REAL
for F, G, H being Point of (R_Normed_Algebra_of_BoundedFunctions 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 end;

theorem ThB28: :: C0SP1:36

for X being non empty set
for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent

proof end;

theorem ThB29: :: C0SP1:37

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace

proof end;

registration

let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X -> complete ;
coherence
R_Normed_Algebra_of_BoundedFunctions X is complete by ThB29;

end;

theorem :: C0SP1:38

for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra

proof end;