:: deftheorem defines * NDIFF_2:def 2 :
for X, Y, Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds g * f = (modetrans (g,Y,Z)) * (modetrans (f,X,Y));