let I be Instruction of (STC N); :: thesis: I is ins-loc-free
I in the InstructionsF of (STC N) ;
then I in {[0,0,0],[1,0,0]} by Def7;
then ( I = [0,0,0] or I = [1,0,0] ) by TARSKI:def 2;
hence JumpPart I is empty ; :: according to COMPOS_0:def 8 :: thesis: verum