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