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