let S be non empty ManySortedSign ; :: thesis: S +* S = ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #)
( the carrier of S = the carrier of S \/ the carrier of S & the carrier' of S = the carrier' of S \/ the carrier' of S & the Arity of S = the Arity of S +* the Arity of S & the ResultSort of S = the ResultSort of S +* the ResultSort of S ) ;
hence S +* S = ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) by Def2; :: thesis: verum