thus JumpPart (b := (f,a)) is empty by RECDEF_2:def 2; :: according to COMPOS_1:def 16 :: thesis: verum