let N be non empty with_non-empty_elements set ; :: thesis: for I being Instruction of (STC N) holds JumpPart I = 0
let I be Instruction of (STC N); :: thesis: JumpPart I = 0
the Instructions of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
then ( I = [0,0,0] or I = [1,0,0] ) by TARSKI:def 2;
hence JumpPart I = 0 by RECDEF_2:def 2; :: thesis: verum