:: deftheorem defines MultBy SCMRING2:def 6 :
for R being Ring
for a, b being Data-Location of R holds MultBy (a,b) = [4,{},<*a,b*>];