take
{{}}
; :: according to COMPOS_0:def 1 :: thesis: {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):]

A3: {{}} c= {{}} * by FINSEQ_1:49, ZFMISC_1:31;

A4: {{}} c= NAT * by FINSEQ_1:49, ZFMISC_1:31;

{[1,{},{}]} = [:{1},{{}},{{}}:] by MCART_1:35;

hence {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A3, A4, MCART_1:73; :: thesis: verum

A3: {{}} c= {{}} * by FINSEQ_1:49, ZFMISC_1:31;

A4: {{}} c= NAT * by FINSEQ_1:49, ZFMISC_1:31;

{[1,{},{}]} = [:{1},{{}},{{}}:] by MCART_1:35;

hence {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A3, A4, MCART_1:73; :: thesis: verum