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