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