:: deftheorem Def7 defines modetrans RSSPACE4:def 7 :
for X being non empty set
for Y being RealNormSpace
for f being object st f in BoundedFunctions (X,Y) holds
modetrans (f,X,Y) = f;