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 by Th36; :: thesis: ( C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like )

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

hence ( C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like ) by CLVECT_1:def 13; :: thesis: verum

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

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

hence ( C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like ) by CLVECT_1:def 13; :: thesis: verum