let X, Y be ComplexNormSpace; :: thesis: BoundedLinearOperators X,Y is linearly-closed
set W = BoundedLinearOperators X,Y;
A1: for v, u being VECTOR of (C_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 (C_VectorSpace_of_LinearOperators X,Y); :: thesis: ( v in BoundedLinearOperators X,Y & u in BoundedLinearOperators X,Y implies v + u in BoundedLinearOperators X,Y )
assume that
A2: v in BoundedLinearOperators X,Y and
A3: u in BoundedLinearOperators X,Y ; :: thesis: v + u in BoundedLinearOperators X,Y
reconsider f = v + u as LinearOperator of X,Y by Def5;
f is bounded

proof

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

now

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

end;

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

end;

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

end;

for c being Complex
for v being VECTOR of (C_VectorSpace_of_LinearOperators X,Y) st v in BoundedLinearOperators X,Y holds
c * v in BoundedLinearOperators X,Y

proof

let c be Complex; :: thesis: for v being VECTOR of (C_VectorSpace_of_LinearOperators X,Y) st v in BoundedLinearOperators X,Y holds
c * v in BoundedLinearOperators X,Y
let v be VECTOR of (C_VectorSpace_of_LinearOperators X,Y); :: thesis: ( v in BoundedLinearOperators X,Y implies c * v in BoundedLinearOperators X,Y )
assume A11: v in BoundedLinearOperators X,Y ; :: thesis: c * v in BoundedLinearOperators X,Y
reconsider f = c * v as LinearOperator of X,Y by Def5;
f is bounded

proof

reconsider v1 = v as bounded LinearOperator of X,Y by A11, Def8;
consider K being Real such that
A12: 0 <= K and
A13: for x being VECTOR of X holds ||.(v1 . x).|| <= K * ||.x.|| by Def7;
take K1 = |.c.| * K; :: according to CLOPBAN1:def 7 :: thesis: ( 0 <= K1 & ( for x being VECTOR of X holds ||.(f . x).|| <= K1 * ||.x.|| ) )

A14: now

let x be VECTOR of X; :: thesis: ||.(f . x).|| <= (|.c.| * K) * ||.x.||
0 <= |.c.| by COMPLEX1:132;
then A15: |.c.| * ||.(v1 . x).|| <= |.c.| * (K * ||.x.||) by A13, XREAL_1:66;
||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| by CLVECT_1:def 14;
hence ||.(f . x).|| <= (|.c.| * K) * ||.x.|| by A15, Th19; :: thesis: verum

end;

0 <= |.c.| by COMPLEX1:132;
hence ( 0 <= K1 & ( for x being VECTOR of X holds ||.(f . x).|| <= K1 * ||.x.|| ) ) by A12, A14; :: thesis: verum

end;

hence c * v in BoundedLinearOperators X,Y by Def8; :: thesis: verum

end;

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