let N be with_zero set ; :: thesis: for i being Element of the InstructionsF of (STC N) holds JUMP i is empty
let i be Element of the InstructionsF of (STC N); :: thesis: JUMP i is empty

per cases ( InsCode i = 1 or InsCode i = 0 ) by Th6;

suppose A1: InsCode i = 1 ; :: thesis: JUMP i is empty

reconsider l1 = 0 , l2 = 1 as Nat ;
set X = { (NIC (i,l)) where l is Nat : verum } ;
assume not JUMP i is empty ; :: thesis: contradiction
then consider x being object such that
A2: x in meet { (NIC (i,l)) where l is Nat : verum } ;
NIC (i,l1) in { (NIC (i,l)) where l is Nat : verum } ;
then {(0 + 1)} in { (NIC (i,l)) where l is Nat : verum } by A1, Lm4;
then x in {1} by A2, SETFAM_1:def 1;
then A3: x = 1 by TARSKI:def 1;
NIC (i,l2) in { (NIC (i,l)) where l is Nat : verum } ;
then {(1 + 1)} in { (NIC (i,l)) where l is Nat : verum } by A1, Lm4;
then x in {2} by A2, SETFAM_1:def 1;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

suppose A4: InsCode i = 0 ; :: thesis: JUMP i is empty

reconsider i = i as Instruction of (STC N) ;
for l being Nat holds NIC (i,l) = {l} by A4, Th2, Th4;
hence JUMP i is empty by Th1; :: thesis: verum

end;

end;