let X be RealUnitarySpace; :: 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

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

a * v in BoundedLinearFunctionals X

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

for a being Real
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 DUALSP01:def 6;

f is Lipschitzian

end;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 DUALSP01:def 6;

f is Lipschitzian

proof

hence
v + u in BoundedLinearFunctionals X
by Def10; :: thesis: verum
reconsider v1 = v, u1 = u as Lipschitzian linear-Functional of X by A2, Def10;

consider K2 being Real such that

A4: 0 < K2 and

A5: for x being Point of X holds |.(v1 . x).| <= K2 * ||.x.|| 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 * ||.x.|| by BHSP_6:def 4;

reconsider K3 = K1 + K2 as Real ;

end;consider K2 being Real such that

A4: 0 < K2 and

A5: for x being Point of X holds |.(v1 . x).| <= K2 * ||.x.|| 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 * ||.x.|| by BHSP_6:def 4;

reconsider K3 = K1 + K2 as Real ;

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

hence
f is Lipschitzian
by A4, A6, BHSP_6:def 4; :: thesis: verumlet 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 DUALSP01:12;

hence |.(f . x).| <= K3 * ||.x.|| by A8, A10, XXREAL_0:2; :: thesis: verum

end;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 DUALSP01:12;

hence |.(f . x).| <= K3 * ||.x.|| by A8, A10, XXREAL_0:2; :: thesis: verum

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

a * v in BoundedLinearFunctionals X

proof

hence
BoundedLinearFunctionals X is linearly-closed
by A1; :: thesis: verum
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 DUALSP01:def 6;

f is Lipschitzian

end;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 DUALSP01:def 6;

f is Lipschitzian

proof

hence
a * v in BoundedLinearFunctionals X
by Def10; :: thesis: verum
reconsider v1 = v as Lipschitzian linear-Functional of X by A11, Def10;

consider K being Real such that

A12: 0 < K and

A13: for x being Point of X holds |.(v1 . x).| <= K * ||.x.|| 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 A12, XREAL_1:64;

end;consider K being Real such that

A12: 0 < K and

A13: for x being Point of X holds |.(v1 . x).| <= K * ||.x.|| 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 A12, XREAL_1:64;

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

hence
f is Lipschitzian
by B12, A12, BHSP_6:def 4; :: thesis: verumlet x be VECTOR of X; :: thesis: |.(f . x).| <= ((|.a.| + 1) * 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;

then A16: |.(f . x).| <= |.a.| * (K * ||.x.||) by A15, DUALSP01:13;

0 <= ||.x.|| by BHSP_1:28;

then (|.a.| * K) * ||.x.|| <= ((|.a.| + 1) * K) * ||.x.|| by B2, XREAL_1:64;

hence |.(f . x).| <= ((|.a.| + 1) * K) * ||.x.|| by A16, XXREAL_0:2; :: thesis: verum

end;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;

then A16: |.(f . x).| <= |.a.| * (K * ||.x.||) by A15, DUALSP01:13;

0 <= ||.x.|| by BHSP_1:28;

then (|.a.| * K) * ||.x.|| <= ((|.a.| + 1) * K) * ||.x.|| by B2, XREAL_1:64;

hence |.(f . x).| <= ((|.a.| + 1) * K) * ||.x.|| by A16, XXREAL_0:2; :: thesis: verum