let X be non empty set ; :: thesis: for Y being RealNormSpace holds BoundedFunctions (X,Y) is linearly-closed
let Y be RealNormSpace; :: thesis: BoundedFunctions (X,Y) is linearly-closed
set W = BoundedFunctions (X,Y);
A1: RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) by LOPBAN_1:def 4;
A2: for v, u being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) & u in BoundedFunctions (X,Y) holds
v + u in BoundedFunctions (X,Y)

proof

let v, u be VECTOR of (RealVectSpace (X,Y)); :: thesis: ( v in BoundedFunctions (X,Y) & u in BoundedFunctions (X,Y) implies v + u in BoundedFunctions (X,Y) )
assume that
A3: v in BoundedFunctions (X,Y) and
A4: u in BoundedFunctions (X,Y) ; :: thesis: v + u in BoundedFunctions (X,Y)
reconsider f = v + u as Function of X, the carrier of Y by A1, FUNCT_2:66;
f is bounded

proof

reconsider v1 = v as bounded Function of X, the carrier of Y by A3, Def5;
consider K2 being Real such that
A5: 0 <= K2 and
A6: for x being Element of X holds ||.(v1 . x).|| <= K2 by Def4;
reconsider u1 = u as bounded Function of X, the carrier of Y by A4, Def5;
consider K1 being Real such that
A7: 0 <= K1 and
A8: for x being Element of X holds ||.(u1 . x).|| <= K1 by Def4;
take K3 = K1 + K2; :: according to RSSPACE4:def 4 :: thesis: ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) )

now :: thesis: for x being Element of X holds ||.(f . x).|| <= K3

let x be Element of X; :: thesis: ||.(f . x).|| <= K3
( ||.(u1 . x).|| <= K1 & ||.(v1 . x).|| <= K2 ) by A8, A6;
then A9: ||.(u1 . x).|| + ||.(v1 . x).|| <= K1 + K2 by XREAL_1:7;
( ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| & ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| ) by LOPBAN_1:11, NORMSP_1:def 1;
hence ||.(f . x).|| <= K3 by A9, XXREAL_0:2; :: thesis: verum

end;

hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A7, A5; :: thesis: verum

end;

hence v + u in BoundedFunctions (X,Y) by Def5; :: thesis: verum

end;

for a being Real
for v being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) holds
a * v in BoundedFunctions (X,Y)

proof

let a be Real; :: thesis: for v being VECTOR of (RealVectSpace (X,Y)) st v in BoundedFunctions (X,Y) holds
a * v in BoundedFunctions (X,Y)
let v be VECTOR of (RealVectSpace (X,Y)); :: thesis: ( v in BoundedFunctions (X,Y) implies a * v in BoundedFunctions (X,Y) )
assume A10: v in BoundedFunctions (X,Y) ; :: thesis: a * v in BoundedFunctions (X,Y)
reconsider f = a * v as Function of X, the carrier of Y by A1, FUNCT_2:66;
f is bounded

proof

reconsider v1 = v as bounded Function of X, the carrier of Y by A10, Def5;
reconsider a = a as Real ;
consider K being Real such that
A11: 0 <= K and
A12: for x being Element of X holds ||.(v1 . x).|| <= K by Def4;
reconsider aK = |.a.| * K as Real ;
take aK ; :: according to RSSPACE4:def 4 :: thesis: ( 0 <= aK & ( for x being Element of X holds ||.(f . x).|| <= aK ) )

A13: now :: thesis: for x being Element of X holds ||.(f . x).|| <= |.a.| * K

let x be Element of X; :: thesis: ||.(f . x).|| <= |.a.| * K
A14: 0 <= |.a.| by COMPLEX1:46;
( ||.(f . x).|| = ||.(a * (v1 . x)).|| & ||.(a * (v1 . x)).|| = |.a.| * ||.(v1 . x).|| ) by LOPBAN_1:12, NORMSP_1:def 1;
hence ||.(f . x).|| <= |.a.| * K by A12, A14, XREAL_1:64; :: thesis: verum

end;

0 <= |.a.| by COMPLEX1:46;
hence ( 0 <= aK & ( for x being Element of X holds ||.(f . x).|| <= aK ) ) by A11, A13; :: thesis: verum

end;

hence a * v in BoundedFunctions (X,Y) by Def5; :: thesis: verum

end;

hence BoundedFunctions (X,Y) is linearly-closed by A2, RLSUB_1:def 1; :: thesis: verum