let X, Y be ComplexNormSpace; :: thesis: ( C_NormSpace_of_BoundedLinearOperators X,Y is reflexive & C_NormSpace_of_BoundedLinearOperators X,Y is discerning & C_NormSpace_of_BoundedLinearOperators X,Y is ComplexNormSpace-like )
thus C_NormSpace_of_BoundedLinearOperators X,Y is reflexive :: thesis: ( C_NormSpace_of_BoundedLinearOperators X,Y is discerning & C_NormSpace_of_BoundedLinearOperators X,Y is ComplexNormSpace-like )

proof

thus ||.(0. (C_NormSpace_of_BoundedLinearOperators X,Y)).|| = 0 by Th41; :: according to NORMSP_0:def 6 :: thesis: verum

end;

for x, y being Point of (C_NormSpace_of_BoundedLinearOperators X,Y)
for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_NormSpace_of_BoundedLinearOperators X,Y) ) & ( x = 0. (C_NormSpace_of_BoundedLinearOperators X,Y) implies ||.x.|| = 0 ) & ||.(c * x).|| = |.c.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th41;
hence ( C_NormSpace_of_BoundedLinearOperators X,Y is discerning & C_NormSpace_of_BoundedLinearOperators X,Y is ComplexNormSpace-like ) by CLVECT_1:def 14, NORMSP_0:def 5; :: thesis: verum