for R being Ring
for I being Instruction of (SCM R) st InsCode I = 4 holds
ex a, b being Data-Location of R st I = MultBy (a,b)