let k be Element of NAT ; :: thesis: for a, b being Data-Location holds IncAddr (a := b),k = a := b
let a, b be Data-Location ; :: thesis: IncAddr (a := b),k = a := b
InsCode (a := b) = 1 by MCART_1:7;
hence IncAddr (a := b),k = a := b by Def3; :: thesis: verum