:: Banach Algebra of Bounded Complex-Valued Functionals
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 20, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

definition
let V be ComplexAlgebra;
mode ComplexSubAlgebra of V ->  ComplexAlgebra means :Def1: :: CC0SP1:def 1
( 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 | [:COMPLEX, the carrier of it:] & 1. it = 1. V & 0. it = 0. V );
existence
 ex b1 being ComplexAlgebra st
( the carrier of b1 c= the carrier of V & the addF of b1 = the addF of V || the carrier of b1 & the multF of b1 = the multF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:COMPLEX, the carrier of b1:] & 1. b1 = 1. V & 0. b1 = 0. V )
proofend;
end;

:: deftheorem Def1 defines ComplexSubAlgebra CC0SP1:def_1_:_
 for V, b2 being ComplexAlgebra holds
( b2 is ComplexSubAlgebra of V iff ( the carrier of b2 c= the carrier of V & the addF of b2 = the addF of V || the carrier of b2 & the multF of b2 = the multF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:COMPLEX, the carrier of b2:] & 1. b2 = 1. V & 0. b2 = 0. V ) );

Lm1: now__::_thesis:_for_z_being_Complex
for_X_being_non_empty_set_
for_V_being_ComplexAlgebra
for_V1_being_non_empty_Subset_of_V
for_d1,_d2_being_Element_of_X
for_A_being_BinOp_of_X
for_M_being_Function_of_[:X,X:],X
for_MR_being_Function_of_[:COMPLEX,X:],X_st_V1_=_X_&_MR_=_the_Mult_of_V_|_[:COMPLEX,V1:]_holds_
for_W_being_non_empty_ComplexAlgebraStr_st_W_=_ComplexAlgebraStr(#_X,M,A,MR,d2,d1_#)_holds_
for_w_being_VECTOR_of_W
for_v_being_Element_of_V_st_w_=_v_holds_
z_*_w_=_z_*_v
let z be Complex; ::_thesis: for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let X be non empty set ; ::_thesis: for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let V be ComplexAlgebra; ::_thesis: for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let V1 be non empty Subset of V; ::_thesis: for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let d1, d2 be Element of X; ::_thesis: for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let A be BinOp of X; ::_thesis: for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let M be Function of [:X,X:],X; ::_thesis: for MR being Function of [:COMPLEX,X:],X st V1 = X & MR = the Mult of V | [:COMPLEX,V1:] holds
for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let MR be Function of [:COMPLEX,X:],X; ::_thesis: ( V1 = X & MR = the Mult of V | [:COMPLEX,V1:] implies for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v )
assume that
A1: V1 = X and
A2: MR = the Mult of V | [:COMPLEX,V1:] ; ::_thesis: for W being non empty ComplexAlgebraStr st W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) holds
for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let W be non empty ComplexAlgebraStr ; ::_thesis: ( W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) implies for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v )
assume A3: W = ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) ; ::_thesis: for w being VECTOR of W
for v being Element of V st w = v holds
z * w = z * v
let w be VECTOR of W; ::_thesis: for v being Element of V st w = v holds
z * w = z * v
let v be Element of V; ::_thesis: ( w = v implies z * w = z * v )
assume A4: w = v ; ::_thesis: z * w = z * v
 z in COMPLEX by XCMPLX_0:def_2;
then  [z,w] in [:COMPLEX,V1:] by A1, A3, ZFMISC_1:def_2;
hence  z * w = z * v by A4, A2, A3, FUNCT_1:49; ::_thesis: verum
end;

theorem Th1: :: CC0SP1:1
for X being non empty set
for V being ComplexAlgebra
for V1 being non empty Subset of V
for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for MR being Function of [:COMPLEX,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 | [:COMPLEX,V1:] & V1 is having-inverse holds
ComplexAlgebraStr(# X,M,A,MR,d2,d1 #) is ComplexSubAlgebra of V
proofend;

registration
let V be ComplexAlgebra;
cluster non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative strict vector-associative for ComplexSubAlgebra of V;
existence
 ex b1 being ComplexSubAlgebra of V st b1 is strict
proofend;
end;

definition
let V be ComplexAlgebra;
let V1 be Subset of V;
attrV1 is Cadditively-linearly-closed  means :Def2: :: CC0SP1:def 2
( V1 is add-closed & V1 is having-inverse & ( for a being Complex
for v being Element of V st v in V1 holds
a * v in V1 ) );
end;

:: deftheorem Def2 defines Cadditively-linearly-closed CC0SP1:def_2_:_
 for V being ComplexAlgebra
for V1 being Subset of V holds
( V1 is Cadditively-linearly-closed iff ( V1 is add-closed & V1 is having-inverse & ( for a being Complex
for v being Element of V st v in V1 holds
a * v in V1 ) ) );

definition
let V be ComplexAlgebra;
let V1 be Subset of V;
assume B1: ( V1 is Cadditively-linearly-closed & not V1 is empty ) ;
func Mult_ (V1,V) ->  Function of [:COMPLEX,V1:],V1 equals :Def3: :: CC0SP1:def 3
 the Mult of V | [:COMPLEX,V1:];
correctness
coherence
the Mult of V | [:COMPLEX,V1:] is Function of [:COMPLEX,V1:],V1;
proofend;
end;

:: deftheorem Def3 defines Mult_ CC0SP1:def_3_:_
 for V being ComplexAlgebra
for V1 being Subset of V st V1 is Cadditively-linearly-closed & not V1 is empty holds
Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:];

definition
let X be non empty set ;
func ComplexBoundedFunctions X ->  non empty Subset of (CAlgebra X) equals :: CC0SP1:def 4
 {  f where f is Function of X,COMPLEX : f | X is bounded  }  ;
correctness
coherence
{  f where f is Function of X,COMPLEX : f | X is bounded  }  is non empty Subset of (CAlgebra X);
proofend;
end;

:: deftheorem  defines ComplexBoundedFunctions CC0SP1:def_4_:_
 for X being non empty set holds ComplexBoundedFunctions X =  {  f where f is Function of X,COMPLEX : f | X is bounded  }  ;

registration
let X be non empty set ;
cluster CAlgebra X ->  scalar-unital ;
coherence
 CAlgebra X is scalar-unital
proofend;
end;

registration
let X be non empty set ;
cluster ComplexBoundedFunctions X ->  non empty multiplicatively-closed Cadditively-linearly-closed ;
coherence
 ( ComplexBoundedFunctions X is Cadditively-linearly-closed & ComplexBoundedFunctions X is multiplicatively-closed )
proofend;
end;

registration
let V be ComplexAlgebra;
cluster non empty multiplicatively-closed Cadditively-linearly-closed for Element of bool the carrier of V;
existence
 ex b1 being non empty Subset of V st
( b1 is Cadditively-linearly-closed & b1 is multiplicatively-closed )
proofend;
end;

definition
let V be non empty CLSStruct ;
attrV is scalar-mult-cancelable  means :: CC0SP1:def 5
 for a being Complex
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V );
end;

:: deftheorem  defines scalar-mult-cancelable CC0SP1:def_5_:_
 for V being non empty CLSStruct holds
( V is scalar-mult-cancelable iff for a being Complex
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V ) );

theorem Th2: :: CC0SP1:2
for V being ComplexAlgebra
for V1 being non empty multiplicatively-closed Cadditively-linearly-closed Subset of V holds ComplexAlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is ComplexSubAlgebra of V
proofend;

theorem Th3: :: CC0SP1:3
for V being ComplexAlgebra
for V1 being ComplexSubAlgebra 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 Complex st v1 = v holds
a * v1 = a * v ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
proofend;

definition
let X be non empty set ;
func C_Algebra_of_BoundedFunctions X ->  ComplexAlgebra equals :: CC0SP1:def 6
 ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #);
coherence
 ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #) is ComplexAlgebra by Th2;
end;

:: deftheorem  defines C_Algebra_of_BoundedFunctions CC0SP1:def_6_:_
 for X being non empty set holds C_Algebra_of_BoundedFunctions X = ComplexAlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))) #);

theorem :: CC0SP1:4
for X being non empty set holds C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;

registration
let X be non empty set ;
cluster C_Algebra_of_BoundedFunctions X ->  scalar-unital ;
coherence
 ( C_Algebra_of_BoundedFunctions X is vector-distributive & C_Algebra_of_BoundedFunctions X is scalar-unital )
proofend;
end;

theorem Th5: :: CC0SP1:5
for X being non empty set
for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX 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) )
proofend;

theorem Th6: :: CC0SP1:6
for X being non empty set
for a being Complex
for F, G being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g being Function of X,COMPLEX st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proofend;

theorem Th7: :: CC0SP1:7
for X being non empty set
for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX 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) )
proofend;

theorem Th8: :: CC0SP1:8
for X being non empty set holds 0. (C_Algebra_of_BoundedFunctions X) = X --> 0
proofend;

theorem Th9: :: CC0SP1:9
for X being non empty set holds 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r
proofend;

definition
let X be non empty set ;
let F be set ;
assume A1: F in ComplexBoundedFunctions X ;
func modetrans (F,X) ->  Function of X,COMPLEX means :Def7: :: CC0SP1:def 7
( it = F & it | X is bounded );
correctness
existence
ex b1 being Function of X,COMPLEX st
( b1 = F & b1 | X is bounded );
uniqueness
for b1, b2 being Function of X,COMPLEX st b1 = F & b1 | X is bounded & b2 = F & b2 | X is bounded holds
b1 = b2;
by A1;
end;

:: deftheorem Def7 defines modetrans CC0SP1:def_7_:_
 for X being non empty set
for F being set st F in ComplexBoundedFunctions X holds
for b3 being Function of X,COMPLEX holds
( b3 = modetrans (F,X) iff ( b3 = F & b3 | X is bounded ) );

definition
let X be non empty set ;
let f be Function of X,COMPLEX;
func PreNorms f ->  non empty Subset of REAL equals :: CC0SP1:def 8
 {  |.(f . x).| where x is Element of X : verum  }  ;
coherence
  {  |.(f . x).| where x is Element of X : verum  }  is non empty Subset of REAL
proofend;
end;

:: deftheorem  defines PreNorms CC0SP1:def_8_:_
 for X being non empty set
for f being Function of X,COMPLEX holds PreNorms f =  {  |.(f . x).| where x is Element of X : verum  }  ;

Lm2:  for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
proofend;

theorem Th10: :: CC0SP1:10
for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
PreNorms f is bounded_above
proofend;

theorem Th11: :: CC0SP1:11
for X being non empty set
for f being Function of X,COMPLEX holds
( f | X is bounded iff PreNorms f is bounded_above )
proofend;

definition
let X be non empty set ;
func ComplexBoundedFunctionsNorm X ->  Function of (ComplexBoundedFunctions X),REAL means :Def9: :: CC0SP1:def 9
 for x being set st x in ComplexBoundedFunctions X holds
it . x = upper_bound (PreNorms (modetrans (x,X)));
existence
 ex b1 being Function of (ComplexBoundedFunctions X),REAL st
for x being set st x in ComplexBoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X)))
proofend;
uniqueness
 for b1, b2 being Function of (ComplexBoundedFunctions X),REAL st ( for x being set st x in ComplexBoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in ComplexBoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CC0SP1:def_9_:_
 for X being non empty set
for b2 being Function of (ComplexBoundedFunctions X),REAL holds
( b2 = ComplexBoundedFunctionsNorm X iff for x being set st x in ComplexBoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) );

theorem Th12: :: CC0SP1:12
for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
modetrans (f,X) = f
proofend;

theorem Th13: :: CC0SP1:13
for X being non empty set
for f being Function of X,COMPLEX st f | X is bounded holds
(ComplexBoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
proofend;

definition
let X be non empty set ;
func C_Normed_Algebra_of_BoundedFunctions X ->  Normed_Complex_AlgebraStr  equals :: CC0SP1:def 10
 Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #);
correctness
coherence
Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #) is Normed_Complex_AlgebraStr ;
;
end;

:: deftheorem  defines C_Normed_Algebra_of_BoundedFunctions CC0SP1:def_10_:_
 for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X = Normed_Complex_AlgebraStr(# (ComplexBoundedFunctions X),(mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Add_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))),(One_ ((ComplexBoundedFunctions X),(CAlgebra X))),(Zero_ ((ComplexBoundedFunctions X),(CAlgebra X))),(ComplexBoundedFunctionsNorm X) #);

registration
let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X ->  non empty ;
correctness
coherence
not C_Normed_Algebra_of_BoundedFunctions X is empty ;
;
end;

Lm3: now__::_thesis:_for_X_being_non_empty_set_
for_x,_e_being_Element_of_(C_Normed_Algebra_of_BoundedFunctions_X)_st_e_=_One__((ComplexBoundedFunctions_X),(CAlgebra_X))_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let X be non empty set ; ::_thesis: for x, e being Element of (C_Normed_Algebra_of_BoundedFunctions X) st e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) holds
( x * e = x & e * x = x )
set F = C_Normed_Algebra_of_BoundedFunctions X;
let x, e be Element of (C_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) implies ( x * e = x & e * x = x ) )
set X1 = ComplexBoundedFunctions X;
reconsider f = x as Element of ComplexBoundedFunctions X ;
assume A1: e = One_ ((ComplexBoundedFunctions X),(CAlgebra X)) ; ::_thesis: ( x * e = x & e * x = x )
then  x * e = (mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (f,(1_ (CAlgebra X))) by C0SP1:def_8;
then A2: x * e = ( the multF of (CAlgebra X) || (ComplexBoundedFunctions X)) . (f,(1_ (CAlgebra X))) by C0SP1:def_6;
 e * x = (mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . ((1_ (CAlgebra X)),f) by A1, C0SP1:def_8;
then A3: e * x = ( the multF of (CAlgebra X) || (ComplexBoundedFunctions X)) . ((1_ (CAlgebra X)),f) by C0SP1:def_6;
A4: 1_ (CAlgebra X) = 1_ (C_Algebra_of_BoundedFunctions X) by Th9;
then  [f,(1_ (CAlgebra X))] in [:(ComplexBoundedFunctions X),(ComplexBoundedFunctions X):] by ZFMISC_1:87;
then  x * e = f * (1_ (CAlgebra X)) by A2, FUNCT_1:49;
hence  x * e = x by VECTSP_1:def_4; ::_thesis: e * x = x
 [(1_ (CAlgebra X)),f] in [:(ComplexBoundedFunctions X),(ComplexBoundedFunctions X):] by A4, ZFMISC_1:87;
then  e * x = (1_ (CAlgebra X)) * f by A3, FUNCT_1:49;
hence  e * x = x by VECTSP_1:def_4; ::_thesis: verum
end;

registration
let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X ->  unital ;
correctness
coherence
C_Normed_Algebra_of_BoundedFunctions X is unital ;
proofend;
end;

theorem Th14: :: CC0SP1:14
for W being Normed_Complex_AlgebraStr
for V being ComplexAlgebra st ComplexAlgebraStr(# 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 ComplexAlgebra
proofend;

theorem Th15: :: CC0SP1:15
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is ComplexAlgebra
proofend;

theorem :: CC0SP1:16
for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F
proofend;

theorem Th17: :: CC0SP1:17
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace
proofend;

theorem Th18: :: CC0SP1:18
for X being non empty set holds X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X)
proofend;

theorem Th19: :: CC0SP1:19
for X being non empty set
for x being Element of X
for f being Function of X,COMPLEX
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||
proofend;

theorem :: CC0SP1:20
for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||
proofend;

theorem Th21: :: CC0SP1:21
for X being non empty set
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st F = 0. (C_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
proofend;

theorem Th22: :: CC0SP1:22
for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F &amp; g = G &amp; h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
proofend;

theorem Th23: :: CC0SP1:23
for X being non empty set
for a being Complex
for f, g being Function of X,COMPLEX
for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F &amp; g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proofend;

theorem Th24: :: CC0SP1:24
for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F &amp; g = G &amp; h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
proofend;

theorem Th25: :: CC0SP1:25
for X being non empty set
for a being Complex
for F, G being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_BoundedFunctions X) ) &amp; ( F = 0. (C_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) &amp; ||.(a * F).|| = |.a.| * ||.F.|| &amp; ||.(F + G).|| <= ||.F.|| + ||.G.|| )
proofend;

Lm4:  for X being non empty set holds
( C_Normed_Algebra_of_BoundedFunctions X is reflexive &amp; C_Normed_Algebra_of_BoundedFunctions X is discerning &amp; C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like )
proofend;

registration
let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X ->  right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
 ( C_Normed_Algebra_of_BoundedFunctions X is right_complementable &amp; C_Normed_Algebra_of_BoundedFunctions X is Abelian &amp; C_Normed_Algebra_of_BoundedFunctions X is add-associative &amp; C_Normed_Algebra_of_BoundedFunctions X is right_zeroed &amp; C_Normed_Algebra_of_BoundedFunctions X is vector-distributive &amp; C_Normed_Algebra_of_BoundedFunctions X is scalar-distributive &amp; C_Normed_Algebra_of_BoundedFunctions X is scalar-associative &amp; C_Normed_Algebra_of_BoundedFunctions X is scalar-unital &amp; C_Normed_Algebra_of_BoundedFunctions X is discerning &amp; C_Normed_Algebra_of_BoundedFunctions X is reflexive &amp; C_Normed_Algebra_of_BoundedFunctions X is ComplexNormSpace-like ) by Th17, Lm4;
end;

theorem Th26: :: CC0SP1:26
for X being non empty set
for f, g, h being Function of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F &amp; g = G &amp; h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
proofend;

theorem Th27: :: CC0SP1:27
for X being non empty set
for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent
proofend;

registration
let X be non empty set ;
cluster C_Normed_Algebra_of_BoundedFunctions X ->  complete ;
coherence
 C_Normed_Algebra_of_BoundedFunctions X is complete
proofend;
end;

theorem :: CC0SP1:28
for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions X is Complex_Banach_Algebra
proofend;