set W = BoundedBilinearOperators (X,Y,Z);

A1: for v, u being VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st v in BoundedBilinearOperators (X,Y,Z) & u in BoundedBilinearOperators (X,Y,Z) holds

v + u in BoundedBilinearOperators (X,Y,Z)

for v being VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st v in BoundedBilinearOperators (X,Y,Z) holds

a * v in BoundedBilinearOperators (X,Y,Z)

A1: for v, u being VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st v in BoundedBilinearOperators (X,Y,Z) & u in BoundedBilinearOperators (X,Y,Z) holds

v + u in BoundedBilinearOperators (X,Y,Z)

proof

for a being Real
let v, u be VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)); :: thesis: ( v in BoundedBilinearOperators (X,Y,Z) & u in BoundedBilinearOperators (X,Y,Z) implies v + u in BoundedBilinearOperators (X,Y,Z) )

assume that

A2: v in BoundedBilinearOperators (X,Y,Z) and

A3: u in BoundedBilinearOperators (X,Y,Z) ; :: thesis: v + u in BoundedBilinearOperators (X,Y,Z)

reconsider f = v + u as BilinearOperator of X,Y,Z by EQSET;

f is Lipschitzian

end;assume that

A2: v in BoundedBilinearOperators (X,Y,Z) and

A3: u in BoundedBilinearOperators (X,Y,Z) ; :: thesis: v + u in BoundedBilinearOperators (X,Y,Z)

reconsider f = v + u as BilinearOperator of X,Y,Z by EQSET;

f is Lipschitzian

proof

hence
v + u in BoundedBilinearOperators (X,Y,Z)
by Def9; :: thesis: verum
reconsider v1 = v as Lipschitzian BilinearOperator of X,Y,Z by A2, Def9;

consider K2 being Real such that

A4: 0 <= K2 and

A5: for x being VECTOR of X

for y being VECTOR of Y holds ||.(v1 . (x,y)).|| <= (K2 * ||.x.||) * ||.y.|| by Def8;

reconsider u1 = u as Lipschitzian BilinearOperator of X,Y,Z by A3, Def9;

consider K1 being Real such that

A6: 0 <= K1 and

A7: for x being VECTOR of X

for y being VECTOR of Y holds ||.(u1 . (x,y)).|| <= (K1 * ||.x.||) * ||.y.|| by Def8;

take K3 = K1 + K2; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= K3 & ( for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.|| ) )

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.|| ) ) by A4, A6; :: thesis: verum

end;consider K2 being Real such that

A4: 0 <= K2 and

A5: for x being VECTOR of X

for y being VECTOR of Y holds ||.(v1 . (x,y)).|| <= (K2 * ||.x.||) * ||.y.|| by Def8;

reconsider u1 = u as Lipschitzian BilinearOperator of X,Y,Z by A3, Def9;

consider K1 being Real such that

A6: 0 <= K1 and

A7: for x being VECTOR of X

for y being VECTOR of Y holds ||.(u1 . (x,y)).|| <= (K1 * ||.x.||) * ||.y.|| by Def8;

take K3 = K1 + K2; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= K3 & ( for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.|| ) )

now :: thesis: for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.||

hence
( 0 <= K3 & ( for x being VECTOR of Xfor y being VECTOR of Y holds ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.||

let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.||

let y be VECTOR of Y; :: thesis: ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.||

A8: ||.((u1 . (x,y)) + (v1 . (x,y))).|| <= ||.(u1 . (x,y)).|| + ||.(v1 . (x,y)).|| by NORMSP_1:def 1;

A9: ||.(v1 . (x,y)).|| <= (K2 * ||.x.||) * ||.y.|| by A5;

||.(u1 . (x,y)).|| <= (K1 * ||.x.||) * ||.y.|| by A7;

then A10: ||.(u1 . (x,y)).|| + ||.(v1 . (x,y)).|| <= ((K1 * ||.x.||) * ||.y.||) + ((K2 * ||.x.||) * ||.y.||) by A9, XREAL_1:7;

||.(f . (x,y)).|| = ||.((u1 . (x,y)) + (v1 . (x,y))).|| by Th16;

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

end;let y be VECTOR of Y; :: thesis: ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.||

A8: ||.((u1 . (x,y)) + (v1 . (x,y))).|| <= ||.(u1 . (x,y)).|| + ||.(v1 . (x,y)).|| by NORMSP_1:def 1;

A9: ||.(v1 . (x,y)).|| <= (K2 * ||.x.||) * ||.y.|| by A5;

||.(u1 . (x,y)).|| <= (K1 * ||.x.||) * ||.y.|| by A7;

then A10: ||.(u1 . (x,y)).|| + ||.(v1 . (x,y)).|| <= ((K1 * ||.x.||) * ||.y.||) + ((K2 * ||.x.||) * ||.y.||) by A9, XREAL_1:7;

||.(f . (x,y)).|| = ||.((u1 . (x,y)) + (v1 . (x,y))).|| by Th16;

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

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= (K3 * ||.x.||) * ||.y.|| ) ) by A4, A6; :: thesis: verum

for v being VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st v in BoundedBilinearOperators (X,Y,Z) holds

a * v in BoundedBilinearOperators (X,Y,Z)

proof

hence
BoundedBilinearOperators (X,Y,Z) is linearly-closed
by A1, RLSUB_1:def 1; :: thesis: verum
let a be Real; :: thesis: for v being VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st v in BoundedBilinearOperators (X,Y,Z) holds

a * v in BoundedBilinearOperators (X,Y,Z)

let v be VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)); :: thesis: ( v in BoundedBilinearOperators (X,Y,Z) implies a * v in BoundedBilinearOperators (X,Y,Z) )

assume A11: v in BoundedBilinearOperators (X,Y,Z) ; :: thesis: a * v in BoundedBilinearOperators (X,Y,Z)

reconsider f = a * v as BilinearOperator of X,Y,Z by EQSET;

f is Lipschitzian

end;a * v in BoundedBilinearOperators (X,Y,Z)

let v be VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)); :: thesis: ( v in BoundedBilinearOperators (X,Y,Z) implies a * v in BoundedBilinearOperators (X,Y,Z) )

assume A11: v in BoundedBilinearOperators (X,Y,Z) ; :: thesis: a * v in BoundedBilinearOperators (X,Y,Z)

reconsider f = a * v as BilinearOperator of X,Y,Z by EQSET;

f is Lipschitzian

proof

hence
a * v in BoundedBilinearOperators (X,Y,Z)
by Def9; :: thesis: verum
reconsider v1 = v as Lipschitzian BilinearOperator of X,Y,Z by A11, Def9;

consider K being Real such that

A12: 0 <= K and

A13: for x being VECTOR of X

for y being VECTOR of Y holds ||.(v1 . (x,y)).|| <= (K * ||.x.||) * ||.y.|| by Def8;

take |.a.| * K ; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= |.a.| * K & ( for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.|| ) )

hence ( 0 <= |.a.| * K & ( for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.|| ) ) by A12, A14; :: thesis: verum

end;consider K being Real such that

A12: 0 <= K and

A13: for x being VECTOR of X

for y being VECTOR of Y holds ||.(v1 . (x,y)).|| <= (K * ||.x.||) * ||.y.|| by Def8;

take |.a.| * K ; :: according to LOPBAN_9:def 3 :: thesis: ( 0 <= |.a.| * K & ( for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.|| ) )

A14: now :: thesis: for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.||

0 <= |.a.|
by COMPLEX1:46;for y being VECTOR of Y holds ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.||

let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.||

let y be VECTOR of Y; :: thesis: ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.||

0 <= |.a.| by COMPLEX1:46;

then A15: |.a.| * ||.(v1 . (x,y)).|| <= |.a.| * ((K * ||.x.||) * ||.y.||) by A13, XREAL_1:64;

||.(a * (v1 . (x,y))).|| = |.a.| * ||.(v1 . (x,y)).|| by NORMSP_1:def 1;

hence ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.|| by A15, Th17; :: thesis: verum

end;let y be VECTOR of Y; :: thesis: ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.||

0 <= |.a.| by COMPLEX1:46;

then A15: |.a.| * ||.(v1 . (x,y)).|| <= |.a.| * ((K * ||.x.||) * ||.y.||) by A13, XREAL_1:64;

||.(a * (v1 . (x,y))).|| = |.a.| * ||.(v1 . (x,y)).|| by NORMSP_1:def 1;

hence ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.|| by A15, Th17; :: thesis: verum

hence ( 0 <= |.a.| * K & ( for x being VECTOR of X

for y being VECTOR of Y holds ||.(f . (x,y)).|| <= ((|.a.| * K) * ||.x.||) * ||.y.|| ) ) by A12, A14; :: thesis: verum