:: deftheorem Def1 defines modetrans NDIFF_6:def 1 :
for S being set st S is RealNormSpace holds
modetrans S = S;