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

for v being Element of (CAlgebra X) st v in ComplexBoundedFunctions X holds

- v in ComplexBoundedFunctions X

for a being Complex

for u being Element of (CAlgebra X) st u in ComplexBoundedFunctions X holds

a * u in ComplexBoundedFunctions X

A20: for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds

v * u in ComplexBoundedFunctions X

g | X is bounded ;

then 1. (CAlgebra X) in ComplexBoundedFunctions X ;

hence ComplexBoundedFunctions X is multiplicatively-closed by A20; :: thesis: verum

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

then A7:
ComplexBoundedFunctions X is add-closed
by IDEAL_1:def 1;
let v, u be Element of (CAlgebra X); :: thesis: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v + u in ComplexBoundedFunctions X )

assume A1: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis: v + u in ComplexBoundedFunctions X

consider v1 being Function of X,COMPLEX such that

A2: ( v1 = v & v1 | X is bounded ) by A1;

consider u1 being Function of X,COMPLEX such that

A3: ( u1 = u & u1 | X is bounded ) by A1;

dom (v1 + u1) = X /\ X by FUNCT_2:def 1;

then A4: ( v1 + u1 is Function of X,COMPLEX & (v1 + u1) | X is bounded ) by A2, A3, CFUNCT_1:75;

reconsider h = v + u as Element of Funcs (X,COMPLEX) ;

A5: 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 A6: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;

for x being object st x in dom h holds

h . x = (v1 . x) + (u1 . x) by A2, A3, CFUNCDOM:1;

then v + u = v1 + u1 by A6, A5, VALUED_1:def 1;

hence v + u in ComplexBoundedFunctions X by A4; :: thesis: verum

end;assume A1: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis: v + u in ComplexBoundedFunctions X

consider v1 being Function of X,COMPLEX such that

A2: ( v1 = v & v1 | X is bounded ) by A1;

consider u1 being Function of X,COMPLEX such that

A3: ( u1 = u & u1 | X is bounded ) by A1;

dom (v1 + u1) = X /\ X by FUNCT_2:def 1;

then A4: ( v1 + u1 is Function of X,COMPLEX & (v1 + u1) | X is bounded ) by A2, A3, CFUNCT_1:75;

reconsider h = v + u as Element of Funcs (X,COMPLEX) ;

A5: 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 A6: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;

for x being object st x in dom h holds

h . x = (v1 . x) + (u1 . x) by A2, A3, CFUNCDOM:1;

then v + u = v1 + u1 by A6, A5, VALUED_1:def 1;

hence v + u in ComplexBoundedFunctions X by A4; :: thesis: verum

for v being Element of (CAlgebra X) st v in ComplexBoundedFunctions X holds

- v in ComplexBoundedFunctions X

proof

then A14:
ComplexBoundedFunctions X is having-inverse
;
let v be Element of (CAlgebra X); :: thesis: ( v in ComplexBoundedFunctions X implies - v in ComplexBoundedFunctions X )

assume A8: v in ComplexBoundedFunctions X ; :: thesis: - v in ComplexBoundedFunctions X

consider v1 being Function of X,COMPLEX such that

A9: ( v1 = v & v1 | X is bounded ) by A8;

A10: ( - v1 is Function of X,COMPLEX & (- v1) | X is bounded ) by A9, CFUNCT_1:74;

reconsider h = - v, v2 = v as Element of Funcs (X,COMPLEX) ;

A11: h = (- 1r) * v by CLVECT_1:3;

A12: ex f being Function st

( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;

A13: dom v1 = X by FUNCT_2:def 1;

hence - v in ComplexBoundedFunctions X by A10; :: thesis: verum

end;assume A8: v in ComplexBoundedFunctions X ; :: thesis: - v in ComplexBoundedFunctions X

consider v1 being Function of X,COMPLEX such that

A9: ( v1 = v & v1 | X is bounded ) by A8;

A10: ( - v1 is Function of X,COMPLEX & (- v1) | X is bounded ) by A9, CFUNCT_1:74;

reconsider h = - v, v2 = v as Element of Funcs (X,COMPLEX) ;

A11: h = (- 1r) * v by CLVECT_1:3;

A12: ex f being Function st

( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;

A13: dom v1 = X by FUNCT_2:def 1;

now :: thesis: for x being object st x in dom h holds

h . x = - (v1 . x)

then
- v = - v1
by A13, A12, VALUED_1:9;h . x = - (v1 . x)

let x be object ; :: 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 A11, CFUNCDOM:4;

hence h . x = - (v1 . x) by A9; :: thesis: verum

end;assume x in dom h ; :: thesis: h . x = - (v1 . x)

then reconsider y = x as Element of X ;

h . x = (- 1r) * (v2 . y) by A11, CFUNCDOM:4;

hence h . x = - (v1 . x) by A9; :: thesis: verum

hence - v in ComplexBoundedFunctions X by A10; :: thesis: verum

for a being Complex

for u being Element of (CAlgebra X) st u in ComplexBoundedFunctions X holds

a * u in ComplexBoundedFunctions X

proof

hence
ComplexBoundedFunctions X is Cadditively-linearly-closed
by A7, A14; :: thesis: ComplexBoundedFunctions X is multiplicatively-closed
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 A15: u in ComplexBoundedFunctions X ; :: thesis: a * u in ComplexBoundedFunctions X

consider u1 being Function of X,COMPLEX such that

A16: ( u1 = u & u1 | X is bounded ) by A15;

A17: ( a (#) u1 is Function of X,COMPLEX & (a (#) u1) | X is bounded ) by A16, CFUNCT_1:72;

reconsider h = a * u as Element of Funcs (X,COMPLEX) ;

A18: ex f being Function st

( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;

A19: dom u1 = X by FUNCT_2:def 1;

for x being object st x in dom h holds

h . x = a * (u1 . x) by A16, CFUNCDOM:4;

then a * u = a (#) u1 by A19, A18, VALUED_1:def 5;

hence a * u in ComplexBoundedFunctions X by A17; :: thesis: verum

end;a * u in ComplexBoundedFunctions X

let u be Element of (CAlgebra X); :: thesis: ( u in ComplexBoundedFunctions X implies a * u in ComplexBoundedFunctions X )

assume A15: u in ComplexBoundedFunctions X ; :: thesis: a * u in ComplexBoundedFunctions X

consider u1 being Function of X,COMPLEX such that

A16: ( u1 = u & u1 | X is bounded ) by A15;

A17: ( a (#) u1 is Function of X,COMPLEX & (a (#) u1) | X is bounded ) by A16, CFUNCT_1:72;

reconsider h = a * u as Element of Funcs (X,COMPLEX) ;

A18: ex f being Function st

( h = f & dom f = X & rng f c= COMPLEX ) by FUNCT_2:def 2;

A19: dom u1 = X by FUNCT_2:def 1;

for x being object st x in dom h holds

h . x = a * (u1 . x) by A16, CFUNCDOM:4;

then a * u = a (#) u1 by A19, A18, VALUED_1:def 5;

hence a * u in ComplexBoundedFunctions X by A17; :: thesis: verum

A20: for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds

v * u in ComplexBoundedFunctions X

proof

reconsider g = ComplexFuncUnit X as Function of X,COMPLEX ;
let v, u be Element of (CAlgebra X); :: thesis: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v * u in ComplexBoundedFunctions X )

assume A21: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis: v * u in ComplexBoundedFunctions X

consider v1 being Function of X,COMPLEX such that

A22: ( v1 = v & v1 | X is bounded ) by A21;

consider u1 being Function of X,COMPLEX such that

A23: ( u1 = u & u1 | X is bounded ) by A21;

dom (v1 (#) u1) = X /\ X by FUNCT_2:def 1;

then A24: ( v1 (#) u1 is Function of X,COMPLEX & (v1 (#) u1) | X is bounded ) by A22, A23, CFUNCT_1:76;

reconsider h = v * u as Element of Funcs (X,COMPLEX) ;

A25: 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 A26: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;

for x being object st x in dom h holds

h . x = (v1 . x) * (u1 . x) by A22, A23, CFUNCDOM:2;

then v * u = v1 (#) u1 by A26, A25, VALUED_1:def 4;

hence v * u in ComplexBoundedFunctions X by A24; :: thesis: verum

end;assume A21: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis: v * u in ComplexBoundedFunctions X

consider v1 being Function of X,COMPLEX such that

A22: ( v1 = v & v1 | X is bounded ) by A21;

consider u1 being Function of X,COMPLEX such that

A23: ( u1 = u & u1 | X is bounded ) by A21;

dom (v1 (#) u1) = X /\ X by FUNCT_2:def 1;

then A24: ( v1 (#) u1 is Function of X,COMPLEX & (v1 (#) u1) | X is bounded ) by A22, A23, CFUNCT_1:76;

reconsider h = v * u as Element of Funcs (X,COMPLEX) ;

A25: 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 A26: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;

for x being object st x in dom h holds

h . x = (v1 . x) * (u1 . x) by A22, A23, CFUNCDOM:2;

then v * u = v1 (#) u1 by A26, A25, VALUED_1:def 4;

hence v * u in ComplexBoundedFunctions X by A24; :: thesis: verum

g | X is bounded ;

then 1. (CAlgebra X) in ComplexBoundedFunctions X ;

hence ComplexBoundedFunctions X is multiplicatively-closed by A20; :: thesis: verum