let ins be Instruction of ; :: thesis: ( InsCode ins = 6 implies ex lb being Instruction-Location of SCM+FSA st ins = goto lb )
assume A1: InsCode ins = 6 ; :: thesis: ex lb being Instruction-Location of SCM+FSA st ins = goto lb
then reconsider I = ins as Instruction of by Th34;
consider La being Instruction-Location of SCM such that
A2: I = goto La by A1, AMI_5:52;
La in NAT by AMI_1:def 4;
then reconsider loc = La as Instruction-Location of SCM+FSA by AMI_1:def 4;
take loc ; :: thesis: ins = goto loc
thus ins = goto loc by A2, Def16; :: thesis: verum