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