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