consider X being non empty set such that
A1: S c= [:NAT,(NAT *),(X *):] by Def1;
x in S ;
then x `1_3 in NAT by A1, RECDEF_2:2;
hence InsCode x is natural ; :: thesis: verum