let X be non empty set ; for Y being ComplexNormSpace holds
( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
let Y be ComplexNormSpace; ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
thus
||.(0. (C_NormSpace_of_BoundedFunctions (X,Y))).|| = 0
by Th22; NORMSP_0:def 6 ( C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
for x, y being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( x = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.x.|| = 0 ) & ||.(c * x).|| = |.c.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
by Th22;
hence
( C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
by CLVECT_1:def 13; verum