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