set W = ComplexBoundedFunctions X;
set V = CAlgebra X;
for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v + u in ComplexBoundedFunctions X

proof

let v, u be Element of (CAlgebra X); :: thesis: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v + u in ComplexBoundedFunctions X )
assume A2: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis: v + u in ComplexBoundedFunctions X
consider v1 being Function of X,COMPLEX such that
A3: ( v1 = v & v1 | X is bounded ) by A2;
consider u1 being Function of X,COMPLEX such that
A4: ( u1 = u & u1 | X is bounded ) by A2;
dom (v1 + u1) = X /\ X by FUNCT_2:def 1;
then A5: ( v1 + u1 is Function of X,COMPLEX & (v1 + u1) | X is bounded ) by A3, A4, CFUNCT_1:87;
reconsider h = v + u as Element of Funcs (X,COMPLEX) ;
A6: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def 1;
then A7: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A3, A4, CFUNCDOM:1;
then v + u = v1 + u1 by A7, A6, VALUED_1:def 1;
hence v + u in ComplexBoundedFunctions X by A5; :: thesis: verum

end;

then A8: ComplexBoundedFunctions X is add-closed by IDEAL_1:def 1;
for v being Element of (CAlgebra X) st v in ComplexBoundedFunctions X holds
- v in ComplexBoundedFunctions X

proof

let v be Element of (CAlgebra X); :: thesis: ( v in ComplexBoundedFunctions X implies - v in ComplexBoundedFunctions X )
assume A9: v in ComplexBoundedFunctions X ; :: thesis: - v in ComplexBoundedFunctions X
consider v1 being Function of X,COMPLEX such that
A10: ( v1 = v & v1 | X is bounded ) by A9;
A11: ( - v1 is Function of X,COMPLEX & (- v1) | X is bounded ) by A10, CFUNCT_1:86;
reconsider h = - v, v2 = v as Element of Funcs (X,COMPLEX) ;
A12: h = (- 1r) * v by CLVECT_1:4;
A13: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;
A14: dom v1 = X by FUNCT_2:def 1;

now

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 = (- 1r) * (v2 . y) by A12, CFUNCDOM:6;
hence h . x = - (v1 . x) by A10; :: thesis: verum

end;

then - v = - v1 by A14, A13, VALUED_1:9;
hence - v in ComplexBoundedFunctions X by A11; :: thesis: verum

end;

then A15: ComplexBoundedFunctions X is having-inverse by C0SP1:def 1;
for a being Complex
for u being Element of (CAlgebra X) st u in ComplexBoundedFunctions X holds
a * u in ComplexBoundedFunctions X

proof

let a be Complex; :: thesis: for u being Element of (CAlgebra X) st u in ComplexBoundedFunctions X holds
a * u in ComplexBoundedFunctions X
let u be Element of (CAlgebra X); :: thesis: ( u in ComplexBoundedFunctions X implies a * u in ComplexBoundedFunctions X )
assume A16: u in ComplexBoundedFunctions X ; :: thesis: a * u in ComplexBoundedFunctions X
consider u1 being Function of X,COMPLEX such that
A17: ( u1 = u & u1 | X is bounded ) by A16;
A18: ( a (#) u1 is Function of X,COMPLEX & (a (#) u1) | X is bounded ) by A17, CFUNCT_1:84;
reconsider h = a * u as Element of Funcs (X,COMPLEX) ;
A19: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;
A20: dom u1 = X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = a * (u1 . x) by A17, CFUNCDOM:6;
then a * u = a (#) u1 by A20, A19, VALUED_1:def 5;
hence a * u in ComplexBoundedFunctions X by A18; :: thesis: verum

end;

hence ComplexBoundedFunctions X is Cadditively-linearly-closed by A8, A15, Def10; :: thesis: ComplexBoundedFunctions X is multiplicatively-closed
A21: for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v * u in ComplexBoundedFunctions X

proof

let v, u be Element of (CAlgebra X); :: thesis: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v * u in ComplexBoundedFunctions X )
assume A22: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis: v * u in ComplexBoundedFunctions X
consider v1 being Function of X,COMPLEX such that
A23: ( v1 = v & v1 | X is bounded ) by A22;
consider u1 being Function of X,COMPLEX such that
A24: ( u1 = u & u1 | X is bounded ) by A22;
dom (v1 (#) u1) = X /\ X by FUNCT_2:def 1;
then A25: ( v1 (#) u1 is Function of X,COMPLEX & (v1 (#) u1) | X is bounded ) by A23, A24, CFUNCT_1:88;
reconsider h = v * u as Element of Funcs (X,COMPLEX) ;
A26: ex f being Function st
( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def 1;
then A27: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A23, A24, CFUNCDOM:2;
then v * u = v1 (#) u1 by A27, A26, VALUED_1:def 4;
hence v * u in ComplexBoundedFunctions X by A25; :: thesis: verum

end;

reconsider g = ComplexFuncUnit X as Function of X,COMPLEX ;
g | X is bounded ;
then 1. (CAlgebra X) in ComplexBoundedFunctions X ;
hence ComplexBoundedFunctions X is multiplicatively-closed by C0SP1:def 4, A21; :: thesis: verum