let k be Element of NAT ; :: thesis: for a, b being Int-Location holds IncAddr (MultBy a,b),k = MultBy a,b
let a, b be Int-Location ; :: thesis: IncAddr (MultBy a,b),k = MultBy a,b
( InsCode (MultBy a,b) = 4 & not 4 in {6,7,8} ) by ENUMSET1:def 1, SCMFSA_2:45;
hence IncAddr (MultBy a,b),k = MultBy a,b by Def3; :: thesis: verum