theorem :: RSSPACE4:17

for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||