thus InsCode (a >0_goto i1) is jump-only ; :: according to AMISTD_1:def 4 :: thesis: ( not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )
JUMP (a >0_goto i1) <> {} ;
hence not a >0_goto i1 is sequential by AMISTD_1:43; :: thesis: not a >0_goto i1 is ins-loc-free
take 1 ; :: according to AMISTD_2:def 12 :: thesis: ( 1 in dom (AddressPart (a >0_goto i1)) & (product" (AddressParts (InsCode (a >0_goto i1)))) . 1 = K53() )
dom (AddressPart (a >0_goto i1)) = dom <*i1,a*> by Th25
.= {1,2} by FINSEQ_1:4, FINSEQ_3:29 ;
hence 1 in dom (AddressPart (a >0_goto i1)) by TARSKI:def 2; :: thesis: (product" (AddressParts (InsCode (a >0_goto i1)))) . 1 = K53()
thus (product" (AddressParts (InsCode (a >0_goto i1)))) . 1 = K53() by Th56; :: thesis: verum