{} in ((union {}) \/ the Instructions of Trivial-COM) * by FINSEQ_1:49;
then A1: {{}} c= ((union {}) \/ the Instructions of Trivial-COM) * by ZFMISC_1:31;
take X = (union {}) \/ the Instructions of Trivial-COM; :: according to COMPOS_1:def 4 :: thesis: the Instructions of Trivial-COM c= [:NAT,(NAT *),(X *):]
{} in NAT * by FINSEQ_1:49;
then A2: {{}} c= NAT * by ZFMISC_1:31;
the Instructions of Trivial-COM = {[0,{},{}]} by Def1
.= [:{0},{{}},{{}}:] by MCART_1:35 ;
hence the Instructions of Trivial-COM c= [:NAT,(NAT *),(X *):] by A1, A2, MCART_1:73; :: thesis: verum