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 AMI_1:def 3 :: thesis: STC N is standard-ins
0 in ((union N) \/ the carrier of (STC N)) * by FINSEQ_1:66;
then A1: {0 } c= ((union N) \/ the carrier of (STC N)) * by ZFMISC_1:37;
A2: the Instructions of (STC N) = {[0 ,0 ],[1,0 ]} by Def11
.= [:{0 ,1},{0 }:] by ZFMISC_1:36 ;
take X = (union N) \/ the carrier of (STC N); :: according to AMI_1:def 32 :: thesis: the Instructions of (STC N) c= [:NAT ,(X * ):]
thus the Instructions of (STC N) c= [:NAT ,(X * ):] by A1, A2, ZFMISC_1:119; :: thesis: verum