thus
not the carrier of (STC N) is empty
; STRUCT_0:def 1 STC N is standard-ins
A1:
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 4 the Instructions of (STC N) c= [:NAT,(NAT *),(X *):]
A2:
0 in X *
by FINSEQ_1:49;
0 in NAT *
by FINSEQ_1:49;
then
( [0,0,0] in [:NAT,(NAT *),(X *):] & [1,0,0] in [:NAT,(NAT *),(X *):] )
by A2, MCART_1:69;
hence
the Instructions of (STC N) c= [:NAT,(NAT *),(X *):]
by A1, ZFMISC_1:32; verum