thus not the carrier of (STC N) is empty ; :: according to STRUCT_0:def 1 :: thesis: ( STC N is stored-program & STC N is standard-ins )
the carrier of (STC N) = NAT \/ {NAT} by Def11;
hence NAT c= the carrier of (STC N) by XBOOLE_1:7; :: according to COMPOS_1:def 2 :: thesis: STC N is standard-ins
A2: the Instructions of (STC N) = {[0,0,0],[1,0,0]} by Def11;
take X = (union N) \/ the carrier of (STC N); :: according to COMPOS_1:def 17 :: thesis: the Instructions of (STC N) c= [:NAT,(NAT *),(X *):]
Z: 0 in X * by FINSEQ_1:66;
0 in NAT * by FINSEQ_1:66;
then ( [0,0,0] in [:NAT,(NAT *),(X *):] & [1,0,0] in [:NAT,(NAT *),(X *):] ) by Z, MCART_1:73;
hence the Instructions of (STC N) c= [:NAT,(NAT *),(X *):] by A2, ZFMISC_1:38; :: thesis: verum