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 )
thus ( 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 ) ; :: thesis: verum