let X be non empty set ; :: thesis: for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions X,Y is RealNormSpace-like
let Y be RealNormSpace; :: thesis: 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 RealNormSpace-like by NORMSP_1:def 2; :: thesis: verum