reconsider A = a as Data-Location by Th25;
reconsider L = la as Element of NAT ;
reconsider i = A =0_goto L as Instruction of SCM+FSA by Th38;
take i ; :: thesis: ex A being Data-Location ex La being Element of NAT st
( a = A & la = La & i = A =0_goto La )
take A ; :: thesis: ex La being Element of NAT st
( a = A & la = La & i = A =0_goto La )
take L ; :: thesis: ( a = A & la = L & i = A =0_goto L )
thus ( a = A & la = L & i = A =0_goto L ) ; :: thesis: verum