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