let il be Instruction-Location of SCM+FSA ; :: thesis: goto il = [6,<*il*>]
ex L being Instruction-Location of SCM st
( L = il & goto il = goto L ) by SCMFSA_2:def 16;
hence goto il = [6,<*il*>] ; :: thesis: verum