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