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