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;

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

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 ; :: according to TARSKI:def 3 :: thesis: ( not a in {0} or a in 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;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

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