theorem :: SCMFSA_I:6

SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by Lm1;