{} in ((union N) \/ the carrier of (Trivial-AMI N)) * by FINSEQ_1:66;
then A1: {{} } c= ((union N) \/ the carrier of (Trivial-AMI N)) * by ZFMISC_1:37;
take X = (union N) \/ the carrier of (Trivial-AMI N); :: according to COMPOS_1:def 17 :: thesis: the Instructions of (Trivial-AMI N) c= [:NAT ,(NAT * ),(X * ):]
{} in NAT * by FINSEQ_1:66;
then X: {{} } c= NAT * by ZFMISC_1:37;
the Instructions of (Trivial-AMI N) = {[0 ,{} ,{} ]} by Def2
.= [:{0 },{{} },{{} }:] by MCART_1:39 ;
hence the Instructions of (Trivial-AMI N) c= [:NAT ,(NAT * ),(X * ):] by A1, X, MCART_1:77; :: thesis: verum