let C1, C2 be strict ManySortedSign ; :: thesis: ( C1 is empty & C1 is void & C2 is empty & C2 is void implies C1 = C2 )
assume that
A1: ( C1 is empty & C1 is void ) and
A2: ( C2 is empty & C2 is void ) ; :: thesis: C1 = C2
C1 = C2

proof

A3: ( the carrier of C1 = {} & the carrier' of C1 = {} ) by A1;
then reconsider RS = the ResultSort of C1, RT = the ResultSort of C2 as Function of {},{} by A2;
A4: ( the carrier of C2 = {} & the carrier' of C2 = {} ) by A2;
A5: RT in {(id {})} by ALTCAT_1:2, FUNCT_2:9;
RS in {(id {})} by ALTCAT_1:2, FUNCT_2:9;
then the ResultSort of C1 = id {}
.= the ResultSort of C2 by A5 ;
hence C1 = C2 by A3, A4; :: thesis: verum

end;

hence C1 = C2 ; :: thesis: verum