let X be RealUnitarySpace; :: thesis:
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:
assume A2: ( v in BoundedLinearFunctionals X & u in BoundedLinearFunctionals X ) ; :: thesis:
reconsider f = v + u as linear-Functional of X by DUALSP01:def 6;
f is Lipschitzian
proof
reconsider v1 = v, u1 = u as Lipschitzian linear-Functional of X by ;
consider K2 being Real such that
A4: 0 < K2 and
A5: for x being Point of X holds |.(v1 . x).| <= K2 * by BHSP_6:def 4;
consider K1 being Real such that
A6: 0 < K1 and
A7: for x being Point of X holds |.(u1 . x).| <= K1 * by BHSP_6:def 4;
reconsider K3 = K1 + K2 as Real ;
now :: thesis: for x being VECTOR of X holds |.(f . x).| <= K3 *
let x be VECTOR of X; :: thesis: |.(f . x).| <= K3 *
A8: |.((u1 . x) + (v1 . x)).| <= |.(u1 . x).| + |.(v1 . x).| by COMPLEX1:56;
A9: |.(v1 . x).| <= K2 * by A5;
|.(u1 . x).| <= K1 * by A7;
then A10: |.(u1 . x).| + |.(v1 . x).| <= (K1 * ) + (K2 * ) by ;
|.(f . x).| = |.((u1 . x) + (v1 . x)).| by DUALSP01:12;
hence |.(f . x).| <= K3 * by ; :: thesis: verum
end;
hence f is Lipschitzian by ; :: thesis: verum
end;
hence v + u in BoundedLinearFunctionals X by Def10; :: 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:
reconsider f = a * v as linear-Functional of X by DUALSP01:def 6;
f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian linear-Functional of X by ;
consider K being Real such that
A12: 0 < K and
A13: for x being Point of X holds |.(v1 . x).| <= K * by BHSP_6:def 4;
B12: 0 <= |.a.| by COMPLEX1:46;
|.a.| + 0 < |.a.| + 1 by XREAL_1:8;
then B2: |.a.| * K <= (|.a.| + 1) * K by ;
now :: thesis: for x being VECTOR of X holds |.(f . x).| <= ((|.a.| + 1) * K) *
let x be VECTOR of X; :: thesis: |.(f . x).| <= ((|.a.| + 1) * K) *
0 <= |.a.| by COMPLEX1:46;
then A15: |.a.| * |.(v1 . x).| <= |.a.| * (K * ) by ;
|.(a * (v1 . x)).| = |.a.| * |.(v1 . x).| by COMPLEX1:65;
then A16: |.(f . x).| <= |.a.| * (K * ) by ;
0 <= by BHSP_1:28;
then (|.a.| * K) * <= ((|.a.| + 1) * K) * by ;
hence |.(f . x).| <= ((|.a.| + 1) * K) * by ; :: thesis: verum
end;
hence f is Lipschitzian by ; :: thesis: verum
end;
hence a * v in BoundedLinearFunctionals X by Def10; :: thesis: verum
end;
hence BoundedLinearFunctionals X is linearly-closed by A1; :: thesis: verum