thus ( not SCM is empty & SCM is stored-program ) by Lm1, COMPOS_1:def 2, STRUCT_0:def 1; :: thesis: SCM is standard-ins
consider X being non empty set such that
A1: proj2 SCM-Instr c= X * by FINSEQ_1:106;
take X ; :: according to COMPOS_1:def 17 :: thesis: the Instructions of SCM c= [:NAT,(NAT *),(X *):]
A2: SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):] by AMI_2:34;
[:NAT,(NAT *),(proj2 SCM-Instr):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:77;
then SCM-Instr c= [:NAT,(NAT *),(X *):] by A2, XBOOLE_1:1;
hence the Instructions of SCM c= [:NAT,(NAT *),(X *):] ; :: thesis: verum