theorem :: AMI_3:19

for a, b being Data-Location holds not MultBy (a,b) is halting by Lm7;