:: deftheorem defines * CLOPBAN2:def 2 :
for X being ComplexNormSpace
for f, g being Element of BoundedLinearOperators (X,X) holds g * f = (modetrans (g,X,X)) * (modetrans (f,X,X));