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