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