let X be non empty set ; :: thesis: ( BoundedFunctions X is additively-linearly-closed & BoundedFunctions X is multiplicatively-closed )
set W = BoundedFunctions X;
set V = RAlgebra X;
P0: RAlgebra X is RealLinearSpace by LmAlgebra2;
for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v + u in BoundedFunctions X

proof

let v, u be Element of (RAlgebra X); :: thesis: ( v in BoundedFunctions X & u in BoundedFunctions X implies v + u in BoundedFunctions X )
assume XS1: ( v in BoundedFunctions X & u in BoundedFunctions X ) ; :: thesis: v + u in BoundedFunctions X
consider v1 being Function of X,REAL such that
L010: ( v1 = v & v1 | X is bounded ) by XS1;
consider u1 being Function of X,REAL such that
L020: ( u1 = u & u1 | X is bounded ) by XS1;
dom (v1 + u1) = X /\ X by FUNCT_2:def 1;
then L04: ( v1 + u1 is Function of X,REAL & (v1 + u1) | X is bounded ) by L010, L020, RFUNCT_1:100;
reconsider h = v + u as Element of Funcs X,REAL ;
XSF: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def 1;
then R3: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by L010, L020, FUNCSDOM:10;
then v + u = v1 + u1 by R3, XSF, VALUED_1:def 1;
hence v + u in BoundedFunctions X by L04; :: thesis: verum

end;

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

proof

let v be Element of (RAlgebra X); :: thesis: ( v in BoundedFunctions X implies - v in BoundedFunctions X )
assume XS1: v in BoundedFunctions X ; :: thesis: - v in BoundedFunctions X
consider v1 being Function of X,REAL such that
L010: ( v1 = v & v1 | X is bounded ) by XS1;
M1: ( - v1 is Function of X,REAL & (- v1) | X is bounded ) by L010, RFUNCT_1:99;
reconsider h = - v, v2 = v as Element of Funcs X,REAL ;
R1: h = (- 1) * v by P0, RLVECT_1:29;
XSF: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
R3: dom v1 = 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 X ;
h . x = (- 1) * (v2 . y) by R1, FUNCSDOM:15;
hence h . x = - (v1 . x) by L010; :: thesis: verum

end;

then - v = - v1 by R3, XSF, VALUED_1:9;
hence - v in BoundedFunctions X by M1; :: thesis: verum

end;

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

proof

let a be Real; :: thesis: for u being Element of (RAlgebra X) st u in BoundedFunctions X holds
a * u in BoundedFunctions X
let u be Element of (RAlgebra X); :: thesis: ( u in BoundedFunctions X implies a * u in BoundedFunctions X )
assume XS1: u in BoundedFunctions X ; :: thesis: a * u in BoundedFunctions X
consider u1 being Function of X,REAL such that
L110: ( u1 = u & u1 | X is bounded ) by XS1;
M2: ( a (#) u1 is Function of X,REAL & (a (#) u1) | X is bounded ) by L110, RFUNCT_1:97;
reconsider h = a * u as Element of Funcs X,REAL ;
XSF: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
R3: dom u1 = X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = a * (u1 . x) by L110, FUNCSDOM:15;
then a * u = a (#) u1 by R3, XSF, VALUED_1:def 5;
hence a * u in BoundedFunctions X by M2; :: thesis: verum

end;

hence BoundedFunctions X is additively-linearly-closed by P1, Q1, def210; :: thesis: BoundedFunctions X is multiplicatively-closed
Q2: for v, u being Element of (RAlgebra X) st v in BoundedFunctions X & u in BoundedFunctions X holds
v * u in BoundedFunctions X

proof

let v, u be Element of (RAlgebra X); :: thesis: ( v in BoundedFunctions X & u in BoundedFunctions X implies v * u in BoundedFunctions X )
assume XS1: ( v in BoundedFunctions X & u in BoundedFunctions X ) ; :: thesis: v * u in BoundedFunctions X
consider v1 being Function of X,REAL such that
L010: ( v1 = v & v1 | X is bounded ) by XS1;
consider u1 being Function of X,REAL such that
L020: ( u1 = u & u1 | X is bounded ) by XS1;
dom (v1 (#) u1) = X /\ X by FUNCT_2:def 1;
then M3: ( v1 (#) u1 is Function of X,REAL & (v1 (#) u1) | X is bounded ) by L010, L020, RFUNCT_1:101;
reconsider h = v * u as Element of Funcs X,REAL ;
XSF: ex f being Function st
( h = f & dom f = X & rng f c= REAL ) by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = X /\ (dom u1) by FUNCT_2:def 1;
then R3: (dom v1) /\ (dom u1) = X /\ X by FUNCT_2:def 1;
for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by L010, L020, FUNCSDOM:11;
then v * u = v1 (#) u1 by R3, XSF, VALUED_1:def 4;
hence v * u in BoundedFunctions X by M3; :: thesis: verum

end;

reconsider g = RealFuncUnit X as Function of X,REAL ;
g | X is bounded ;
then 1. (RAlgebra X) in BoundedFunctions X ;
hence BoundedFunctions X is multiplicatively-closed by Rdef200, Q2; :: thesis: verum