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