take {{}} ; :: according to COMPOS_0:def 1 :: thesis: {[0,{},{}]} c= [:NAT,(NAT *),({{}} *):]
A1: {{}} c= {{}} * by ZFMISC_1:31, FINSEQ_1:49;
A2: {{}} c= NAT * by ZFMISC_1:31, FINSEQ_1:49;
{[0,{},{}]} = [:{0},{{}},{{}}:] by MCART_1:35;
hence {[0,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73; :: thesis: verum