let S, S9 be non empty strict ManySortedSign ; :: thesis: ( S <= S9 & S9 <= S implies S = S9 )
assume that
A1: S <= S9 and
A2: S9 <= S ; :: thesis: S = S9
A3: the carrier' of S9 c= the carrier' of S by A2;
A4: dom the ResultSort of S9 = the carrier' of S9 by FUNCT_2:def 1;
the ResultSort of S9 | the carrier' of S = the ResultSort of S by A1;
then A5: the ResultSort of S = the ResultSort of S9 by A3, A4, RELAT_1:68;
A6: dom the Arity of S9 = the carrier' of S9 by FUNCT_2:def 1;
the Arity of S9 | the carrier' of S = the Arity of S by A1;
then A7: the Arity of S = the Arity of S9 by A3, A6, RELAT_1:68;
the carrier' of S c= the carrier' of S9 by A1;
then A8: the carrier' of S = the carrier' of S9 by A3, XBOOLE_0:def 10;
( the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier of S ) by A1, A2;
hence S = S9 by A8, A7, A5, XBOOLE_0:def 10; :: thesis: verum