let X be non empty set ; :: thesis:
set W = BoundedFunctions X;
set V = RAlgebra X;
A1: for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v * u in BoundedFunctions X

let v, u be Element of (RAlgebra X); :: thesis:
assume that
A2: v in BoundedFunctions X and
A3: u in BoundedFunctions X ; :: thesis:
consider u1 being Function of X,REAL such that
A4: u1 = u and
A5: u1 | X is bounded by A3;
reconsider h = v * u as Element of Funcs (X,REAL) ;
consider v1 being Function of X,REAL such that
A6: v1 = v and
A7: v1 | X is bounded by A2;
dom (v1 (#) u1) = X /\ X by FUNCT_2:def 1;
then A8: (v1 (#) u1) | X is bounded by A7, A5, RFUNCT_1:84;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def 1;
then A9: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & (dom v1) /\ (dom u1) = X /\ X ) by FUNCT_2:def 1, FUNCT_2:def 2;
for x being object st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A6, A4, FUNCSDOM:2;
then v * u = v1 (#) u1 by A9, VALUED_1:def 4;
hence v * u in BoundedFunctions X by A8; :: thesis:

end;

reconsider g = RealFuncUnit X as Function of X,REAL ;
for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v + u in BoundedFunctions X

let v, u be Element of (RAlgebra X); :: thesis:
assume that
A10: v in BoundedFunctions X and
A11: u in BoundedFunctions X ; :: thesis:
consider u1 being Function of X,REAL such that
A12: u1 = u and
A13: u1 | X is bounded by A11;
reconsider h = v + u as Element of Funcs (X,REAL) ;
consider v1 being Function of X,REAL such that
A14: v1 = v and
A15: v1 | X is bounded by A10;
dom (v1 + u1) = X /\ X by FUNCT_2:def 1;
then A16: (v1 + u1) | X is bounded by A15, A13, RFUNCT_1:83;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def 1;
then A17: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & (dom v1) /\ (dom u1) = X /\ X ) by FUNCT_2:def 1, FUNCT_2:def 2;
for x being object st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A14, A12, FUNCSDOM:1;
then v + u = v1 + u1 by A17, VALUED_1:def 1;
hence v + u in BoundedFunctions X by A16; :: thesis:

end;

then A18: BoundedFunctions X is add-closed by IDEAL_1:def 1;
A19: RAlgebra X is RealLinearSpace by Th7;
for v being Element of (RAlgebra X) st v in BoundedFunctions X holds
- v in BoundedFunctions X

let v be Element of (RAlgebra X); :: thesis:
assume v in BoundedFunctions X ; :: thesis:
then consider v1 being Function of X,REAL such that
A20: v1 = v and
A21: v1 | X is bounded ;
A22: (- v1) | X is bounded by A21, RFUNCT_1:82;
reconsider h = - v, v2 = v as Element of Funcs (X,REAL) ;
A23: h = (- 1) * v by A19, RLVECT_1:16;

A24: now :: thesis:

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

end;

( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & dom v1 = X ) by FUNCT_2:def 1, FUNCT_2:def 2;
then - v = - v1 by A24, VALUED_1:9;
hence - v in BoundedFunctions X by A22; :: thesis:

end;

then A25: BoundedFunctions X is having-inverse ;
for a being Real
for u being Element of (RAlgebra X) st u in BoundedFunctions X holds
a * u in BoundedFunctions X

let a be Real; :: thesis:
let u be Element of (RAlgebra X); :: thesis:
assume u in BoundedFunctions X ; :: thesis:
then consider u1 being Function of X,REAL such that
A26: u1 = u and
A27: u1 | X is bounded ;
A28: (a (#) u1) | X is bounded by A27, RFUNCT_1:80;
reconsider h = a * u as Element of Funcs (X,REAL) ;
A29: ( ex f being Function st
( h = f & dom f = X & rng f c= REAL ) & dom u1 = X ) by FUNCT_2:def 1, FUNCT_2:def 2;
for x being object st x in dom h holds
h . x = a * (u1 . x) by A26, FUNCSDOM:4;
then a * u = a (#) u1 by A29, VALUED_1:def 5;
hence a * u in BoundedFunctions X by A28; :: thesis:

end;

hence BoundedFunctions X is additively-linearly-closed by A18, A25; :: thesis:
g | X is bounded ;
then 1. (RAlgebra X) in BoundedFunctions X ;
hence BoundedFunctions X is multiplicatively-closed by A1; :: thesis: