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