thus InsCode (SCM-goto i1) is jump-only ; :: according to AMISTD_1:def 2 :: thesis: ( not SCM-goto i1 is sequential & not SCM-goto i1 is ins-loc-free )
JUMP (SCM-goto i1) <> {} ;
hence not SCM-goto i1 is sequential by AMISTD_1:13; :: thesis: not SCM-goto i1 is ins-loc-free
dom (JumpPart (SCM-goto i1)) = dom <*i1*> by RECDEF_2:def 2
.= {1} by FINSEQ_1:2, FINSEQ_1:def 8 ;
hence not JumpPart (SCM-goto i1) is empty ; :: according to COMPOS_1:def 16 :: thesis: verum