let R be good Ring; :: thesis: JumpPart (halt (SCM R)) = {}
thus JumpPart (halt (SCM R)) = [0 ,{} ,{} ] `2_3 by SCMRING2:30
.= {} by RECDEF_2:def 2 ; :: thesis: verum