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