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

proof

let v, u be Element of (CAlgebra the carrier of X); :: thesis: ( v in CContinuousFunctions X & u in CContinuousFunctions X implies v + u in CContinuousFunctions X )
assume A1: ( v in CContinuousFunctions X & u in CContinuousFunctions X ) ; :: thesis: v + u in CContinuousFunctions X
consider v1 being continuous Function of the carrier of X,COMPLEX such that
A2: v1 = v by A1;
consider u1 being continuous Function of the carrier of X,COMPLEX such that
A3: u1 = u by A1;
reconsider h = v + u as Element of Funcs ( the carrier of X,COMPLEX) ;
A4: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def 1;
then A5: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of 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 A6: v + u = v1 + u1 by A5, A4, VALUED_1:def 1;
v1 + u1 is continuous Function of the carrier of X,COMPLEX by Th4;
hence v + u in CContinuousFunctions X by A6; :: thesis: verum

end;

then A7: CContinuousFunctions X is add-closed by IDEAL_1:def 1;
for v being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X holds
- v in CContinuousFunctions X

proof

let v be Element of (CAlgebra the carrier of X); :: thesis: ( v in CContinuousFunctions X implies - v in CContinuousFunctions X )
assume A8: v in CContinuousFunctions X ; :: thesis: - v in CContinuousFunctions X
consider v1 being continuous Function of the carrier of X,COMPLEX such that
A9: v1 = v by A8;
reconsider h = - v, v2 = v as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider e = - 1r as Complex ;
A10: h = e * v by CLVECT_1:3;
A11: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def 2;
A12: dom v1 = the carrier of 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 the carrier of X ;
reconsider mj = - 1 as Element of COMPLEX by XCMPLX_0:def 2;
h . x = mj * (v2 . y) by A10, CFUNCDOM:4;
hence h . x = - (v1 . x) by A9; :: thesis: verum

end;

then A13: - v = - v1 by A12, A11, VALUED_1:9;
e (#) v1 is continuous Function of the carrier of X,COMPLEX by Th5;
hence - v in CContinuousFunctions X by A13; :: thesis: verum

end;

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

proof

let a be Complex; :: thesis: for u being Element of (CAlgebra the carrier of X) st u in CContinuousFunctions X holds
a * u in CContinuousFunctions X
let u be Element of (CAlgebra the carrier of X); :: thesis: ( u in CContinuousFunctions X implies a * u in CContinuousFunctions X )
assume A15: u in CContinuousFunctions X ; :: thesis: a * u in CContinuousFunctions X
consider u1 being continuous Function of the carrier of X,COMPLEX such that
A16: u1 = u by A15;
reconsider h = a * u as Element of Funcs ( the carrier of X,COMPLEX) ;
A17: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def 2;
A18: dom u1 = the carrier of 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 A19: a * u = a (#) u1 by A18, A17, VALUED_1:def 5;
a (#) u1 is continuous Function of the carrier of X,COMPLEX by Th5;
hence a * u in CContinuousFunctions X by A19; :: thesis: verum

end;

hence CContinuousFunctions X is Cadditively-linearly-closed by A7, A14; :: thesis: CContinuousFunctions X is multiplicatively-closed
A20: for v, u being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X & u in CContinuousFunctions X holds
v * u in CContinuousFunctions X

proof

let v, u be Element of (CAlgebra the carrier of X); :: thesis: ( v in CContinuousFunctions X & u in CContinuousFunctions X implies v * u in CContinuousFunctions X )
assume A21: ( v in CContinuousFunctions X & u in CContinuousFunctions X ) ; :: thesis: v * u in CContinuousFunctions X
consider v1 being continuous Function of the carrier of X,COMPLEX such that
A22: v1 = v by A21;
consider u1 being continuous Function of the carrier of X,COMPLEX such that
A23: u1 = u by A21;
reconsider h = v * u as Element of Funcs ( the carrier of X,COMPLEX) ;
A24: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def 1;
then A25: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of 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 A26: v * u = v1 (#) u1 by A25, A24, VALUED_1:def 4;
v1 (#) u1 is continuous Function of the carrier of X,COMPLEX by Th7;
hence v * u in CContinuousFunctions X by A26; :: thesis: verum

end;

reconsider g = ComplexFuncUnit the carrier of X as Function of the carrier of X,COMPLEX ;
g = X --> 1r ;
then 1. (CAlgebra the carrier of X) in CContinuousFunctions X ;
hence CContinuousFunctions X is multiplicatively-closed by A20, C0SP1:def 4; :: thesis: verum