:: deftheorem defines * NDIFF_2:def 1 :
for X, Y, Z being RealNormSpace
for f being Element of BoundedLinearOperators (X,Y)
for g being Element of BoundedLinearOperators (Y,Z) holds g * f = (modetrans (g,Y,Z)) * (modetrans (f,X,Y));