dom (JumpPart (goto i1,R)) = dom <*i1*> by RECDEF_2:def 2
.= {1} by FINSEQ_1:4, FINSEQ_1:def 8 ;
then 1 in dom (JumpPart (goto i1,R)) by TARSKI:def 1;
hence not JumpPart (goto i1,R) is empty ; :: according to AMISTD_2:def 13 :: thesis: verum