:: deftheorem defines MultReal* DUALSP01:def 3 :
for X being ModuleStr over F_Real holds MultReal* X = the lmult of X;