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;
reconsider A = the Arity of C1, B = the Arity of C2 as Function of {} ,{{} } by A2, A3, FUNCT_7:19;
A4: ( the carrier of C2 = {} & the carrier' of C2 = {} ) by A2;
A5: RT in {(id {} )} by ALTCAT_1:3, FUNCT_2:12;
RS in {(id {} )} by ALTCAT_1:3, FUNCT_2:12;
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