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 )
( dom the Arity of S = the carrier' of S & 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 RELAT_1:97; :: thesis: verum