set W = ContinuousFunctions X;
set V = RAlgebra the carrier of X;
A1: RAlgebra the carrier of X is RealLinearSpace by C0SP1:7;
for v, u being Element of (RAlgebra the carrier of X) st v in ContinuousFunctions X & u in ContinuousFunctions X holds
v + u in ContinuousFunctions X

proof

let v, u be Element of (RAlgebra the carrier of X); :: thesis: ( v in ContinuousFunctions X & u in ContinuousFunctions X implies v + u in ContinuousFunctions X )
assume XS1: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; :: thesis: v + u in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A2: v1 = v by XS1;
consider u1 being continuous RealMap of X such that
A3: u1 = u by XS1;
reconsider h = v + u as Element of Funcs ( the carrier of X,REAL) ;
XSF: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= REAL ) 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 set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A2, A3, FUNCSDOM:10;
then v + u = v1 + u1 by A5, XSF, VALUED_1:def 1;
hence v + u in ContinuousFunctions X ; :: thesis: verum

end;

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

proof

let v be Element of (RAlgebra the carrier of X); :: thesis: ( v in ContinuousFunctions X implies - v in ContinuousFunctions X )
assume XS2: v in ContinuousFunctions X ; :: thesis: - v in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A7: v1 = v by XS2;
reconsider h = - v, v2 = v as Element of Funcs ( the carrier of X,REAL) ;
A9: h = (- 1) * v by A1, RLVECT_1:29;
XSF1: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= REAL ) by FUNCT_2:def 2;
A10: dom v1 = the carrier of 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 the carrier of X ;
h . x = (- 1) * (v2 . y) by A9, FUNCSDOM:15;
hence h . x = - (v1 . x) by A7; :: thesis: verum

end;

then - v = - v1 by A10, XSF1, VALUED_1:9;
hence - v in ContinuousFunctions X ; :: thesis: verum

end;

then A11: ContinuousFunctions X is having-inverse by C0SP1:def 1;
for a being Real
for u being Element of (RAlgebra the carrier of X) st u in ContinuousFunctions X holds
a * u in ContinuousFunctions X

proof

let a be Real; :: thesis: for u being Element of (RAlgebra the carrier of X) st u in ContinuousFunctions X holds
a * u in ContinuousFunctions X
let u be Element of (RAlgebra the carrier of X); :: thesis: ( u in ContinuousFunctions X implies a * u in ContinuousFunctions X )
assume XS3: u in ContinuousFunctions X ; :: thesis: a * u in ContinuousFunctions X
consider u1 being continuous RealMap of X such that
A12: u1 = u by XS3;
reconsider h = a * u as Element of Funcs ( the carrier of X,REAL) ;
XSF2: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= REAL ) by FUNCT_2:def 2;
A14: dom u1 = the carrier of X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = a * (u1 . x) by A12, FUNCSDOM:15;
then a * u = a (#) u1 by A14, XSF2, VALUED_1:def 5;
hence a * u in ContinuousFunctions X ; :: thesis: verum

end;

hence ContinuousFunctions X is additively-linearly-closed by A6, A11, C0SP1:def 10; :: thesis: ContinuousFunctions X is multiplicatively-closed
A15: for v, u being Element of (RAlgebra the carrier of X) st v in ContinuousFunctions X & u in ContinuousFunctions X holds
v * u in ContinuousFunctions X

proof

let v, u be Element of (RAlgebra the carrier of X); :: thesis: ( v in ContinuousFunctions X & u in ContinuousFunctions X implies v * u in ContinuousFunctions X )
assume XS4: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; :: thesis: v * u in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A16: v1 = v by XS4;
consider u1 being continuous RealMap of X such that
A17: u1 = u by XS4;
reconsider h = v * u as Element of Funcs ( the carrier of X,REAL) ;
XSF3: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= REAL ) by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def 1;
then A19: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A16, A17, FUNCSDOM:11;
then v * u = v1 (#) u1 by A19, XSF3, VALUED_1:def 4;
hence v * u in ContinuousFunctions X ; :: thesis: verum

end;

reconsider g = RealFuncUnit the carrier of X as RealMap of X ;
g = X --> 1 ;
then 1. (RAlgebra the carrier of X) in ContinuousFunctions X ;
hence ContinuousFunctions X is multiplicatively-closed by A15, C0SP1:def 4; :: thesis: verum