:: deftheorem defines * CLOPBAN2:def 3 :
for X being ComplexNormSpace
for f being Element of BoundedLinearOperators (X,X)
for z being Complex holds z * f = (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f);