:: deftheorem defines (.) MATHMORP:def 6 :
for t being Real
for T being non empty RLSStruct
for A being Subset of T holds t (.) A = { (t * a) where a is Point of T : a in A } ;