let lb be Element of NAT ; :: thesis: for a being Int-Location holds InsCode (a =0_goto lb) = 7
let a be Int-Location ; :: thesis: InsCode (a =0_goto lb) = 7
ex A being Data-Location ex La being Element of NAT st
( a = A & lb = La & a =0_goto lb = A =0_goto La ) by Def17;
hence InsCode (a =0_goto lb) = 7 by MCART_1:7; :: thesis: verum