:: deftheorem defines MultF_Real* DUALSP01:def 1 :
for X being RealLinearSpace holds MultF_Real* X = the Mult of X;