theorem :: CSSPACE4:18

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