thus InsCode (goto i1) is jump-only ; :: according to AMISTD_1:def 4 :: thesis: ( not goto i1 is sequential & not goto i1 is ins-loc-free )
thus not goto i1 is sequential :: thesis: not goto i1 is ins-loc-free

proof

JUMP (goto i1) <> {} ;
hence not goto i1 is sequential by AMISTD_1:43; :: thesis: verum

end;

take 1 ; :: according to AMISTD_2:def 12 :: thesis: ( 1 in dom (AddressPart (goto i1)) & (product" (AddressParts (InsCode (goto i1)))) . 1 = NAT )
dom (AddressPart (goto i1)) = dom <*i1*> by MCART_1:def 2
.= {1} by FINSEQ_1:4, FINSEQ_1:def 8 ;
hence 1 in dom (AddressPart (goto i1)) by TARSKI:def 1; :: thesis: (product" (AddressParts (InsCode (goto i1)))) . 1 = NAT
thus (product" (AddressParts (InsCode (goto i1)))) . 1 = NAT by Th35; :: thesis: verum