W: SCM+FSA-Instr c= [:NAT ,(proj2 SCM+FSA-Instr ):] by LmX;
I in SCM+FSA-Instr ;
then I in [:NAT ,(proj2 SCM+FSA-Instr ):] by W;
then I `1 in NAT by MCART_1:10;
hence InsCode I is natural ; :: thesis: verum