let lb be Instruction-Location of SCM+FSA ; :: thesis: InsCode (goto lb) = 6
ex La being Instruction-Location of SCM st
( lb = La & goto lb = goto La ) by Def16;
hence InsCode (goto lb) = 6 by MCART_1:7; :: thesis: verum