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 Def14;
hence InsCode (MultBy a,b) = 4 by RECDEF_2:def 1; :: thesis: verum