let S, S9 be non empty strict ManySortedSign ; ( S <= S9 & S9 <= S implies S = S9 )
assume that
A1:
S <= S9
and
A2:
S9 <= S
; 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; verum