thus JumpPart (f :=<0,...,0> a) is empty by RECDEF_2:def 2; :: according to COMPOS_0:def 8 :: thesis: verum