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