let S be non empty ManySortedSign ; :: thesis: ( 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 )
A1: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
hence ( 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, RELAT_1:97; :: thesis: verum