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 11;
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