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 A1: ( the carrier of E1 is empty & the carrier of E2 is empty ) ; :: thesis: E1 = E2
then A2: [:the carrier of E2,the carrier of E2:] = {} by ZFMISC_1:113;
[:the carrier of E1,the carrier of E1:] = {} by A1, ZFMISC_1:113;
then A3: the Arrows of E1 = {} by PBOOLE:134
.= the Arrows of E2 by A2, PBOOLE:134 ;
A4: [:the carrier of E2,the carrier of E2,the carrier of E2:] = {} by A1, MCART_1:35;
[:the carrier of E1,the carrier of E1,the carrier of E1:] = {} by A1, MCART_1:35;
then the Comp of E1 = {} by PBOOLE:134
.= the Comp of E2 by A4, PBOOLE:134 ;
hence E1 = E2 by A1, A3; :: thesis: verum