:: deftheorem Def4 defines modetrans NDIFF_6:def 4 :
for S, T being RealNormSpace
for f being set st f is PartFunc of S,T holds
modetrans (f,S,T) = f;