let lb be Instruction-Location of SCM+FSA ; :: 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
consider A being Data-Location , La being Instruction-Location of SCM such that
( a = A & lb = La ) and
A1: a =0_goto lb = A =0_goto La by Def17;
thus InsCode (a =0_goto lb) = 7 by A1, MCART_1:7; :: thesis: verum