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