:: C0SP1 semantic presentation

begin

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

:: deftheorem Def1 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;
attrV1 is additively-closed  means :Def2: :: C0SP1:def 2
( V1 is add-closed & V1 is having-inverse );
end;

:: deftheorem Def2 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 ) );

Lm1:  for V being non empty addLoopStr holds [#] V is add-closed
proof
let V be non empty addLoopStr ; ::_thesis: [#] V is add-closed
 for v, u being Element of V st v in [#] V & u in [#] V holds
v + u in [#] V ;
hence  [#] V is add-closed by IDEAL_1:def_1; ::_thesis: verum
end;

Lm2:  for V being non empty addLoopStr holds [#] V is having-inverse
proof
let V be non empty addLoopStr ; ::_thesis: [#] V is having-inverse
 for v being Element of V st v in [#] V holds
- v in [#] V ;
hence  [#] V is having-inverse by Def1; ::_thesis: verum
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 Lm1, Lm2;
end;

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

registration
let V be non empty addLoopStr ;
cluster non empty add-closed having-inverse for Element of bool the carrier of V;
correctness
existence
ex b1 being Subset of V st
( b1 is add-closed & b1 is having-inverse & not b1 is empty );
proof
take  [#] V ; ::_thesis: ( [#] V is add-closed & [#] V is having-inverse & not [#] V is empty )
thus  ( [#] V is add-closed & [#] V is having-inverse & not [#] V is empty ) ; ::_thesis: verum
end;
end;

definition
let V be Ring;
mode Subring of V ->  Ring means :Def3: :: 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 b1 being Ring 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 & 1. b1 = 1. V & 0. b1 = 0. V )
proof
take  V ; ::_thesis: ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & 1. V = 1. V & 0. V = 0. V )
thus  ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & 1. V = 1. V & 0. V = 0. V ) by RELSET_1:19; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Subring C0SP1:def_3_:_
 for V, b2 being Ring holds
( b2 is Subring 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 & 1. b2 = 1. V & 0. b2 = 0. V ) );


theorem Th1: :: 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
let X be non empty set ; ::_thesis: 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
let d1, d2 be Element of X; ::_thesis: 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
let A be BinOp of X; ::_thesis: 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
let M be Function of [:X,X:],X; ::_thesis: 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
let V be Ring; ::_thesis: 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
let V1 be Subset of V; ::_thesis: ( V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse implies doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V )
assume that
A1: V1 = X and
A2: A = the addF of V || V1 and
A3: M = the multF of V || V1 and
A4: d1 = 1. V and
A5: d2 = 0. V and
A6: for v being Element of V st v in V1 holds
- v in V1 ; :: according to C0SP1:def_1 ::_thesis: doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
reconsider W = doubleLoopStr(# X,A,M,d1,d2 #) as non empty doubleLoopStr ;
A7: now__::_thesis:_for_a,_x_being_Element_of_W_holds_a_*_x_=_the_multF_of_V_._(a,x)
let a, x be Element of W; ::_thesis: a * x = the multF of V . (a,x)
 a * x = the multF of V . [a,x] by A1, A3, FUNCT_1:49;
hence  a * x = the multF of V . (a,x) ; ::_thesis: verum
end;
A8: now__::_thesis:_for_x,_y_being_Element_of_W_holds_x_+_y_=_the_addF_of_V_._(x,y)
let x, y be Element of W; ::_thesis: x + y = the addF of V . (x,y)
 x + y = the addF of V . [x,y] by A1, A2, FUNCT_1:49;
hence  x + y = the addF of V . (x,y) ; ::_thesis: verum
end;
A9: ( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )
proof
set MV = the multF of V;
set Av = the addF of V;
hereby  :: according to RLVECT_1:def_2 ::_thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )
let x, y be Element of W; ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
 ( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence  x + y = y + x ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )
let x, y, z be Element of W; ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def_3;
 x + (y + z) = the addF of V . (x1,(y + z)) by A8;
then A10: x + (y + z) = x1 + (y1 + z1) by A8;
 (x + y) + z = the addF of V . ((x + y),z1) by A8;
then  (x + y) + z = (x1 + y1) + z1 by A8;
hence  (x + y) + z = x + (y + z) by A10, RLVECT_1:def_3; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: ( W is right_complementable & W is associative & W is well-unital & W is distributive )
let x be Element of W; ::_thesis: x + (0. W) = x
reconsider y = x as Element of V by A1, TARSKI:def_3;
 x + (0. W) = y + (0. V) by A5, A8;
hence  x + (0. W) = x by RLVECT_1:4; ::_thesis: verum
end;
thus  W is right_complementable ::_thesis: ( W is associative & W is well-unital & W is distributive )
proof
let x be Element of W; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of V by A1, TARSKI:def_3;
consider v being Element of V such that
A11: x1 + v = 0. V by ALGSTR_0:def_11;
 v = - x1 by A11, VECTSP_1:16;
then reconsider y = v as Element of W by A1, A6;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. W
thus  x + y = 0. W by A5, A8, A11; ::_thesis: verum
end;
hereby  :: according to GROUP_1:def_3 ::_thesis: ( W is well-unital & W is distributive )
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, TARSKI:def_3;
 a * (b * x) = the multF of V . (a,(b * x)) by A7;
then A12: a * (b * x) = a1 * (b1 * y) by A7;
 a * b = a1 * b1 by A7;
then  (a * b) * x = (a1 * b1) * y by A7;
hence  (a * b) * x = a * (b * x) by A12, GROUP_1:def_3; ::_thesis: verum
end;
hereby  :: according to VECTSP_1:def_6 ::_thesis: W is distributive
let x be Element of W; ::_thesis: ( x * (1. W) = x & (1. W) * x = x )
reconsider y = x as Element of V by A1, TARSKI:def_3;
 ( x * (1. W) = y * (1. V) & (1. W) * x = (1. V) * y ) by A4, A7;
hence  ( x * (1. W) = x & (1. W) * x = x ) by VECTSP_1:def_6; ::_thesis: verum
end;
hereby  :: according to VECTSP_1:def_7 ::_thesis: verum
let a, x, y be Element of W; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) )
reconsider x1 = x, y1 = y, a1 = a as Element of V by A1, TARSKI:def_3;
 (x + y) * a = the multF of V . ((x + y),a) by A7;
then  (x + y) * a = (x1 + y1) * a1 by A8;
then  (x + y) * a = (x1 * a1) + (y1 * a1) by VECTSP_1:def_7;
then  (x + y) * a = the addF of V . (( the multF of V . (x1,a1)),(y * a)) by A7;
then A13: (x + y) * a = the addF of V . ((x * a),(y * a)) by A7;
 a * (x + y) = the multF of V . (a,(x + y)) by A7;
then  a * (x + y) = a1 * (x1 + y1) by A8;
then  a * (x + y) = (a1 * x1) + (a1 * y1) by VECTSP_1:def_7;
then  a * (x + y) = the addF of V . (( the multF of V . (a,x1)),(a * y)) by A7;
then  a * (x + y) = the addF of V . ((a * x),(a * y)) by A7;
hence  ( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) ) by A8, A13; ::_thesis: verum
end;
end;
 ( 0. W = 0. V & 1. W = 1. V ) by A4, A5;
hence  doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V by A1, A2, A3, A9, Def3; ::_thesis: verum
end;

registration
let V be Ring;
cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital for Subring of V;
existence
 ex b1 being Subring of V st b1 is strict
proof
set V1 = [#] V;
 ( the addF of V = the addF of V || ([#] V) & the multF of V = the multF of V || ([#] V) ) by RELSET_1:19;
then  doubleLoopStr(# the carrier of V, the addF of V, the multF of V,(1. V),(0. V) #) is Subring of V by Th1;
hence  ex b1 being Subring of V st b1 is strict ; ::_thesis: verum
end;
end;

definition
let V be non empty multLoopStr_0 ;
let V1 be Subset of V;
attrV1 is multiplicatively-closed  means :Def4: :: 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 Def4 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 B1: ( V1 is add-closed & not V1 is empty ) ;
func Add_ (V1,V) ->  BinOp of V1 equals :Def5: :: C0SP1:def 5
 the addF of V || V1;
correctness
coherence
the addF of V || V1 is BinOp of V1;
proof
A1: dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1;
A2: for z being set st z in [:V1,V1:] holds
( the addF of V || V1) . z in V1
proof
let z be set ; ::_thesis: ( z in [:V1,V1:] implies ( the addF of V || V1) . z in V1 )
assume A3: z in [:V1,V1:] ; ::_thesis: ( the addF of V || V1) . z in V1
then consider r, x being set  such that
A4: ( r in V1 & x in V1 ) and
A5: z = [r,x] by ZFMISC_1:def_2;
reconsider y = x, r1 = r as Element of V by A4;
 [r,x] in dom ( the addF of V || V1) by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then  ( the addF of V || V1) . z = r1 + y by A5, FUNCT_1:47;
hence  ( the addF of V || V1) . z in V1 by B1, A4, IDEAL_1:def_1; ::_thesis: verum
end;
 dom ( the addF of V || V1) = [:V1,V1:] by A1, RELAT_1:62, ZFMISC_1:96;
hence  the addF of V || V1 is BinOp of V1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;

:: deftheorem Def5 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 B1: ( V1 is multiplicatively-closed & not V1 is empty ) ;
func mult_ (V1,V) ->  BinOp of V1 equals :Def6: :: C0SP1:def 6
 the multF of V || V1;
correctness
coherence
the multF of V || V1 is BinOp of V1;
proof
A1: dom the multF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1;
A2: for z being set st z in [:V1,V1:] holds
( the multF of V || V1) . z in V1
proof
let z be set ; ::_thesis: ( z in [:V1,V1:] implies ( the multF of V || V1) . z in V1 )
assume A3: z in [:V1,V1:] ; ::_thesis: ( the multF of V || V1) . z in V1
then consider r, x being set  such that
A4: ( r in V1 & x in V1 ) and
A5: z = [r,x] by ZFMISC_1:def_2;
reconsider y = x, r1 = r as Element of V by A4;
 [r,x] in dom ( the multF of V || V1) by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then  ( the multF of V || V1) . z = r1 * y by A5, FUNCT_1:47;
hence  ( the multF of V || V1) . z in V1 by B1, A4, Def4; ::_thesis: verum
end;
 dom ( the multF of V || V1) = [:V1,V1:] by A1, RELAT_1:62, ZFMISC_1:96;
hence  the multF of V || V1 is BinOp of V1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;

:: deftheorem Def6 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 :Def7: :: C0SP1:def 7
 0. V;
correctness
coherence
0. V is Element of V1;
proof
set x = the Element of V1;
reconsider x1 = the Element of V1 as Element of V by A1, TARSKI:def_3;
 ( - x1 in V1 & x1 + (- x1) = 0. V ) by A1, Def1, RLVECT_1:def_10;
hence  0. V is Element of V1 by A1, IDEAL_1:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def7 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 :Def8: :: C0SP1:def 8
 1. V;
correctness
coherence
1. V is Element of V1;
by A1, Def4;
end;

:: deftheorem Def8 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
let V be Ring; ::_thesis: 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
let V1 be Subset of V; ::_thesis: ( V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty implies doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring )
assume A1: ( V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty ) ; ::_thesis: doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring
then A2: ( One_ (V1,V) = 1_ V & mult_ (V1,V) = the multF of V || V1 ) by Def6, Def8;
 ( Zero_ (V1,V) = 0. V & Add_ (V1,V) = the addF of V || V1 ) by A1, Def5, Def7;
hence  doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring by A1, A2, Th1; ::_thesis: verum
end;

begin


definition
let V be Algebra;
mode Subalgebra of V ->  Algebra means :Def9: :: 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 b1 being Algebra 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 | [:REAL, the carrier of b1:] & 1. b1 = 1. V & 0. b1 = 0. V )
proof
take  V ; ::_thesis: ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] & 1. V = 1. V & 0. V = 0. V )
thus  ( the carrier of V c= the carrier of V & the addF of V = the addF of V || the carrier of V & the multF of V = the multF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] & 1. V = 1. V & 0. V = 0. V ) by RELSET_1:19; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Subalgebra C0SP1:def_9_:_
 for V, b2 being Algebra holds
( b2 is Subalgebra 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 | [:REAL, the carrier of b2:] & 1. b2 = 1. V & 0. b2 = 0. V ) );

theorem Th3: :: 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
let X be non empty set ; ::_thesis: 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
let d1, d2 be Element of X; ::_thesis: 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
let A be BinOp of X; ::_thesis: 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
let M be Function of [:X,X:],X; ::_thesis: 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
let V be Algebra; ::_thesis: 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
let V1 be Subset of V; ::_thesis: 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
let MR be Function of [:REAL,X:],X; ::_thesis: ( 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 implies AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V )
assume that
A1: V1 = X and
A2: d1 = 0. V and
A3: d2 = 1. V and
A4: A = the addF of V || V1 and
A5: M = the multF of V || V1 and
A6: MR = the Mult of V | [:REAL,V1:] and
A7: for v being Element of V st v in V1 holds
- v in V1 ; :: according to C0SP1:def_1 ::_thesis: AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
reconsider W = AlgebraStr(# X,M,A,MR,d2,d1 #) as non empty AlgebraStr ;
A8: now__::_thesis:_for_x,_y_being_Element_of_W_holds_x_+_y_=_the_addF_of_V_._(x,y)
let x, y be Element of W; ::_thesis: x + y = the addF of V . (x,y)
 x + y = the addF of V . [x,y] by A1, A4, FUNCT_1:49;
hence  x + y = the addF of V . (x,y) ; ::_thesis: verum
end;
A9: now__::_thesis:_for_a,_x_being_VECTOR_of_W_holds_a_*_x_=_the_multF_of_V_._(a,x)
let a, x be VECTOR of W; ::_thesis: a * x = the multF of V . (a,x)
 a * x = the multF of V . [a,x] by A1, A5, FUNCT_1:49;
hence  a * x = the multF of V . (a,x) ; ::_thesis: verum
end;
A10: now__::_thesis:_for_a_being_Real
for_x_being_VECTOR_of_W_holds_a_*_x_=_the_Mult_of_V_._(a,x)
let a be Real; ::_thesis: for x being VECTOR of W holds a * x = the Mult of V . (a,x)
let x be VECTOR of W; ::_thesis: a * x = the Mult of V . (a,x)
 a * x = the Mult of V . [a,x] by A1, A6, FUNCT_1:49;
hence  a * x = the Mult of V . (a,x) ; ::_thesis: verum
end;
A11: ( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
set Mv = the multF of V;
set Av = the addF of V;
hereby  :: according to RLVECT_1:def_2 ::_thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let x, y be VECTOR of W; ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def_3;
 ( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence  x + y = y + x ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
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, TARSKI:def_3;
 x + (y + z) = the addF of V . (x1,(y + z)) by A8;
then A12: x + (y + z) = x1 + (y1 + z1) by A8;
 (x + y) + z = the addF of V . ((x + y),z1) by A8;
then  (x + y) + z = (x1 + y1) + z1 by A8;
hence  (x + y) + z = x + (y + z) by A12, RLVECT_1:def_3; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: ( W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let x be VECTOR of W; ::_thesis: x + (0. W) = x
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
thus x + (0. W) = y + (0. V) by A2, A8
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
thus  W is right_complementable ::_thesis: ( W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
proof
let x be Element of W; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as Element of V by A1, TARSKI:def_3;
consider v being Element of V such that
A13: x1 + v = 0. V by ALGSTR_0:def_11;
 v = - x1 by A13, VECTSP_1:16;
then reconsider y = v as Element of W by A1, A7;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. W
thus  x + y = 0. W by A2, A8, A13; ::_thesis: verum
end;
hereby  :: according to GROUP_1:def_12 ::_thesis: ( W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let v, w be Element of W; ::_thesis: v * w = w * v
reconsider v1 = v, w1 = w as Element of V by A1, TARSKI:def_3;
 ( v * w = v1 * w1 & w * v = w1 * v1 ) by A9;
hence  v * w = w * v ; ::_thesis: verum
end;
hereby  :: according to GROUP_1:def_3 ::_thesis: ( W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
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, TARSKI:def_3;
 a * (b * x) = the multF of V . (a,(b * x)) by A9;
then A14: a * (b * x) = a1 * (b1 * y) by A9;
 a * b = a1 * b1 by A9;
then  (a * b) * x = (a1 * b1) * y by A9;
hence  (a * b) * x = a * (b * x) by A14, GROUP_1:def_3; ::_thesis: verum
end;
hereby  :: according to VECTSP_1:def_4 ::_thesis: ( W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let v be Element of W; ::_thesis: v * (1. W) = v
reconsider v1 = v as Element of V by A1, TARSKI:def_3;
 v * (1. W) = v1 * (1. V) by A3, A9;
hence  v * (1. W) = v by VECTSP_1:def_4; ::_thesis: verum
end;
hereby  :: according to VECTSP_1:def_2 ::_thesis: ( W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
let x, y, z be Element of W; ::_thesis: x * (y + z) = (x * y) + (x * z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def_3;
 y + z = y1 + z1 by A8;
then  x * (y + z) = x1 * (y1 + z1) by A9;
then A15: x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def_2;
 ( x * y = x1 * y1 & x * z = x1 * z1 ) by A9;
hence  x * (y + z) = (x * y) + (x * z) by A8, A15; ::_thesis: verum
end;
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, TARSKI:def_3;
reconsider aa = a as Real by XREAL_0:def_1;
A16: aa * x = aa * x1 by A10;
 x + y = x1 + y1 by A8;
then  aa * (x + y) = aa * (x1 + y1) by A10;
then A17: a * (x + y) = (a * x1) + (a * y1) by RLVECT_1:def_5;
 aa * y = aa * y1 by A10;
hence  a * (x + y) = (a * x) + (a * y) by A8, A16, A17; ::_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)
reconsider aa = a, bb = b as Real by XREAL_0:def_1;
let x be Element of W; ::_thesis: (a + b) * x = (a * x) + (b * x)
reconsider x1 = x as Element of V by A1, TARSKI:def_3;
A18: aa * x = aa * x1 by A10;
A19: bb * x = bb * x1 by A10;
 (aa + bb) * x = (a + b) * x1 by A10;
then  (a + b) * x = (a * x1) + (b * x1) by RLVECT_1:def_6;
hence  (a + b) * x = (a * x) + (b * x) by A8, A18, A19; ::_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, TARSKI:def_3;
reconsider aa = a, bb = b as Real by XREAL_0:def_1;
A20: bb * x = bb * x1 by A10;
 (aa * bb) * x = (a * b) * x1 by A10;
then  (aa * bb) * x = a * (bb * x1) by RLVECT_1:def_7;
hence  (a * b) * x = a * (b * x) by A10, A20; ::_thesis: verum
end;
thus  W is vector-associative ::_thesis: verum
proof
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
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def_3;
let a be Real; ::_thesis: a * (x * y) = (a * x) * y
A21: a * x = a * x1 by A10;
 x * y = x1 * y1 by A9;
then  a * (x * y) = a * (x1 * y1) by A10;
then  a * (x * y) = (a * x1) * y1 by FUNCSDOM:def_9;
hence  a * (x * y) = (a * x) * y by A9, A21; ::_thesis: verum
end;
end;
 ( 0. W = 0. V & 1. W = 1. V ) by A2, A3;
hence  AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V by A1, A4, A5, A6, A11, Def9; ::_thesis: verum
end;

registration
let V be Algebra;
cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() strict vector-associative unital associative commutative right-distributive right_unital well-unital left_unital for Subalgebra of V;
existence
 ex b1 being Subalgebra of V st b1 is strict
proof
set V1 = [#] V;
A1: the Mult of V = the Mult of V | [:REAL,([#] V):] by RELSET_1:19;
 ( the addF of V = the addF of V || ([#] V) & the multF of V = the multF of V || ([#] V) ) by RELSET_1:19;
then  AlgebraStr(# the carrier of V, the multF of V, the addF of V, the Mult of V,(1. V),(0. V) #) is Subalgebra of V by A1, Th3;
hence  ex b1 being Subalgebra of V st b1 is strict ; ::_thesis: verum
end;
end;

definition
let V be Algebra;
let V1 be Subset of V;
attrV1 is additively-linearly-closed  means :Def10: :: 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 Def10 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 for Element of bool the carrier of V;
coherence
 for b1 being Subset of V st b1 is additively-linearly-closed holds
b1 is additively-closed
proof
now__::_thesis:_for_V1_being_Subset_of_V_st_V1_is_additively-linearly-closed_holds_
V1_is_additively-closed
let V1 be Subset of V; ::_thesis: ( V1 is additively-linearly-closed implies V1 is additively-closed )
assume  V1 is additively-linearly-closed ; ::_thesis: V1 is additively-closed
then  ( V1 is add-closed & V1 is having-inverse ) by Def10;
hence  V1 is additively-closed ; ::_thesis: verum
end;
hence  for b1 being Subset of V st b1 is additively-linearly-closed holds
b1 is additively-closed ; ::_thesis: verum
end;
end;

definition
let V be Algebra;
let V1 be Subset of V;
assume B1: ( V1 is additively-linearly-closed & not V1 is empty ) ;
func Mult_ (V1,V) ->  Function of [:REAL,V1:],V1 equals :Def11: :: C0SP1:def 11
 the Mult of V | [:REAL,V1:];
correctness
coherence
the Mult of V | [:REAL,V1:] is Function of [:REAL,V1:],V1;
proof
A1: ( [:REAL,V1:] c= [:REAL, the carrier of V:] & dom the Mult of V = [:REAL, the carrier of V:] ) by FUNCT_2:def_1, ZFMISC_1:95;
A2: for z being set st z in [:REAL,V1:] holds
( the Mult of V | [:REAL,V1:]) . z in V1
proof
let z be set ; ::_thesis: ( z in [:REAL,V1:] implies ( the Mult of V | [:REAL,V1:]) . z in V1 )
assume A3: z in [:REAL,V1:] ; ::_thesis: ( the Mult of V | [:REAL,V1:]) . z in V1
consider r, x being set  such that
A4: r in REAL and
A5: x in V1 and
A6: z = [r,x] by A3, ZFMISC_1:def_2;
reconsider r = r as Real by A4;
reconsider y = x as VECTOR of V by A5;
 [r,x] in dom ( the Mult of V | [:REAL,V1:]) by A1, A3, A6, RELAT_1:62;
then  ( the Mult of V | [:REAL,V1:]) . z = r * y by A6, FUNCT_1:47;
hence  ( the Mult of V | [:REAL,V1:]) . z in V1 by B1, A5, Def10; ::_thesis: verum
end;
 dom ( the Mult of V | [:REAL,V1:]) = [:REAL,V1:] by A1, RELAT_1:62;
hence  the Mult of V | [:REAL,V1:] is Function of [:REAL,V1:],V1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;

:: deftheorem Def11 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 ;
attrV is scalar-mult-cancelable  means :Def12: :: 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 Def12 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 Th4: :: C0SP1:4
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr
for a being Real holds a * (0. V) = 0. V
proof
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ; ::_thesis: for a being Real holds a * (0. V) = 0. V
let a be Real; ::_thesis: a * (0. V) = 0. V
 (a * (0. V)) + (a * (0. V)) = a * ((0. V) + (0. V)) by RLVECT_1:def_5;
then  (a * (0. V)) + (a * (0. V)) = a * (0. V) by RLVECT_1:4;
then  (a * (0. V)) + (a * (0. V)) = (a * (0. V)) + (0. V) by RLVECT_1:4;
hence  a * (0. V) = 0. V by RLVECT_1:8; ::_thesis: verum
end;

theorem :: C0SP1:5
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st V is scalar-mult-cancelable holds
V is RealLinearSpace
proof
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ; ::_thesis: ( V is scalar-mult-cancelable implies V is RealLinearSpace )
assume A1: V is scalar-mult-cancelable ; ::_thesis: V is RealLinearSpace
 for v being VECTOR of V holds 1 * v = v
proof
let v be VECTOR of V; ::_thesis: 1 * v = v
 (1 * v) + (1 * (- v)) = 1 * (v + (- v)) by RLVECT_1:def_5;
then  ( (1 * v) - (1 * v) = 0. V & (1 * v) + (1 * (- v)) = 1 * (0. V) ) by RLVECT_1:5;
then A2: - (1 * v) = 1 * (- v) by Th4, RLVECT_1:8;
1 * v = (1 * 1) * v
.= 1 * (1 * v) by RLVECT_1:def_7 ;
then  (1 * (1 * v)) - (1 * v) = 0. V by RLVECT_1:15;
then  1 * ((1 * v) - v) = 0. V by A2, RLVECT_1:def_5;
then  (1 * v) - v = 0. V by A1, Def12;
hence  1 * v = v by RLVECT_1:21; ::_thesis: verum
end;
hence  V is RealLinearSpace by RLVECT_1:def_8; ::_thesis: verum
end;

Lm3:  for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st ( for v being VECTOR of V holds 1 * v = v ) holds
V is RealLinearSpace
by RLVECT_1:def_8;

theorem Th6: :: 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
let V be Algebra; ::_thesis: 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
let V1 be Subset of V; ::_thesis: ( V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty implies AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V )
assume A1: ( V1 is additively-linearly-closed & V1 is multiplicatively-closed & not V1 is empty ) ; ::_thesis: AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V
then A2: Mult_ (V1,V) = the Mult of V | [:REAL,V1:] by Def11;
A3: ( One_ (V1,V) = 1_ V & mult_ (V1,V) = the multF of V || V1 ) by A1, Def6, Def8;
 ( Zero_ (V1,V) = 0. V & Add_ (V1,V) = the addF of V || V1 ) by A1, Def5, Def7;
hence  AlgebraStr(# V1,(mult_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Subalgebra of V by A1, A3, A2, Th3; ::_thesis: verum
end;

registration
let X be non empty set ;
cluster RAlgebra X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative 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 vector-distributive & RAlgebra X is scalar-distributive & RAlgebra X is scalar-associative & RAlgebra X is vector-associative );
;
end;

theorem Th7: :: C0SP1:7
for X being non empty set holds RAlgebra X is RealLinearSpace
proof
let X be non empty set ; ::_thesis: RAlgebra X is RealLinearSpace
 for v being VECTOR of (RAlgebra X) holds 1 * v = v by FUNCSDOM:12;
hence  RAlgebra X is RealLinearSpace by Lm3; ::_thesis: verum
end;

theorem Th8: :: 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
let V be Algebra; ::_thesis: 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 )
let V1 be Subalgebra of V; ::_thesis: ( ( 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 )
hereby  ::_thesis: ( ( 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 )
let x1, y1 be Element of V1; ::_thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 + y1 = x + y
let x, y be Element of V; ::_thesis: ( x1 = x & y1 = y implies x1 + y1 = x + y )
assume A1: ( x1 = x & y1 = y ) ; ::_thesis: x1 + y1 = x + y
 x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by Def9;
hence  x1 + y1 = x + y by A1, FUNCT_1:49; ::_thesis: verum
end;
hereby  ::_thesis: ( ( 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 )
let x1, y1 be Element of V1; ::_thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 * y1 = x * y
let x, y be Element of V; ::_thesis: ( x1 = x & y1 = y implies x1 * y1 = x * y )
assume A2: ( x1 = x & y1 = y ) ; ::_thesis: x1 * y1 = x * y
 x1 * y1 = ( the multF of V || the carrier of V1) . [x1,y1] by Def9;
hence  x1 * y1 = x * y by A2, FUNCT_1:49; ::_thesis: verum
end;
hereby  ::_thesis: ( 1_ V1 = 1_ V & 0. V1 = 0. V )
let v1 be Element of V1; ::_thesis: for v being Element of V
for a being Real st v1 = v holds
a * v1 = a * v
let v be Element of V; ::_thesis: for a being Real st v1 = v holds
a * v1 = a * v
let a be Real; ::_thesis: ( v1 = v implies a * v1 = a * v )
assume A3: v1 = v ; ::_thesis: a * v1 = a * v
 a * v1 = ( the Mult of V | [:REAL, the carrier of V1:]) . [a,v1] by Def9;
hence  a * v1 = a * v by A3, FUNCT_1:49; ::_thesis: verum
end;
thus  ( 1_ V1 = 1_ V & 0. V1 = 0. V ) by Def9; ::_thesis: verum
end;

begin

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
A1: not  {  f where f is Function of X,REAL : f | X is bounded  }  is empty
proof
reconsider g = X --> 0 as Function of X,REAL by FUNCOP_1:46;
 g | X is bounded ;
then  g in  {  f where f is Function of X,REAL : f | X is bounded  }  ;
hence  not  {  f where f is Function of X,REAL : f | X is bounded  }  is empty ; ::_thesis: verum
end;
  {  f where f is Function of X,REAL : f | X is bounded  }  c= Funcs (X,REAL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  f where f is Function of X,REAL : f | X is bounded  }  or x in Funcs (X,REAL) )
assume  x in  {  f where f is Function of X,REAL : f | X is bounded  }  ; ::_thesis: x in Funcs (X,REAL)
then  ex f being Function of X,REAL st
( x = f & f | X is bounded ) ;
hence  x in Funcs (X,REAL) by FUNCT_2:8; ::_thesis: verum
end;
hence   {  f where f is Function of X,REAL : f | X is bounded  }  is non empty Subset of (RAlgebra X) by A1; ::_thesis: verum
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 Th9: :: C0SP1:9
for X being non empty set holds
( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )
proof
let X be non empty set ; ::_thesis: ( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )
set W = BoundedFunctions X;
set V = RAlgebra X;
A1: for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v * u in BoundedFunctions X
proof
let v, u be Element of (RAlgebra X); ::_thesis: ( v in BoundedFunctions X & u in BoundedFunctions X implies v * u in BoundedFunctions X )
assume that
A2: v in BoundedFunctions X and
A3: u in BoundedFunctions X ; ::_thesis: v * u in BoundedFunctions X
consider u1 being Function of X,REAL such that
A4: u1 = u and
A5: u1 | X is bounded by A3;
reconsider h = v * u as Element of Funcs (X,REAL) ;
consider v1 being Function of X,REAL such that
A6: v1 = v and
A7: v1 | X is bounded by A2;
 dom (v1 (#) u1) = X /\ X by FUNCT_2:def_1;
then A8: (v1 (#) u1) | X is bounded by A7, A5, RFUNCT_1:84;
 (dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def_1;
then A9: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & (dom v1) /\ (dom u1) = X /\ X ) by FUNCT_2:def_1, FUNCT_2:def_2;
 for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A6, A4, FUNCSDOM:2;
then  v * u = v1 (#) u1 by A9, VALUED_1:def_4;
hence  v * u in BoundedFunctions X by A8; ::_thesis: verum
end;
reconsider g = RealFuncUnit X as Function of X,REAL ;
 for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v + u in BoundedFunctions X
proof
let v, u be Element of (RAlgebra X); ::_thesis: ( v in BoundedFunctions X & u in BoundedFunctions X implies v + u in BoundedFunctions X )
assume that
A10: v in BoundedFunctions X and
A11: u in BoundedFunctions X ; ::_thesis: v + u in BoundedFunctions X
consider u1 being Function of X,REAL such that
A12: u1 = u and
A13: u1 | X is bounded by A11;
reconsider h = v + u as Element of Funcs (X,REAL) ;
consider v1 being Function of X,REAL such that
A14: v1 = v and
A15: v1 | X is bounded by A10;
 dom (v1 + u1) = X /\ X by FUNCT_2:def_1;
then A16: (v1 + u1) | X is bounded by A15, A13, RFUNCT_1:83;
 (dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def_1;
then A17: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & (dom v1) /\ (dom u1) = X /\ X ) by FUNCT_2:def_1, FUNCT_2:def_2;
 for x being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A14, A12, FUNCSDOM:1;
then  v + u = v1 + u1 by A17, VALUED_1:def_1;
hence  v + u in BoundedFunctions X by A16; ::_thesis: verum
end;
then A18: BoundedFunctions X is add-closed by IDEAL_1:def_1;
A19: RAlgebra X is RealLinearSpace by Th7;
 for v being Element of (RAlgebra X) st v in BoundedFunctions X holds
- v in BoundedFunctions X
proof
let v be Element of (RAlgebra X); ::_thesis: ( v in BoundedFunctions X implies - v in BoundedFunctions X )
assume  v in BoundedFunctions X ; ::_thesis: - v in BoundedFunctions X
then consider v1 being Function of X,REAL such that
A20: v1 = v and
A21: v1 | X is bounded ;
A22: (- v1) | X is bounded by A21, RFUNCT_1:82;
reconsider h = - v, v2 = v as Element of Funcs (X,REAL) ;
A23: h = (- 1) * v by A19, RLVECT_1:16;
A24: 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 X ;
 h . x = (- 1) * (v2 . y) by A23, FUNCSDOM:4;
hence  h . x = - (v1 . x) by A20; ::_thesis: verum
end;
 ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & dom v1 = X ) by FUNCT_2:def_1, FUNCT_2:def_2;
then  - v = - v1 by A24, VALUED_1:9;
hence  - v in BoundedFunctions X by A22; ::_thesis: verum
end;
then A25: BoundedFunctions X is having-inverse by Def1;
 for a being Real
for u being Element of (RAlgebra X) st u in BoundedFunctions X holds
a * u in BoundedFunctions X
proof
let a be Real; ::_thesis: for u being Element of (RAlgebra X) st u in BoundedFunctions X holds
a * u in BoundedFunctions X
let u be Element of (RAlgebra X); ::_thesis: ( u in BoundedFunctions X implies a * u in BoundedFunctions X )
assume  u in BoundedFunctions X ; ::_thesis: a * u in BoundedFunctions X
then consider u1 being Function of X,REAL such that
A26: u1 = u and
A27: u1 | X is bounded ;
A28: (a (#) u1) | X is bounded by A27, RFUNCT_1:80;
reconsider h = a * u as Element of Funcs (X,REAL) ;
A29: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & dom u1 = X ) by FUNCT_2:def_1, FUNCT_2:def_2;
 for x being set st x in dom h holds
h . x = a * (u1 . x) by A26, FUNCSDOM:4;
then  a * u = a (#) u1 by A29, VALUED_1:def_5;
hence  a * u in BoundedFunctions X by A28; ::_thesis: verum
end;
hence  BoundedFunctions X is additively-linearly-closed by A18, A25, Def10; ::_thesis: BoundedFunctions X is multiplicatively-closed
 g | X is bounded ;
then  1. (RAlgebra X) in BoundedFunctions X ;
hence  BoundedFunctions X is multiplicatively-closed by A1, Def4; ::_thesis: verum
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 Th9;
end;

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 Th6;
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:10
for X being non empty set holds R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;

theorem :: C0SP1:11
for X being non empty set holds R_Algebra_of_BoundedFunctions X is RealLinearSpace
proof
let X be non empty set ; ::_thesis: R_Algebra_of_BoundedFunctions X is RealLinearSpace
now__::_thesis:_for_v_being_VECTOR_of_(R_Algebra_of_BoundedFunctions_X)_holds_1_*_v_=_v
let v be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: 1 * v = v
reconsider v1 = v as VECTOR of (RAlgebra X) by TARSKI:def_3;
 R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
then  1 * v = 1 * v1 by Th8;
hence  1 * v = v by FUNCSDOM:12; ::_thesis: verum
end;
hence  R_Algebra_of_BoundedFunctions X is RealLinearSpace by Lm3; ::_thesis: verum
end;


theorem Th12: :: 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
let X be non empty set ; ::_thesis: 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) )
let F, G, H be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: 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) )
let f, g, h be Function of X,REAL; ::_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) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (RAlgebra X) by TARSKI:def_3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby  ::_thesis: ( ( for x being Element of X holds h . x = (f . x) + (g . x) ) implies H = F + G )
assume A3: H = F + G ; ::_thesis: for x being Element of X holds h . x = (f . x) + (g . x)
let x be Element of X; ::_thesis: h . x = (f . x) + (g . x)
 h1 = f1 + g1 by A2, A3, Th8;
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, Th8; ::_thesis: verum
end;

theorem Th13: :: 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
let X be non empty set ; ::_thesis: 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) )
let a be Real; ::_thesis: 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) )
let F, G be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: 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) )
let f, g be Function of X,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) )
reconsider f1 = F, g1 = G as VECTOR of (RAlgebra X) by TARSKI:def_3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
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 X holds g . x = a * (f . x)
let x be Element of X; ::_thesis: g . x = a * (f . x)
 g1 = a * f1 by A2, A3, Th8;
hence  g . x = a * (f . x) by A1, FUNCSDOM:4; ::_thesis: verum
end;
assume  for x being Element 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, Th8; ::_thesis: verum
end;

theorem Th14: :: 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
let X be non empty set ; ::_thesis: 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) )
let F, G, H be VECTOR of (R_Algebra_of_BoundedFunctions X); ::_thesis: 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) )
let f, g, h be Function of X,REAL; ::_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) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (RAlgebra X) by TARSKI:def_3;
A2: R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
hereby  ::_thesis: ( ( for x being Element of X holds h . x = (f . x) * (g . x) ) implies H = F * G )
assume A3: H = F * G ; ::_thesis: for x being Element of X holds h . x = (f . x) * (g . x)
let x be Element of X; ::_thesis: h . x = (f . x) * (g . x)
 h1 = f1 * g1 by A2, A3, Th8;
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, Th8; ::_thesis: verum
end;

theorem Th15: :: C0SP1:15
for X being non empty set holds 0. (R_Algebra_of_BoundedFunctions X) = X --> 0
proof
let X be non empty set ; ::_thesis: 0. (R_Algebra_of_BoundedFunctions X) = X --> 0
 ( R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X & 0. (RAlgebra X) = X --> 0 ) by Th6;
hence  0. (R_Algebra_of_BoundedFunctions X) = X --> 0 by Th8; ::_thesis: verum
end;

theorem Th16: :: C0SP1:16
for X being non empty set holds 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1
proof
let X be non empty set ; ::_thesis: 1_ (R_Algebra_of_BoundedFunctions X) = X --> 1
 ( R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X & 1_ (RAlgebra X) = X --> 1 ) by Th6;
hence  1_ (R_Algebra_of_BoundedFunctions X) = X --> 1 by Th8; ::_thesis: verum
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 :Def15: :: C0SP1:def 15
( it = F & it | X is bounded );
correctness
existence
ex b1 being Function of X,REAL st
( b1 = F & b1 | X is bounded );
uniqueness
for b1, b2 being Function of X,REAL st b1 = F & b1 | X is bounded & b2 = F & b2 | X is bounded holds
b1 = b2;
by A1;
end;

:: deftheorem Def15 defines modetrans C0SP1:def_15_:_
 for X being non empty set
for F being set st F in BoundedFunctions X holds
for b3 being Function of X,REAL 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,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
set z = the Element of X;
A1: now__::_thesis:_for_z_being_set_st_z_in__{__(abs_(f_._x))_where_x_is_Element_of_X_:_verum__}__holds_
z_in_REAL
let z be set ; ::_thesis: ( z in  {  (abs (f . x)) where x is Element of X : verum  }  implies z in REAL )
now__::_thesis:_(_z_in__{__(abs_(f_._x))_where_x_is_Element_of_X_:_verum__}__implies_z_in_REAL_)
assume  z in  {  (abs (f . x)) where x is Element of X : verum  }  ; ::_thesis: z in REAL
then  ex x being Element of X st z = abs (f . x) ;
hence  z in REAL ; ::_thesis: verum
end;
hence  ( z in  {  (abs (f . x)) where x is Element of X : verum  }  implies z in REAL ) ; ::_thesis: verum
end;
 abs (f . the Element of X) in  {  (abs (f . x)) where x is Element of X : verum  }  ;
hence   {  (abs (f . x)) where x is Element of X : verum  }  is non empty Subset of REAL by A1, TARSKI:def_3; ::_thesis: verum
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 Th17: :: C0SP1:17
for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
PreNorms f is bounded_above
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f | X is bounded holds
PreNorms f is bounded_above
let f be Function of X,REAL; ::_thesis: ( f | X is bounded implies PreNorms f is bounded_above )
assume  f | X is bounded ; ::_thesis: PreNorms f is bounded_above
then consider K being real number  such that
A1: for x being set st x in X /\ (dom f) holds
abs (f . x) <= K by RFUNCT_1:73;
A2: X /\ (dom f) = X /\ X by FUNCT_2:def_1;
take  K ; :: according to XXREAL_2:def_10 ::_thesis: K is UpperBound of PreNorms f
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in PreNorms f or r <= K )
assume  r in PreNorms f ; ::_thesis: r <= K
then  ex t being Element of X st r = abs (f . t) ;
hence  r <= K by A1, A2; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for f being Function of X,REAL holds
( f | X is bounded iff PreNorms f is bounded_above )
let f be Function of X,REAL; ::_thesis: ( f | X is bounded iff PreNorms f is bounded_above )
now__::_thesis:_(_PreNorms_f_is_bounded_above_implies_ex_K_being_Real_st_f_|_X_is_bounded_)
reconsider K = upper_bound (PreNorms f) as Real ;
assume A1: PreNorms f is bounded_above ; ::_thesis: ex K being Real st f | X is bounded
take K = K; ::_thesis: f | X is bounded
now__::_thesis:_for_t_being_set_st_t_in_X_/\_(dom_f)_holds_
abs_(f_._t)_<=_K
let t be set ; ::_thesis: ( t in X /\ (dom f) implies abs (f . t) <= K )
assume  t in X /\ (dom f) ; ::_thesis: abs (f . t) <= K
then  abs (f . t) in PreNorms f ;
hence  abs (f . t) <= K by A1, SEQ_4:def_1; ::_thesis: verum
end;
hence  f | X is bounded by RFUNCT_1:73; ::_thesis: verum
end;
hence  ( f | X is bounded iff PreNorms f is bounded_above ) by Th17; ::_thesis: verum
end;

definition
let X be non empty set ;
func BoundedFunctionsNorm X ->  Function of (BoundedFunctions X),REAL means :Def17: :: C0SP1:def 17
 for x being set st x in BoundedFunctions X holds
it . x = upper_bound (PreNorms (modetrans (x,X)));
existence
 ex b1 being Function of (BoundedFunctions X),REAL st
for x being set st x in BoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X)))
proof
deffunc H1( set ) ->  Element of REAL = upper_bound (PreNorms (modetrans ($1,X)));
A1: for z being set st z in BoundedFunctions X holds
H1(z) in REAL ;
 ex f being Function of (BoundedFunctions X),REAL st
for x being set st x in BoundedFunctions X holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence  ex b1 being Function of (BoundedFunctions X),REAL st
for x being set st x in BoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X))) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (BoundedFunctions X),REAL st ( for x being set st x in BoundedFunctions X holds
b1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in BoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of (BoundedFunctions X),REAL; ::_thesis: ( ( for x being set st x in BoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in BoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in BoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) and
A3: for x being set st x in BoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in BoundedFunctions X holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in BoundedFunctions X implies NORM1 . z = NORM2 . z )
assume A5: z in BoundedFunctions X ; ::_thesis: NORM1 . z = NORM2 . z
 NORM1 . z = upper_bound (PreNorms (modetrans (z,X))) by A2, A5;
hence  NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
 ( dom NORM1 = BoundedFunctions X & dom NORM2 = BoundedFunctions X ) by FUNCT_2:def_1;
hence  NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines BoundedFunctionsNorm C0SP1:def_17_:_
 for X being non empty set
for b2 being Function of (BoundedFunctions X),REAL holds
( b2 = BoundedFunctionsNorm X iff for x being set st x in BoundedFunctions X holds
b2 . x = upper_bound (PreNorms (modetrans (x,X))) );

theorem Th19: :: C0SP1:19
for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
modetrans (f,X) = f
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f | X is bounded holds
modetrans (f,X) = f
let f be Function of X,REAL; ::_thesis: ( f | X is bounded implies modetrans (f,X) = f )
assume  f | X is bounded ; ::_thesis: modetrans (f,X) = f
then  f in BoundedFunctions X ;
hence  modetrans (f,X) = f by Def15; ::_thesis: verum
end;

theorem Th20: :: C0SP1:20
for X being non empty set
for f being Function of X,REAL st f | X is bounded holds
(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
proof
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f | X is bounded holds
(BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
let f be Function of X,REAL; ::_thesis: ( f | X is bounded implies (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f) )
reconsider f9 = f as set ;
assume A1: f | X is bounded ; ::_thesis: (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f)
then  f in BoundedFunctions X ;
then  (BoundedFunctionsNorm X) . f = upper_bound (PreNorms (modetrans (f9,X))) by Def17;
hence  (BoundedFunctionsNorm X) . f = upper_bound (PreNorms f) by A1, Th19; ::_thesis: verum
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;

Lm4: now__::_thesis:_for_X_being_non_empty_set_
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_)
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 ) )
set X1 = BoundedFunctions X;
reconsider f = x as Element of BoundedFunctions X ;
assume A1: e = One_ ((BoundedFunctions X),(RAlgebra X)) ; ::_thesis: ( x * e = x & e * x = x )
then  x * e = (mult_ ((BoundedFunctions X),(RAlgebra X))) . (f,(1_ (RAlgebra X))) by Def8;
then A2: x * e = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . (f,(1_ (RAlgebra X))) by Def6;
 e * x = (mult_ ((BoundedFunctions X),(RAlgebra X))) . ((1_ (RAlgebra X)),f) by A1, Def8;
then A3: e * x = ( the multF of (RAlgebra X) || (BoundedFunctions X)) . ((1_ (RAlgebra X)),f) by Def6;
A4: 1_ (RAlgebra X) = 1_ (R_Algebra_of_BoundedFunctions X) by Th16;
then  [f,(1_ (RAlgebra X))] in [:(BoundedFunctions X),(BoundedFunctions X):] by ZFMISC_1:87;
then  x * e = f * (1_ (RAlgebra X)) by A2, FUNCT_1:49;
hence  x * e = x by VECTSP_1:def_4; ::_thesis: e * x = x
 [(1_ (RAlgebra X)),f] in [:(BoundedFunctions X),(BoundedFunctions X):] by A4, ZFMISC_1:87;
then  e * x = (1_ (RAlgebra 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 R_Normed_Algebra_of_BoundedFunctions X ->  unital ;
correctness
coherence
R_Normed_Algebra_of_BoundedFunctions X is unital ;
proof
reconsider e = One_ ((BoundedFunctions X),(RAlgebra X)) as Element of (R_Normed_Algebra_of_BoundedFunctions X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm4; ::_thesis: verum
end;
end;

theorem Th21: :: C0SP1:21
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: 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;
A3: 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;
A4: 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
A5: x1 + v = 0. V by ALGSTR_0:def_11;
reconsider y = v as Element of W by A1;
 x + y = 0. W by A1, A5;
hence  x is right_complementable by ALGSTR_0:def_11; ::_thesis: verum
end;
A6: 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;
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 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;
A9: 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;
A10: W is vector-distributive
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;
A11: W is scalar-distributive
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
thus  verum ; ::_thesis: verum
end;
A12: W is scalar-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;
A13: W is vector-associative
proof
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
reconsider x1 = x, y1 = y as Element of V by A1;
let a be Real; ::_thesis: a * (x * y) = (a * x) * y
 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;
 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;
hence  W is Algebra by A9, A8, A4, A7, A6, A2, A3, A10, A11, A12, A13, 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;


theorem Th22: :: C0SP1:22
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Algebra
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is Algebra
 1. (R_Normed_Algebra_of_BoundedFunctions X) = 1_ (R_Algebra_of_BoundedFunctions X) ;
hence  R_Normed_Algebra_of_BoundedFunctions X is Algebra by Th21; ::_thesis: verum
end;

theorem Th23: :: C0SP1:23
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
let X be non empty set ; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = F
set X1 = BoundedFunctions X;
reconsider f1 = F as Element of BoundedFunctions X ;
A1: [1,f1] in [:REAL,(BoundedFunctions X):] by ZFMISC_1:87;
thus (Mult_ ((BoundedFunctions X),(RAlgebra X))) . (1,F) = ( the Mult of (RAlgebra X) | [:REAL,(BoundedFunctions X):]) . (1,f1) by Def11
.= the Mult of (RAlgebra X) . (1,f1) by A1, FUNCT_1:49
.= F by FUNCSDOM:12 ; ::_thesis: verum
end;

theorem Th24: :: C0SP1:24
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
 ( ( for v being VECTOR of (R_Normed_Algebra_of_BoundedFunctions X) holds 1 * v = v ) & R_Normed_Algebra_of_BoundedFunctions X is Algebra ) by Th22, Th23;
hence  R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace by Lm3; ::_thesis: verum
end;

theorem Th25: :: C0SP1:25
for X being non empty set holds X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X)
proof
let X be non empty set ; ::_thesis: X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X)
 X --> 0 = 0. (R_Algebra_of_BoundedFunctions X) by Th15;
hence  X --> 0 = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: verum
end;

theorem Th26: :: C0SP1:26
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
let X be non empty set ; ::_thesis: 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.||
let x be Element of X; ::_thesis: 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.||
let f be Function of X,REAL; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
abs (f . x) <= ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( f = F & f | X is bounded implies abs (f . x) <= ||.F.|| )
assume that
A1: f = F and
A2: f | X is bounded ; ::_thesis: abs (f . x) <= ||.F.||
A3: abs (f . x) in PreNorms f ;
 ( not PreNorms f is empty & PreNorms f is bounded_above ) by A2, Th17;
then  abs (f . x) <= upper_bound (PreNorms f) by A3, SEQ_4:def_1;
hence  abs (f . x) <= ||.F.|| by A1, A2, Th20; ::_thesis: verum
end;

theorem :: C0SP1:27
for X being non empty set
for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||
proof
let X be non empty set ; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds 0 <= ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: 0 <= ||.F.||
 F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A1: F = g and
A2: g | X is bounded ;
A3: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A2, Th17;
consider r0 being set  such that
A4: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A4;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume  r in PreNorms g ; ::_thesis: 0 <= r
then  ex t being Element of X st r = abs (g . t) ;
hence  0 <= r by COMPLEX1:46; ::_thesis: verum
end;
then  0 <= r0 by A4;
then  0 <= upper_bound (PreNorms g) by A3, A4, SEQ_4:def_1;
hence  0 <= ||.F.|| by A1, A2, Th20; ::_thesis: verum
end;

theorem Th28: :: C0SP1:28
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
let X be non empty set ; ::_thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st F = 0. (R_Normed_Algebra_of_BoundedFunctions X) holds
0 = ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies 0 = ||.F.|| )
set z = X --> 0;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:46;
 F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A1: g = F and
A2: g | X is bounded ;
A3: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A2, Th17;
consider r0 being set  such that
A4: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A4;
A5: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
assume A6: F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: 0 = ||.F.||
A7: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume  r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A8: r = abs (g . t) ;
 z = g by A6, A1, Th25;
then  abs (g . t) = abs 0 by FUNCOP_1:7;
hence  ( 0 <= r & r <= 0 ) by A8, ABSVALUE:2; ::_thesis: verum
end;
then  0 <= r0 by A4;
then  upper_bound (PreNorms g) = 0 by A7, A3, A4, A5, SEQ_4:def_1;
hence  0 = ||.F.|| by A1, A2, Th20; ::_thesis: verum
end;

theorem Th29: :: C0SP1:29
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
let X be non empty set ; ::_thesis: 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) )
let f, g, h be Function of X,REAL; ::_thesis: 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) )
let F, G, H be Point of (R_Normed_Algebra_of_BoundedFunctions 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_BoundedFunctions X) ;
A1: ( H = F + G iff h1 = f1 + g1 ) ;
assume  ( f = F & g = G & h = H ) ; ::_thesis: ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
hence  ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) by A1, Th12; ::_thesis: verum
end;

theorem Th30: :: C0SP1:30
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
let X be non empty set ; ::_thesis: 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) )
let a be Real; ::_thesis: 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) )
let f, g be Function of X,REAL; ::_thesis: 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) )
let F, G be Point of (R_Normed_Algebra_of_BoundedFunctions 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_BoundedFunctions X) ;
A1: ( G = a * F iff g1 = a * f1 ) ;
assume  ( f = F & g = G ) ; ::_thesis: ( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
hence  ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) by A1, Th13; ::_thesis: verum
end;

theorem Th31: :: C0SP1:31
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
let X be non empty set ; ::_thesis: 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) )
let f, g, h be Function of X,REAL; ::_thesis: 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) )
let F, G, H be Point of (R_Normed_Algebra_of_BoundedFunctions 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_BoundedFunctions X) ;
A1: ( H = F * G iff h1 = f1 * g1 ) ;
assume  ( f = F & g = G & h = H ) ; ::_thesis: ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
hence  ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) by A1, Th14; ::_thesis: verum
end;

theorem Th32: :: C0SP1:32
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
let X be non empty set ; ::_thesis: 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.|| )
let a be Real; ::_thesis: 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.|| )
let F, G be Point of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( ( ||.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.|| )
A1: now__::_thesis:_(_F_=_0._(R_Normed_Algebra_of_BoundedFunctions_X)_implies_||.F.||_=_0_)
set z = X --> 0;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:46;
 F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A2: F = g and
A3: g | X is bounded ;
A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A3, Th17;
consider r0 being set  such that
A5: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A5;
A6: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
assume  F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; ::_thesis: ||.F.|| = 0
then A7: z = g by A2, Th25;
A8: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume  r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A9: r = abs (g . t) ;
abs (g . t) = abs 0 by A7, FUNCOP_1:7
.= 0 by ABSVALUE:2 ;
hence  ( 0 <= r & r <= 0 ) by A9; ::_thesis: verum
end;
then  0 <= r0 by A5;
then  upper_bound (PreNorms g) = 0 by A8, A4, A5, A6, SEQ_4:def_1;
hence  ||.F.|| = 0 by A2, A3, Th20; ::_thesis: verum
end;
A10: ||.(F + G).|| <= ||.F.|| + ||.G.||
proof
 F + G in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A11: h1 = F + G and
A12: h1 | X is bounded ;
 G in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A13: g1 = G and
A14: g1 | X is bounded ;
 F in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A15: f1 = F and
A16: f1 | X is bounded ;
A17: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(h1_._t)_<=_||.F.||_+_||.G.||
let t be Element of X; ::_thesis: abs (h1 . t) <= ||.F.|| + ||.G.||
 ( abs (f1 . t) <= ||.F.|| & abs (g1 . t) <= ||.G.|| ) by A15, A16, A13, A14, Th26;
then A18: (abs (f1 . t)) + (abs (g1 . t)) <= ||.F.|| + ||.G.|| by XREAL_1:7;
 ( abs (h1 . t) = abs ((f1 . t) + (g1 . t)) & abs ((f1 . t) + (g1 . t)) <= (abs (f1 . t)) + (abs (g1 . t)) ) by A15, A13, A11, Th29, COMPLEX1:56;
hence  abs (h1 . t) <= ||.F.|| + ||.G.|| by A18, XXREAL_0:2; ::_thesis: verum
end;
A19: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_||.F.||_+_||.G.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= ||.F.|| + ||.G.|| )
assume  r in PreNorms h1 ; ::_thesis: r <= ||.F.|| + ||.G.||
then  ex t being Element of X st r = abs (h1 . t) ;
hence  r <= ||.F.|| + ||.G.|| by A17; ::_thesis: verum
end;
 ( ( for s being real number st s in PreNorms h1 holds
s <= ||.F.|| + ||.G.|| ) implies upper_bound (PreNorms h1) <= ||.F.|| + ||.G.|| ) by SEQ_4:45;
hence  ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A12, A19, Th20; ::_thesis: verum
end;
A20: ||.(a * F).|| = (abs a) * ||.F.||
proof
 F in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A21: f1 = F and
A22: f1 | X is bounded ;
 a * F in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A23: h1 = a * F and
A24: h1 | X is bounded ;
A25: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(h1_._t)_<=_(abs_a)_*_||.F.||
let t be Element of X; ::_thesis: abs (h1 . t) <= (abs a) * ||.F.||
 abs (h1 . t) = abs (a * (f1 . t)) by A21, A23, Th30;
then A26: abs (h1 . t) = (abs a) * (abs (f1 . t)) by COMPLEX1:65;
 0 <= abs a by COMPLEX1:46;
hence  abs (h1 . t) <= (abs a) * ||.F.|| by A21, A22, A26, Th26, XREAL_1:64; ::_thesis: verum
end;
A27: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_(abs_a)_*_||.F.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= (abs a) * ||.F.|| )
assume  r in PreNorms h1 ; ::_thesis: r <= (abs a) * ||.F.||
then  ex t being Element of X st r = abs (h1 . t) ;
hence  r <= (abs a) * ||.F.|| by A25; ::_thesis: verum
end;
 ( ( for s being real number st s in PreNorms h1 holds
s <= (abs a) * ||.F.|| ) implies upper_bound (PreNorms h1) <= (abs a) * ||.F.|| ) by SEQ_4:45;
then A28: ||.(a * F).|| <= (abs a) * ||.F.|| by A23, A24, A27, Th20;
percases ( a <> 0 or a = 0 ) ;
supposeA29: a <> 0 ; ::_thesis: ||.(a * F).|| = (abs a) * ||.F.||
A30: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(f1_._t)_<=_((abs_a)_")_*_||.(a_*_F).||
let t be Element of X; ::_thesis: abs (f1 . t) <= ((abs a) ") * ||.(a * F).||
 abs (a ") = abs (1 / a) ;
then A31: abs (a ") = 1 / (abs a) by ABSVALUE:7;
 h1 . t = a * (f1 . t) by A21, A23, Th30;
then  (a ") * (h1 . t) = ((a ") * a) * (f1 . t) ;
then A32: (a ") * (h1 . t) = 1 * (f1 . t) by A29, XCMPLX_0:def_7;
 ( abs ((a ") * (h1 . t)) = (abs (a ")) * (abs (h1 . t)) & 0 <= abs (a ") ) by COMPLEX1:46, COMPLEX1:65;
hence  abs (f1 . t) <= ((abs a) ") * ||.(a * F).|| by A23, A24, A32, A31, Th26, XREAL_1:64; ::_thesis: verum
end;
A33: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_
r_<=_((abs_a)_")_*_||.(a_*_F).||
let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= ((abs a) ") * ||.(a * F).|| )
assume  r in PreNorms f1 ; ::_thesis: r <= ((abs a) ") * ||.(a * F).||
then  ex t being Element of X st r = abs (f1 . t) ;
hence  r <= ((abs a) ") * ||.(a * F).|| by A30; ::_thesis: verum
end;
A34: 0 <= abs a by COMPLEX1:46;
 ( ( for s being real number st s in PreNorms f1 holds
s <= ((abs a) ") * ||.(a * F).|| ) implies upper_bound (PreNorms f1) <= ((abs a) ") * ||.(a * F).|| ) by SEQ_4:45;
then  ||.F.|| <= ((abs a) ") * ||.(a * F).|| by A21, A22, A33, Th20;
then  (abs a) * ||.F.|| <= (abs a) * (((abs a) ") * ||.(a * F).||) by A34, XREAL_1:64;
then A35: (abs a) * ||.F.|| <= ((abs a) * ((abs a) ")) * ||.(a * F).|| ;
 abs a <> 0 by A29, COMPLEX1:47;
then  (abs a) * ||.F.|| <= 1 * ||.(a * F).|| by A35, XCMPLX_0:def_7;
hence  ||.(a * F).|| = (abs a) * ||.F.|| by A28, XXREAL_0:1; ::_thesis: verum
end;
supposeA36: a = 0 ; ::_thesis: ||.(a * F).|| = (abs a) * ||.F.||
reconsider fz = F as VECTOR of (R_Algebra_of_BoundedFunctions X) ;
a * fz = (a + a) * fz by A36
.= (a * fz) + (a * fz) by RLVECT_1:def_6 ;
then  0. (R_Algebra_of_BoundedFunctions X) = (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:16;
then  0. (R_Algebra_of_BoundedFunctions X) = ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def_3;
then  0. (R_Algebra_of_BoundedFunctions X) = (0. (R_Algebra_of_BoundedFunctions X)) + (a * fz) by VECTSP_1:16;
then A37: a * F = 0. (R_Normed_Algebra_of_BoundedFunctions X) by RLVECT_1:4;
 (abs a) * ||.F.|| = 0 * ||.F.|| by A36, ABSVALUE:2;
hence  ||.(a * F).|| = (abs a) * ||.F.|| by A37, Th28; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_||.F.||_=_0_implies_F_=_0._(R_Normed_Algebra_of_BoundedFunctions_X)_)
set z = X --> 0;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:46;
 F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A38: F = g and
A39: g | X is bounded ;
assume A40: ||.F.|| = 0 ; ::_thesis: F = 0. (R_Normed_Algebra_of_BoundedFunctions X)
now__::_thesis:_for_t_being_Element_of_X_holds_g_._t_=_z_._t
let t be Element of X; ::_thesis: g . t = z . t
 abs (g . t) <= ||.F.|| by A38, A39, Th26;
then  abs (g . t) = 0 by A40, COMPLEX1:46;
hence g . t = 0 by ABSVALUE:2
.= z . t by FUNCOP_1:7 ;
::_thesis: verum
end;
then  g = z by FUNCT_2:63;
hence  F = 0. (R_Normed_Algebra_of_BoundedFunctions X) by A38, Th25; ::_thesis: verum
end;
hence  ( ( ||.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.|| ) by A1, A20, A10; ::_thesis: verum
end;

theorem Th33: :: C0SP1:33
for X being non empty set holds
( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )
proof
let X be non empty set ; ::_thesis: ( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )
thus  ||.(0. (R_Normed_Algebra_of_BoundedFunctions X)).|| = 0 by Th32; :: according to NORMSP_0:def_6 ::_thesis: ( R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like )
 for x, y being Point of (R_Normed_Algebra_of_BoundedFunctions X)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th32;
hence  ( R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum
end;

registration
let X be non empty set ;
cluster R_Normed_Algebra_of_BoundedFunctions X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
 ( R_Normed_Algebra_of_BoundedFunctions X is reflexive & R_Normed_Algebra_of_BoundedFunctions X is discerning & R_Normed_Algebra_of_BoundedFunctions X is RealNormSpace-like & R_Normed_Algebra_of_BoundedFunctions X is vector-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-distributive & R_Normed_Algebra_of_BoundedFunctions X is scalar-associative & R_Normed_Algebra_of_BoundedFunctions X is scalar-unital & 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 Th24, Th33;
end;

theorem Th34: :: C0SP1:34
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
let X be non empty set ; ::_thesis: 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) )
let f, g, h be Function of X,REAL; ::_thesis: 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) )
let F, G, H be Point of (R_Normed_Algebra_of_BoundedFunctions 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:_(_(_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)_implies_F_-_G_=_H_)
assume A3: 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 A3;
hence  (h . x) + (g . x) = f . x ; ::_thesis: verum
end;
then  F = H + G by A1, Th29;
then  F - G = H + (G - G) by RLVECT_1:def_3;
then  F - G = H + (0. (R_Normed_Algebra_of_BoundedFunctions X)) by RLVECT_1:15;
hence  F - G = H by RLVECT_1:4; ::_thesis: verum
end;
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_BoundedFunctions X)) by RLVECT_1:15;
then A4: 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, A4, Th29;
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;
hence  ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) by A2; ::_thesis: verum
end;

theorem Th35: :: C0SP1:35
for X being non empty set
for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X be non empty set ; ::_thesis: for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_Normed_Algebra_of_BoundedFunctions X); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
defpred S1[ set , set ] means  ex xseq being Real_Sequence st
( ( for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . $1 ) & xseq is convergent & $2 = lim xseq );
assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
A2: for x being Element of X ex y being Element of REAL st S1[x,y]
proof
let x be Element of X; ::_thesis: ex y being Element of REAL st S1[x,y]
deffunc H1( Element of NAT ) ->  Element of REAL = (modetrans ((vseq . $1),X)) . x;
consider xseq being Real_Sequence such that
A3: for n being Element of NAT holds xseq . n = H1(n) from FUNCT_2:sch_4();
take  lim xseq ; ::_thesis: S1[x, lim xseq]
A4: for m, k being Element of NAT holds abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
 (vseq . m) - (vseq . k) in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A5: h1 = (vseq . m) - (vseq . k) and
A6: h1 | X is bounded ;
 vseq . m in BoundedFunctions X ;
then  ex vseqm being Function of X,REAL st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A7: modetrans ((vseq . m),X) = vseq . m by Th19;
 vseq . k in BoundedFunctions X ;
then  ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A8: modetrans ((vseq . k),X) = vseq . k by Th19;
 ( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A3;
then  (xseq . m) - (xseq . k) = h1 . x by A7, A8, A5, Th34;
hence  abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).|| by A5, A6, Th26; ::_thesis: verum
end;
now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_((xseq_._n)_-_(xseq_._k))_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e )
assume A9: e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e
 e is Real by XREAL_0:def_1;
then consider k being Element of NAT  such that
A10: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A9, RSSPACE3:8;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs ((xseq . n) - (xseq . k)) < e
hereby  ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n >= k implies abs ((xseq . n) - (xseq . k)) < e )
assume  n >= k ; ::_thesis: abs ((xseq . n) - (xseq . k)) < e
then A11: ||.((vseq . n) - (vseq . k)).|| < e by A10;
 abs ((xseq . n) - (xseq . k)) <= ||.((vseq . n) - (vseq . k)).|| by A4;
hence  abs ((xseq . n) - (xseq . k)) < e by A11, XXREAL_0:2; ::_thesis: verum
end;
end;
then  xseq is convergent by SEQ_4:41;
hence  S1[x, lim xseq] by A3; ::_thesis: verum
end;
consider tseq being Function of X,REAL such that
A12: for x being Element of X holds S1[x,tseq . x] from FUNCT_2:sch_3(A2);
now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume A13: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
reconsider e = e1 as Real by XREAL_0:def_1;
consider k being Element of NAT  such that
A14: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A13, RSSPACE3:8;
take k = k; ::_thesis: for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let m be Element of NAT ; ::_thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
A15: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def_4;
assume  m >= k ; ::_thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
then A16: ||.((vseq . m) - (vseq . k)).|| < e by A14;
 ( abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by NORMSP_0:def_4, NORMSP_1:9;
hence  abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A16, A15, XXREAL_0:2; ::_thesis: verum
end;
hence  for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ; ::_thesis: verum
end;
then A17: ||.vseq.|| is convergent by SEQ_4:41;
now__::_thesis:_for_x_being_set_st_x_in_X_/\_(dom_tseq)_holds_
abs_(tseq_._x)_<=_lim_||.vseq.||
let x be set ; ::_thesis: ( x in X /\ (dom tseq) implies abs (tseq . x) <= lim ||.vseq.|| )
assume A18: x in X /\ (dom tseq) ; ::_thesis: abs (tseq . x) <= lim ||.vseq.||
then consider xseq being Real_Sequence such that
A19: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A20: ( xseq is convergent & tseq . x = lim xseq ) by A12;
A21: for n being Element of NAT holds (abs xseq) . n <= ||.vseq.|| . n
proof
let n be Element of NAT ; ::_thesis: (abs xseq) . n <= ||.vseq.|| . n
A22: xseq . n = (modetrans ((vseq . n),X)) . x by A19;
 vseq . n in BoundedFunctions X ;
then A23: ex h1 being Function of X,REAL st
( vseq . n = h1 & h1 | X is bounded ) ;
then  modetrans ((vseq . n),X) = vseq . n by Th19;
then  abs (xseq . n) <= ||.(vseq . n).|| by A18, A23, A22, Th26;
then  (abs xseq) . n <= ||.(vseq . n).|| by VALUED_1:18;
hence  (abs xseq) . n <= ||.vseq.|| . n by NORMSP_0:def_4; ::_thesis: verum
end;
 ( abs xseq is convergent & abs (tseq . x) = lim (abs xseq) ) by A20, SEQ_4:14;
hence  abs (tseq . x) <= lim ||.vseq.|| by A17, A21, SEQ_2:18; ::_thesis: verum
end;
then  tseq | X is bounded by RFUNCT_1:73;
then  tseq in BoundedFunctions X ;
then reconsider tv = tseq as Point of (R_Normed_Algebra_of_BoundedFunctions X) ;
A24: 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
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= 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
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e )
assume  e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
then consider k being Element of NAT  such that
A25: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, RSSPACE3:8;
take  k ; ::_thesis: for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
for_x_being_Element_of_X_holds_abs_(((modetrans_((vseq_._n),X))_._x)_-_(tseq_._x))_<=_e
let n be Element of NAT ; ::_thesis: ( n >= k implies for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e )
assume A26: n >= k ; ::_thesis: for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
now__::_thesis:_for_x_being_Element_of_X_holds_abs_(((modetrans_((vseq_._n),X))_._x)_-_(tseq_._x))_<=_e
let x be Element of X; ::_thesis: abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e
consider xseq being Real_Sequence such that
A27: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X)) . x and
A28: xseq is convergent and
A29: tseq . x = lim xseq by A12;
reconsider fseq = NAT --> (xseq . n) as Real_Sequence ;
set wseq = xseq - fseq;
deffunc H1( Element of NAT ) ->  Element of REAL = abs ((xseq . $1) - (xseq . n));
consider rseq being Real_Sequence such that
A30: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A31: for m, k being Element of NAT holds abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).||
 (vseq . m) - (vseq . k) in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A32: h1 = (vseq . m) - (vseq . k) and
A33: h1 | X is bounded ;
 vseq . m in BoundedFunctions X ;
then  ex vseqm being Function of X,REAL st
( vseq . m = vseqm & vseqm | X is bounded ) ;
then A34: modetrans ((vseq . m),X) = vseq . m by Th19;
 vseq . k in BoundedFunctions X ;
then  ex vseqk being Function of X,REAL st
( vseq . k = vseqk & vseqk | X is bounded ) ;
then A35: modetrans ((vseq . k),X) = vseq . k by Th19;
 ( xseq . m = (modetrans ((vseq . m),X)) . x & xseq . k = (modetrans ((vseq . k),X)) . x ) by A27;
then  (xseq . m) - (xseq . k) = h1 . x by A34, A35, A32, Th34;
hence  abs ((xseq . m) - (xseq . k)) <= ||.((vseq . m) - (vseq . k)).|| by A32, A33, Th26; ::_thesis: verum
end;
A36: for m being Element of NAT st m >= k holds
rseq . m <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e )
assume  m >= k ; ::_thesis: rseq . m <= e
then A37: ||.((vseq . n) - (vseq . m)).|| < e by A25, A26;
 rseq . m = abs ((xseq . m) - (xseq . n)) by A30;
then  rseq . m = abs ((xseq . n) - (xseq . m)) by COMPLEX1:60;
then  rseq . m <= ||.((vseq . n) - (vseq . m)).|| by A31;
hence  rseq . m <= e by A37, XXREAL_0:2; ::_thesis: verum
end;
A38: now__::_thesis:_for_m_being_Element_of_NAT_holds_(xseq_-_fseq)_._m_=_(xseq_._m)_-_(xseq_._n)
let m be Element of NAT ; ::_thesis: (xseq - fseq) . m = (xseq . m) - (xseq . n)
 (xseq - fseq) . m = (xseq . m) + ((- fseq) . m) by SEQ_1:7;
then  (xseq - fseq) . m = (xseq . m) + (- (fseq . m)) by SEQ_1:10;
hence  (xseq - fseq) . m = (xseq . m) - (xseq . n) by FUNCOP_1:7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
rseq_._x_=_(abs_(xseq_-_fseq))_._x
let x be set ; ::_thesis: ( x in NAT implies rseq . x = (abs (xseq - fseq)) . x )
assume  x in NAT ; ::_thesis: rseq . x = (abs (xseq - fseq)) . x
then reconsider k = x as Element of NAT ;
 rseq . x = abs ((xseq . k) - (xseq . n)) by A30;
then  rseq . x = abs ((xseq - fseq) . k) by A38;
hence  rseq . x = (abs (xseq - fseq)) . x by VALUED_1:18; ::_thesis: verum
end;
then A39: rseq = abs (xseq - fseq) by FUNCT_2:12;
A40: xseq - fseq is convergent by A28, SEQ_2:11;
then  rseq is convergent by A39;
then A41: lim rseq <= e by A36, RSSPACE2:5;
 lim fseq = fseq . 0 by SEQ_4:26;
then  lim fseq = xseq . n by FUNCOP_1:7;
then  lim (xseq - fseq) = (tseq . x) - (xseq . n) by A28, A29, SEQ_2:12;
then  lim rseq = abs ((tseq . x) - (xseq . n)) by A40, A39, SEQ_4:14;
then  abs ((xseq . n) - (tseq . x)) <= e by A41, COMPLEX1:60;
hence  abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e by A27; ::_thesis: verum
end;
hence  for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e ; ::_thesis: verum
end;
hence  for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e ; ::_thesis: verum
end;
A42: 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
A43: for n being Element of NAT st n >= k holds
for x being Element of X holds abs (((modetrans ((vseq . n),X)) . x) - (tseq . x)) <= e by A24;
take  k ; ::_thesis: for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
hereby  ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A44: n >= k ; ::_thesis: ||.((vseq . n) - tv).|| <= e
 vseq . n in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A45: f1 = vseq . n and
 f1 | X is bounded ;
 (vseq . n) - tv in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A46: h1 = (vseq . n) - tv and
A47: h1 | X is bounded ;
A48: now__::_thesis:_for_t_being_Element_of_X_holds_abs_(h1_._t)_<=_e
let t be Element of X; ::_thesis: abs (h1 . t) <= e
 ( modetrans ((vseq . n),X) = f1 & h1 . t = (f1 . t) - (tseq . t) ) by A45, A46, Def15, Th34;
hence  abs (h1 . t) <= e by A43, A44; ::_thesis: verum
end;
A49: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_e
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= e )
assume  r in PreNorms h1 ; ::_thesis: r <= e
then  ex t being Element of X st r = abs (h1 . t) ;
hence  r <= e by A48; ::_thesis: verum
end;
 ( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
hence  ||.((vseq . n) - tv).|| <= e by A46, A47, A49, Th20; ::_thesis: verum
end;
end;
 for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A50: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT  such that
A51: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A42, A50, XREAL_1:215;
take  m ; ::_thesis: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
A52: e / 2 < e by A50, XREAL_1:216;
hereby  ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume  n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
then  ||.((vseq . n) - tv).|| <= e / 2 by A51;
hence  ||.((vseq . n) - tv).|| < e by A52, XXREAL_0:2; ::_thesis: verum
end;
end;
hence  vseq is convergent by NORMSP_1:def_6; ::_thesis: verum
end;

theorem Th36: :: C0SP1:36
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace
 for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th35;
hence  R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace by LOPBAN_1:def_15; ::_thesis: verum
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 Th36;
end;

theorem :: C0SP1:37
for X being non empty set holds R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra
proof
let X be non empty set ; ::_thesis: R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra
set B = R_Normed_Algebra_of_BoundedFunctions X;
reconsider B = R_Normed_Algebra_of_BoundedFunctions X as Normed_Algebra by Th22;
 1. B in BoundedFunctions X ;
then consider ONE being Function of X,REAL such that
A1: ONE = 1. B and
A2: ONE | X is bounded ;
 1. B = 1_ (R_Algebra_of_BoundedFunctions X) ;
then A3: 1. B = X --> 1 by Th16;
 for s being set holds
( s in PreNorms ONE iff s = 1 )
proof
set t = the Element of X;
let s be set ; ::_thesis: ( s in PreNorms ONE iff s = 1 )
A4: (X --> 1) . the Element of X = 1 by FUNCOP_1:7;
hereby  ::_thesis: ( s = 1 implies s in PreNorms ONE )
assume  s in PreNorms ONE ; ::_thesis: s = 1
then consider t being Element of X such that
A5: s = abs ((X --> 1) . t) by A1, A3;
 (X --> 1) . t = 1 by FUNCOP_1:7;
hence  s = 1 by A5, COMPLEX1:48; ::_thesis: verum
end;
assume  s = 1 ; ::_thesis: s in PreNorms ONE
then  s = abs ((X --> 1) . the Element of X) by A4, COMPLEX1:48;
hence  s in PreNorms ONE by A1, A3; ::_thesis: verum
end;
then  PreNorms ONE = {1} by TARSKI:def_1;
then  upper_bound (PreNorms ONE) = 1 by SEQ_4:9;
then A6: ||.(1. B).|| = 1 by A1, A2, Th20;
A7: now__::_thesis:_for_a_being_Real
for_f,_g_being_Element_of_B_holds_a_*_(f_*_g)_=_f_*_(a_*_g)
let a be Real; ::_thesis: for f, g being Element of B holds a * (f * g) = f * (a * g)
let f, g be Element of B; ::_thesis: a * (f * g) = f * (a * g)
 f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A8: f1 = f and
 f1 | X is bounded ;
 g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A9: g1 = g and
 g1 | X is bounded ;
 a * (f * g) in BoundedFunctions X ;
then consider h3 being Function of X,REAL such that
A10: h3 = a * (f * g) and
 h3 | X is bounded ;
 f * g in BoundedFunctions X ;
then consider h2 being Function of X,REAL such that
A11: h2 = f * g and
 h2 | X is bounded ;
 a * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A12: h1 = a * g and
 h1 | X is bounded ;
now__::_thesis:_for_x_being_Element_of_X_holds_h3_._x_=_(f1_._x)_*_(h1_._x)
let x be Element of X; ::_thesis: h3 . x = (f1 . x) * (h1 . x)
 h3 . x = a * (h2 . x) by A11, A10, Th30;
then  h3 . x = a * ((f1 . x) * (g1 . x)) by A8, A9, A11, Th31;
then  h3 . x = (f1 . x) * (a * (g1 . x)) ;
hence  h3 . x = (f1 . x) * (h1 . x) by A9, A12, Th30; ::_thesis: verum
end;
hence  a * (f * g) = f * (a * g) by A8, A12, A10, Th31; ::_thesis: verum
end;
A13: now__::_thesis:_for_f,_g_being_Element_of_B_holds_||.(f_*_g).||_<=_||.f.||_*_||.g.||
let f, g be Element of B; ::_thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
 f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A14: f1 = f and
A15: f1 | X is bounded ;
 g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A16: g1 = g and
A17: g1 | X is bounded ;
A18: ( not PreNorms g1 is empty & PreNorms g1 is bounded_above ) by A17, Th17;
 f * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A19: h1 = f * g and
A20: h1 | X is bounded ;
A21: ( not PreNorms f1 is empty & PreNorms f1 is bounded_above ) by A15, Th17;
now__::_thesis:_for_s_being_real_number_st_s_in_PreNorms_h1_holds_
s_<=_(upper_bound_(PreNorms_f1))_*_(upper_bound_(PreNorms_g1))
let s be real number ; ::_thesis: ( s in PreNorms h1 implies s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) )
assume  s in PreNorms h1 ; ::_thesis: s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
then consider t being Element of X such that
A22: s = abs (h1 . t) ;
 abs (g1 . t) in PreNorms g1 ;
then A23: abs (g1 . t) <= upper_bound (PreNorms g1) by A18, SEQ_4:def_1;
 abs (f1 . t) in PreNorms f1 ;
then A24: abs (f1 . t) <= upper_bound (PreNorms f1) by A21, SEQ_4:def_1;
then  0 <= upper_bound (PreNorms f1) by COMPLEX1:46;
then A25: (upper_bound (PreNorms f1)) * (abs (g1 . t)) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A23, XREAL_1:64;
 0 <= abs (g1 . t) by COMPLEX1:46;
then A26: (abs (f1 . t)) * (abs (g1 . t)) <= (upper_bound (PreNorms f1)) * (abs (g1 . t)) by A24, XREAL_1:64;
 abs (h1 . t) = abs ((f1 . t) * (g1 . t)) by A14, A16, A19, Th31;
then  abs (h1 . t) = (abs (f1 . t)) * (abs (g1 . t)) by COMPLEX1:65;
hence  s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A22, A26, A25, XXREAL_0:2; ::_thesis: verum
end;
then A27: upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by SEQ_4:45;
A28: ||.g.|| = upper_bound (PreNorms g1) by A16, A17, Th20;
 ||.f.|| = upper_bound (PreNorms f1) by A14, A15, Th20;
hence  ||.(f * g).|| <= ||.f.|| * ||.g.|| by A19, A20, A28, A27, Th20; ::_thesis: verum
end;
A29: now__::_thesis:_for_f,_g,_h_being_Element_of_B_holds_(g_+_h)_*_f_=_(g_*_f)_+_(h_*_f)
let f, g, h be Element of B; ::_thesis: (g + h) * f = (g * f) + (h * f)
 f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A30: f1 = f and
 f1 | X is bounded ;
 h in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A31: h1 = h and
 h1 | X is bounded ;
 g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A32: g1 = g and
 g1 | X is bounded ;
 (g + h) * f in BoundedFunctions X ;
then consider F1 being Function of X,REAL such that
A33: F1 = (g + h) * f and
 F1 | X is bounded ;
 h * f in BoundedFunctions X ;
then consider hf1 being Function of X,REAL such that
A34: hf1 = h * f and
 hf1 | X is bounded ;
 g * f in BoundedFunctions X ;
then consider gf1 being Function of X,REAL such that
A35: gf1 = g * f and
 gf1 | X is bounded ;
 g + h in BoundedFunctions X ;
then consider gPh1 being Function of X,REAL such that
A36: gPh1 = g + h and
 gPh1 | X is bounded ;
now__::_thesis:_for_x_being_Element_of_X_holds_F1_._x_=_(gf1_._x)_+_(hf1_._x)
let x be Element of X; ::_thesis: F1 . x = (gf1 . x) + (hf1 . x)
 F1 . x = (gPh1 . x) * (f1 . x) by A30, A36, A33, Th31;
then  F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x) by A32, A31, A36, Th29;
then  F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)) ;
then  F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x)) by A30, A32, A35, Th31;
hence  F1 . x = (gf1 . x) + (hf1 . x) by A30, A31, A34, Th31; ::_thesis: verum
end;
hence  (g + h) * f = (g * f) + (h * f) by A35, A34, A33, Th29; ::_thesis: verum
end;
 for f being Element of B holds (1. B) * f = f by Lm4;
then  B is left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Algebra by A13, A6, A7, A29, LOPBAN_2:def_9, LOPBAN_2:def_10, LOPBAN_2:def_11, VECTSP_1:def_3, VECTSP_1:def_8;
hence  R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra ; ::_thesis: verum
end;