:: deftheorem defines + CLOPBAN2:def 1 :
for X being ComplexNormSpace
for f, g being Element of BoundedLinearOperators (X,X) holds f + g = (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (f,g);