let X, Y be RealNormSpace; :: thesis: BoundedLinearOperators X,Y is linearly-closed
set W = BoundedLinearOperators X,Y;
A1: for v, u being VECTOR of (R_VectorSpace_of_LinearOperators X,Y) st v in BoundedLinearOperators X,Y & u in BoundedLinearOperators X,Y holds
v + u in BoundedLinearOperators X,Y

proof

let v, u be VECTOR of (R_VectorSpace_of_LinearOperators X,Y); :: thesis: ( v in BoundedLinearOperators X,Y & u in BoundedLinearOperators X,Y implies v + u in BoundedLinearOperators X,Y )
assume A2: ( v in BoundedLinearOperators X,Y & u in BoundedLinearOperators X,Y ) ; :: thesis: v + u in BoundedLinearOperators X,Y
reconsider f = v + u as LinearOperator of X,Y by Def7;
f is bounded

proof

reconsider u1 = u as bounded LinearOperator of X,Y by A2, Def10;
reconsider v1 = v as bounded LinearOperator of X,Y by A2, Def10;
consider K1 being Real such that
A3: ( 0 <= K1 & ( for x being VECTOR of X holds ||.(u1 . x).|| <= K1 * ||.x.|| ) ) by Def9;
consider K2 being Real such that
A4: ( 0 <= K2 & ( for x being VECTOR of X holds ||.(v1 . x).|| <= K2 * ||.x.|| ) ) by Def9;
take K3 = K1 + K2; :: according to LOPBAN_1:def 9 :: thesis: ( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ||.x.|| ) )
A5: 0 + 0 <= K1 + K2 by A3, A4;

now

let x be VECTOR of X; :: thesis: ||.(f . x).|| <= K3 * ||.x.||
A6: ||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th20;
A7: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by NORMSP_1:def 2;
A8: ||.(u1 . x).|| <= K1 * ||.x.|| by A3;
||.(v1 . x).|| <= K2 * ||.x.|| by A4;
then ||.(u1 . x).|| + ||.(v1 . x).|| <= (K1 * ||.x.||) + (K2 * ||.x.||) by A8, XREAL_1:9;
hence ||.(f . x).|| <= K3 * ||.x.|| by A6, A7, XXREAL_0:2; :: thesis: verum

end;

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

end;

hence v + u in BoundedLinearOperators X,Y by Def10; :: thesis: verum

end;

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

proof

let a be Real; :: thesis: for v being VECTOR of (R_VectorSpace_of_LinearOperators X,Y) st v in BoundedLinearOperators X,Y holds
a * v in BoundedLinearOperators X,Y
let v be VECTOR of (R_VectorSpace_of_LinearOperators X,Y); :: thesis: ( v in BoundedLinearOperators X,Y implies a * v in BoundedLinearOperators X,Y )
assume A9: v in BoundedLinearOperators X,Y ; :: thesis: a * v in BoundedLinearOperators X,Y
reconsider f = a * v as LinearOperator of X,Y by Def7;
f is bounded

proof

reconsider v1 = v as bounded LinearOperator of X,Y by A9, Def10;
consider K being Real such that
A10: ( 0 <= K & ( for x being VECTOR of X holds ||.(v1 . x).|| <= K * ||.x.|| ) ) by Def9;
take K1 = (abs a) * K; :: according to LOPBAN_1:def 9 :: thesis: ( 0 <= K1 & ( for x being VECTOR of X holds ||.(f . x).|| <= K1 * ||.x.|| ) )
A11: ( 0 <= K & 0 <= abs a ) by A10, COMPLEX1:132;

now

let x be VECTOR of X; :: thesis: ||.(f . x).|| <= ((abs a) * K) * ||.x.||
A12: ||.(a * (v1 . x)).|| = (abs a) * ||.(v1 . x).|| by NORMSP_1:def 2;
0 <= abs a by COMPLEX1:132;
then (abs a) * ||.(v1 . x).|| <= (abs a) * (K * ||.x.||) by A10, XREAL_1:66;
hence ||.(f . x).|| <= ((abs a) * K) * ||.x.|| by A12, Th21; :: thesis: verum

end;

hence ( 0 <= K1 & ( for x being VECTOR of X holds ||.(f . x).|| <= K1 * ||.x.|| ) ) by A11; :: thesis: verum

end;

hence a * v in BoundedLinearOperators X,Y by Def10; :: thesis: verum

end;

hence BoundedLinearOperators X,Y is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum