let X be ComplexNormSpace; :: thesis:
set C = C_Normed_Algebra_of_BoundedLinearOperators X;
set BS = C_NormSpace_of_BoundedLinearOperators (X,X);
thus C_Normed_Algebra_of_BoundedLinearOperators X is reflexive :: thesis:

proof

thus ||.(0. (C_Normed_Algebra_of_BoundedLinearOperators X)).|| = ||.(0. (C_NormSpace_of_BoundedLinearOperators (X,X))).||
.= 0 ; :: according to NORMSP_0:def 6 :: thesis:

end;

thus C_Normed_Algebra_of_BoundedLinearOperators X is discerning :: thesis:

proof

let x be Point of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to NORMSP_0:def 5 :: thesis:
reconsider y = x as Point of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
assume ||.x.|| = 0 ; :: thesis:
then ||.y.|| = 0 ;
then y = 0. (C_NormSpace_of_BoundedLinearOperators (X,X)) by NORMSP_0:def 5;
hence x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) ; :: thesis:

end;

thus C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like :: thesis:

proof

let x, y be Point of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to CLVECT_1:def 13 :: thesis:
let a be Complex; :: thesis:
reconsider x1 = x, y1 = y as Point of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: ||.x1.|| = ||.x.|| ;
thus ||.(a * x).|| = ||.(a * x1).||
.= |.a.| * ||.x.|| by A1, CLVECT_1:def 13 ; :: thesis:
( ||.(x + y).|| = ||.(x1 + y1).|| & ||.x1.|| + ||.y1.|| = ||.x.|| + ||.y.|| ) ;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by CLVECT_1:def 13; :: thesis:

end;

set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
( ( for x, y, z being Element of (C_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1r * x = x ) ) & ( for a being Complex
for v, w being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) ) by Th19;
hence ( C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) ; :: thesis: