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 A2: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; :: thesis: v + u in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A3: v1 = v by A2;
consider u1 being continuous RealMap of X such that
A4: u1 = u by A2;
reconsider h = v + u as Element of Funcs ( the carrier of X,REAL) ;
A5: 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 A6: (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 A3, A4, FUNCSDOM:10;
then v + u = v1 + u1 by A6, A5, VALUED_1:def 1;
hence v + u in ContinuousFunctions X ; :: thesis: verum

end;

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

end;

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

end;

then A13: 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 A14: u in ContinuousFunctions X ; :: thesis: a * u in ContinuousFunctions X
consider u1 being continuous RealMap of X such that
A15: u1 = u by A14;
reconsider h = a * u as Element of Funcs ( the carrier of X,REAL) ;
A16: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= REAL ) by FUNCT_2:def 2;
A17: 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 A15, FUNCSDOM:15;
then a * u = a (#) u1 by A17, A16, VALUED_1:def 5;
hence a * u in ContinuousFunctions X ; :: thesis: verum

end;

hence ContinuousFunctions X is additively-linearly-closed by A7, A13, C0SP1:def 10; :: thesis: ContinuousFunctions X is multiplicatively-closed
A18: 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 A19: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; :: thesis: v * u in ContinuousFunctions X
consider v1 being continuous RealMap of X such that
A20: v1 = v by A19;
consider u1 being continuous RealMap of X such that
A21: u1 = u by A19;
reconsider h = v * u as Element of Funcs ( the carrier of X,REAL) ;
A22: 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 A23: (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 A20, A21, FUNCSDOM:11;
then v * u = v1 (#) u1 by A23, A22, 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 A18, C0SP1:def 4; :: thesis: verum