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' & the carrier' of S c= the carrier' of S' & the Arity of S' | the carrier' of S = the Arity of S & the ResultSort of S' | the carrier' of S = the ResultSort of S ) by A1, Def1;
A4: ( the carrier of S' c= the carrier of S & the carrier' of S' c= the carrier' of S & the Arity of S | the carrier' of S' = the Arity of S' & the ResultSort of S | the carrier' of S' = the ResultSort of S' ) by A2, Def1;
A5: dom the Arity of S' = the carrier' of S' by FUNCT_2:def 1;
A6: dom the ResultSort of S' = the carrier' of S' by FUNCT_2:def 1;
A7: the carrier' of S = the carrier' of S' by A3, A4, XBOOLE_0:def 10;
A8: the Arity of S = the Arity of S' by A3, A4, A5, RELAT_1:97;
the ResultSort of S = the ResultSort of S' by A3, A4, A6, RELAT_1:97;
hence S = S' by A3, A4, A7, A8, XBOOLE_0:def 10; :: thesis: verum