let E1, E2 be strict AltCatStr ; :: thesis: ( the carrier of E1 is empty & the carrier of E2 is empty implies E1 = E2 )

set C1 = the carrier of E1;

set C2 = the carrier of E2;

assume that

A1: the carrier of E1 is empty and

A2: the carrier of E2 is empty ; :: thesis: E1 = E2

A3: [: the carrier of E2, the carrier of E2, the carrier of E2:] = {} by A2, MCART_1:31;

[: the carrier of E1, the carrier of E1, the carrier of E1:] = {} by A1, MCART_1:31;

then A4: the Comp of E1 = {}

.= the Comp of E2 by A3 ;

A5: [: the carrier of E2, the carrier of E2:] = {} by A2, ZFMISC_1:90;

[: the carrier of E1, the carrier of E1:] = {} by A1, ZFMISC_1:90;

then the Arrows of E1 = {}

.= the Arrows of E2 by A5 ;

hence E1 = E2 by A1, A2, A4; :: thesis: verum

set C1 = the carrier of E1;

set C2 = the carrier of E2;

assume that

A1: the carrier of E1 is empty and

A2: the carrier of E2 is empty ; :: thesis: E1 = E2

A3: [: the carrier of E2, the carrier of E2, the carrier of E2:] = {} by A2, MCART_1:31;

[: the carrier of E1, the carrier of E1, the carrier of E1:] = {} by A1, MCART_1:31;

then A4: the Comp of E1 = {}

.= the Comp of E2 by A3 ;

A5: [: the carrier of E2, the carrier of E2:] = {} by A2, ZFMISC_1:90;

[: the carrier of E1, the carrier of E1:] = {} by A1, ZFMISC_1:90;

then the Arrows of E1 = {}

.= the Arrows of E2 by A5 ;

hence E1 = E2 by A1, A2, A4; :: thesis: verum