take
{{}}
; :: according to COMPOS_0:def 1 :: thesis: {[0,{},{}],[1,{},{}]} 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;

then A3: {[0,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73;

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

then A4: {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73;

{[0,{},{}]} \/ {[1,{},{}]} = {[0,{},{}],[1,0,0]} by ENUMSET1:1;

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

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;

then A3: {[0,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73;

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

then A4: {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73;

{[0,{},{}]} \/ {[1,{},{}]} = {[0,{},{}],[1,0,0]} by ENUMSET1:1;

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