let N be non empty with_non-empty_elements set ; :: thesis: for i being Element of the Instructions of (STC N) holds
( InsCode i = 1 or InsCode i = 0 )
let i be Element of the Instructions of (STC N); :: thesis: ( InsCode i = 1 or InsCode i = 0 )
the Instructions of (STC N) = {[1,0,0],[0,0,0]} by Def11;
then ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def 2;
hence ( InsCode i = 1 or InsCode i = 0 ) by RECDEF_2:def 1; :: thesis: verum