f :=<0,...,0> a = [12,{} ,<*a,f*>] by SCMFSA_2:def 22;
hence JumpPart (f :=<0,...,0> a) is empty by RECDEF_2:def 2; :: according to AMISTD_2:def 13 :: thesis: verum