set W = ComplexBoundedFunctions X;
set V = CAlgebra X;
for v, u being Element of () st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v + u in ComplexBoundedFunctions X
proof
let v, u be Element of (); :: thesis:
assume A1: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis:
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 ;
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 ;
then v + u = v1 + u1 by ;
hence v + u in ComplexBoundedFunctions X by A4; :: thesis: verum
end;
then A7: ComplexBoundedFunctions X is add-closed by IDEAL_1:def 1;
for v being Element of () st v in ComplexBoundedFunctions X holds
- v in ComplexBoundedFunctions X
proof
let v be Element of (); :: thesis: ( v in ComplexBoundedFunctions X implies - v in ComplexBoundedFunctions X )
assume A8: v in ComplexBoundedFunctions X ; :: thesis:
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 ;
reconsider h = - v, v2 = v as Element of Funcs (X,COMPLEX) ;
A11: h = () * 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)
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 = () * (v2 . y) by ;
hence h . x = - (v1 . x) by A9; :: thesis: verum
end;
then - v = - v1 by ;
hence - v in ComplexBoundedFunctions X by A10; :: thesis: verum
end;
then A14: ComplexBoundedFunctions X is having-inverse ;
for a being Complex
for u being Element of () st u in ComplexBoundedFunctions X holds
a * u in ComplexBoundedFunctions X
proof
let a be Complex; :: thesis: for u being Element of () st u in ComplexBoundedFunctions X holds
a * u in ComplexBoundedFunctions X

let u be Element of (); :: thesis: ( u in ComplexBoundedFunctions X implies a * u in ComplexBoundedFunctions X )
assume A15: u in ComplexBoundedFunctions X ; :: thesis:
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 ;
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 ;
then a * u = a (#) u1 by ;
hence a * u in ComplexBoundedFunctions X by A17; :: thesis: verum
end;
hence ComplexBoundedFunctions X is Cadditively-linearly-closed by ; :: thesis:
A20: for v, u being Element of () st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v * u in ComplexBoundedFunctions X
proof
let v, u be Element of (); :: thesis:
assume A21: ( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X ) ; :: thesis:
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 ;
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 ;
then v * u = v1 (#) u1 by ;
hence v * u in ComplexBoundedFunctions X by A24; :: thesis: verum
end;
reconsider g = ComplexFuncUnit X as Function of X,COMPLEX ;
g | X is bounded ;
then 1. () in ComplexBoundedFunctions X ;
hence ComplexBoundedFunctions X is multiplicatively-closed by A20; :: thesis: verum