let x be Element of {[0,{},{}],[1,{},{}]}; :: thesis: JumpPart x = {}
( x = [0,{},{}] or x = [1,{},{}] ) by TARSKI:def 2;
hence JumpPart x = {} by RECDEF_2:def 2; :: thesis: verum