SubFrom (a,b) = [3,{},<*a,b*>] by SCMFSA10:4;
hence JumpPart (SubFrom (a,b)) is empty by RECDEF_2:def 2; :: according to COMPOS_0:def 8 :: thesis: verum