la in NAT by AMI_1:def 4;
then reconsider L = la as Instruction-Location of SCM by AMI_1:def 4;
reconsider i = goto L as Instruction of SCM+FSA by Th38;
take i ; :: thesis: ex La being Instruction-Location of SCM st
( la = La & i = goto La )
take L ; :: thesis: ( la = L & i = goto L )
thus ( la = L & i = goto L ) ; :: thesis: verum