for X, Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||