let S be non empty standard-ins homogeneous set ; :: thesis: for I being Element of S st JumpPart I = {} holds
JumpParts (InsCode I) = {0}
let I be Element of S; :: thesis: ( JumpPart I = {} implies JumpParts (InsCode I) = {0} )
assume A1: JumpPart I = {} ; :: thesis: JumpParts (InsCode I) = {0}
set T = InsCode I;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {0} c= JumpParts (InsCode I)

let a be object ; :: thesis: ( a in JumpParts (InsCode I) implies a in {0} )
assume a in JumpParts (InsCode I) ; :: thesis: a in {0}
then consider II being Element of S such that
A2: a = JumpPart II and
A3: InsCode II = InsCode I ;
dom (JumpPart II) = dom (JumpPart I) by A3, Def5;
then a = 0 by A1, A2;
hence a in {0} by TARSKI:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {0} or a in JumpParts (InsCode I) )
assume a in {0} ; :: thesis: a in JumpParts (InsCode I)
then a = 0 by TARSKI:def 1;
hence a in JumpParts (InsCode I) by A1; :: thesis: verum