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