Divide (a,b) = [5,{},<*a,b*>] by SCMFSA10:13;
hence JumpPart (Divide (a,b)) is empty by RECDEF_2:def 2; :: according to COMPOS_1:def 37 :: thesis: verum