dom (JumpPart (a =0_goto i1)) = dom <*i1*> by RECDEF_2:def 2
.= {1} by FINSEQ_1:4, FINSEQ_1:55 ;
hence not JumpPart (a =0_goto i1) is empty ; :: according to COMPOS_1:def 37 :: thesis: verum