let N be with_zero set ; :: thesis: for i being Element of the InstructionsF of (STC N) holds
( InsCode i = 1 or InsCode i = 0 )
let i be Element of the InstructionsF of (STC N); :: thesis: ( InsCode i = 1 or InsCode i = 0 )
the InstructionsF of (STC N) = {[1,{},{}],[0,{},{}]} by Def7;
then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def 2;
hence ( InsCode i = 1 or InsCode i = 0 ) ; :: thesis: verum