:: deftheorem defines * LOPBAN_2:def 3 :
for X being RealNormSpace
for f being Element of BoundedLinearOperators (X,X)
for a being Real holds a * f = (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f);