consider X being non empty set such that
W: the Instructions of S c= [:NAT ,(NAT * ),(X * ):] by Def32;
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