thus not the carrier of (SCM R) is empty by Def1; :: according to STRUCT_0:def 1 :: thesis: ( SCM R is standard-ins & SCM R is stored-program )
A1: the Instructions of (SCM R) = SCM-Instr R by Def1;
SCM-Instr R c= [:NAT ,(((union {the carrier of R}) \/ SCM-Memory ) * ):] ;
hence the Instructions of (SCM R) c= [:NAT ,(((union {the carrier of R}) \/ the carrier of (SCM R)) * ):] by A1, Def1; :: according to AMI_1:def 32 :: thesis: SCM R is stored-program
NAT c= the carrier of SCM ;
hence NAT c= the carrier of (SCM R) by Def1; :: according to AMI_1:def 3 :: thesis: verum