let X be non empty set ; :: thesis: for Y being RealNormSpace holds
( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
let Y be RealNormSpace; :: thesis: ( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
thus ||.(0. (R_NormSpace_of_BoundedFunctions (X,Y))).|| = 0 by Th24; :: according to NORMSP_0:def 6 :: thesis: ( R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like )
for x, y being Point of (R_NormSpace_of_BoundedFunctions (X,Y))
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) ) & ( x = 0. (R_NormSpace_of_BoundedFunctions (X,Y)) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th24;
hence ( R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like ) by NORMSP_0:def 5, NORMSP_1:def 1; :: thesis: verum