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

proof

let v, u be VECTOR of (X *'); :: thesis: ( v in BoundedLinearFunctionals X & u in BoundedLinearFunctionals X implies v + u in BoundedLinearFunctionals X )
assume A2: ( v in BoundedLinearFunctionals X & u in BoundedLinearFunctionals X ) ; :: thesis: v + u in BoundedLinearFunctionals X
reconsider f = v + u as linear-Functional of X by Def7;
f is Lipschitzian

proof

reconsider v1 = v, u1 = u as Lipschitzian Functional of X by A2, Def9;
consider K2 being Real such that
A4: 0 <= K2 and
A5: for x being VECTOR of X holds |.(v1 . x).| <= K2 * ||.x.|| by Def8;
consider K1 being Real such that
A6: 0 <= K1 and
A7: for x being VECTOR of X holds |.(u1 . x).| <= K1 * ||.x.|| by Def8;
take K3 = K1 + K2; :: according to DUALSP01:def 9 :: thesis: ( 0 <= K3 & ( for x being VECTOR of X holds |.(f . x).| <= K3 * ||.x.|| ) )

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

let x be VECTOR of X; :: thesis: |.(f . x).| <= K3 * ||.x.||
A8: |.((u1 . x) + (v1 . x)).| <= |.(u1 . x).| + |.(v1 . x).| by COMPLEX1:56;
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:7;
|.(f . x).| = |.((u1 . x) + (v1 . x)).| by Th20b;
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 BoundedLinearFunctionals X by Def9; :: thesis: verum

end;

for a being Real
for v being VECTOR of (X *') st v in BoundedLinearFunctionals X holds
a * v in BoundedLinearFunctionals X

proof

let a be Real; :: thesis: for v being VECTOR of (X *') st v in BoundedLinearFunctionals X holds
a * v in BoundedLinearFunctionals X
let v be VECTOR of (X *'); :: thesis: ( v in BoundedLinearFunctionals X implies a * v in BoundedLinearFunctionals X )
assume A11: v in BoundedLinearFunctionals X ; :: thesis: a * v in BoundedLinearFunctionals X
reconsider f = a * v as linear-Functional of X by Def7;
f is Lipschitzian

proof

reconsider v1 = v as Lipschitzian Functional of X by A11, Def9;
consider K being Real such that
A12: 0 <= K and
A13: for x being VECTOR of X holds |.(v1 . x).| <= K * ||.x.|| by Def8;
take |.a.| * K ; :: according to DUALSP01:def 9 :: thesis: ( 0 <= |.a.| * K & ( for x being VECTOR of X holds |.(f . x).| <= (|.a.| * K) * ||.x.|| ) )

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

let x be VECTOR of X; :: thesis: |.(f . x).| <= (|.a.| * K) * ||.x.||
0 <= |.a.| by COMPLEX1:46;
then A15: |.a.| * |.(v1 . x).| <= |.a.| * (K * ||.x.||) by A13, XREAL_1:64;
|.(a * (v1 . x)).| = |.a.| * |.(v1 . x).| by COMPLEX1:65;
hence |.(f . x).| <= (|.a.| * K) * ||.x.|| by A15, Th21b; :: thesis: verum

end;

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

end;

hence a * v in BoundedLinearFunctionals X by Def9; :: thesis: verum

end;

hence BoundedLinearFunctionals X is linearly-closed by A1; :: thesis: verum