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