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 A3: ( v in BoundedFunctions X,Y & 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:121;
f is bounded

proof

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

now

let x be Element of X; :: thesis: ||.(f . x).|| <= K3
A7: ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| by LOPBAN_1:14;
A8: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by NORMSP_1:def 2;
A9: ||.(u1 . x).|| <= K1 by A4;
||.(v1 . x).|| <= K2 by A5;
then ||.(u1 . x).|| + ||.(v1 . x).|| <= K1 + K2 by A9, XREAL_1:9;
hence ||.(f . x).|| <= K3 by A7, A8, XXREAL_0:2; :: thesis: verum

end;

hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A6; :: 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:121;
f is bounded

proof

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

now

let x be Element of X; :: thesis: ||.(f . x).|| <= (abs a) * K
A13: ||.(f . x).|| = ||.(a * (v1 . x)).|| by LOPBAN_1:15;
A14: ||.(a * (v1 . x)).|| = (abs a) * ||.(v1 . x).|| by NORMSP_1:def 2;
0 <= abs a by COMPLEX1:132;
hence ||.(f . x).|| <= (abs a) * K by A11, A13, A14, XREAL_1:66; :: thesis: verum

end;

hence ( 0 <= K1 & ( for x being Element of X holds ||.(f . x).|| <= K1 ) ) by A12; :: 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