:: deftheorem Def9 defines MultBy SCMFSA_2:def 11 :
for a, b being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = MultBy (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b₃ = MultBy (A,B) ) );