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

( 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