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

let v, u be Element of (RAlgebra the carrier of X); :: thesis:
assume A2: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; :: thesis:
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;
A5: ( v1 + u1 is Function of the carrier of X,REAL & v1 + u1 is continuous ) by NAGATA_1:22;
reconsider h = v + u as Element of Funcs ( the carrier of X,REAL) ;
A6: 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 A7: (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 A3, A4, FUNCSDOM:1;
then v + u = v1 + u1 by A7, A6, VALUED_1:def 1;
hence v + u in ContinuousFunctions X by A5; :: thesis:

end;

then A8: 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

let v be Element of (RAlgebra the carrier of X); :: thesis:
assume A9: v in ContinuousFunctions X ; :: thesis:
consider v1 being continuous RealMap of X such that
A10: v1 = v by A9;
A11: - v1 is continuous RealMap of X by PSCOMP_1:9;
reconsider h = - v, v2 = v as Element of Funcs ( the carrier of X,REAL) ;
A12: h = (- 1) * v by A1, RLVECT_1:16;
A13: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= REAL ) by FUNCT_2:def 2;
A14: dom v1 = the carrier of X by FUNCT_2:def 1;

let x be object ; :: thesis:
assume x in dom h ; :: thesis:
then reconsider y = x as Element of the carrier of X ;
h . x = (- 1) * (v2 . y) by A12, FUNCSDOM:4;
hence h . x = - (v1 . x) by A10; :: thesis:

end;

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

end;

then A15: ContinuousFunctions X is having-inverse ;
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

let a be Real; :: thesis:
let u be Element of (RAlgebra the carrier of X); :: thesis:
assume A16: u in ContinuousFunctions X ; :: thesis:
consider u1 being continuous RealMap of X such that
A17: u1 = u by A16;
A18: a (#) u1 is continuous RealMap of X

reconsider U = u1 as continuous Function of X,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of X;
consider H being Function of X,R^1 such that
A19: for p being Point of X
for r1 being Real st U . p = r1 holds
H . p = a * r1 and
A20: H is continuous by JGRAPH_2:23;
reconsider h = H as RealMap of X by TOPMETR:17;
A21: dom h = the carrier of X by FUNCT_2:def 1
.= dom u1 by FUNCT_2:def 1 ;
for c being object st c in dom h holds
h . c = a * (u1 . c) by A19;
then h = a (#) u1 by A21, VALUED_1:def 5;
hence a (#) u1 is continuous RealMap of X by A20, JORDAN5A:27; :: thesis:

end;

reconsider h = a * 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;
A23: 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 A17, FUNCSDOM:4;
then a * u = a (#) u1 by A23, A22, VALUED_1:def 5;
hence a * u in ContinuousFunctions X by A18; :: thesis:

end;

hence ContinuousFunctions X is additively-linearly-closed by A8, A15; :: thesis:
A24: 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

let v, u be Element of (RAlgebra the carrier of X); :: thesis:
assume A25: ( v in ContinuousFunctions X & u in ContinuousFunctions X ) ; :: thesis:
consider v1 being continuous RealMap of X such that
A26: v1 = v by A25;
consider u1 being continuous RealMap of X such that
A27: u1 = u by A25;
A28: v1 (#) u1 is continuous RealMap of X

reconsider V = v1, U = u1 as continuous Function of X,R^1 by JORDAN5A:27, TOPMETR:17;
consider H being Function of X,R^1 such that
A29: for p being Point of X
for r1, r2 being Real st V . p = r1 & U . p = r2 holds
H . p = r1 * r2 and
A30: H is continuous by JGRAPH_2:25;
reconsider h = H as RealMap of X by TOPMETR:17;
A31: dom h = the carrier of X /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X /\ (dom u1) by FUNCT_2:def 1
.= (dom v1) /\ (dom u1) by FUNCT_2:def 1 ;
for c being object st c in dom h holds
h . c = (v1 . c) * (u1 . c) by A29;
then h = v1 (#) u1 by A31, VALUED_1:def 4;
hence v1 (#) u1 is continuous RealMap of X by A30, JORDAN5A:27; :: thesis:

end;

reconsider h = v * u as Element of Funcs ( the carrier of X,REAL) ;
A32: 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 A33: (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 A26, A27, FUNCSDOM:2;
then v * u = v1 (#) u1 by A33, A32, VALUED_1:def 4;
hence v * u in ContinuousFunctions X by A28; :: thesis:

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 A24; :: thesis: