let a, b be Int-Location; :: thesis: InsCode (MultBy (a,b)) = 4
ex A, B being Data-Location st
( a = A & b = B & MultBy (a,b) = MultBy (A,B) ) by Def9;
hence InsCode (MultBy (a,b)) = 4 ; :: thesis: verum