thus
not the carrier of (STC N) is empty
; STRUCT_0:def 1 ( 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; COMPOS_1:def 2 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); COMPOS_1:def 17 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; verum