thus ( not SCM is empty & SCM is stored-program ) by AMI_1:def 3, STRUCT_0:def 1; :: thesis: SCM is standard-ins
consider X being non empty set such that
WW: proj2 SCM-Instr c= X * by FINSEQ_1:106;
take X ; :: according to AMI_1:def 32 :: thesis: the Instructions of SCM c= [:K98(),(X * ):]
S: SCM-Instr c= [:NAT ,(proj2 SCM-Instr ):] by AMI_2:34;
[:NAT ,(proj2 SCM-Instr ):] c= [:NAT ,(X * ):] by WW, ZFMISC_1:118;
then SCM-Instr c= [:NAT ,(X * ):] by S, XBOOLE_1:1;
hence the Instructions of SCM c= [:NAT ,(X * ):] ; :: thesis: verum