consider X being non empty set such that
W: the Instructions of S c= [:NAT,(NAT *),(X *):] by Def17;
I in the Instructions of S ;
then I in [:NAT,(NAT *),(X *):] by W;
then I = [(I `1_3),(I `2_3),(I `3_3)] by RECDEF_2:3;
then [(I `1_3),(I `2_3)] in proj1 the Instructions of S by RELAT_1:def 4;
then InsCode I in InsCodes S by RELAT_1:def 4;
hence InsCode I is InsType of S ; :: thesis: verum