:: deftheorem Def11 defines modetrans LOPBAN_9:def 6 :
for X, Y, Z being RealNormSpace
for f being object st f in BoundedBilinearOperators (X,Y,Z) holds
modetrans (f,X,Y,Z) = f;