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