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 #)
A1: the carrier' of S = the carrier' of S \/ the carrier' of S ;
A2: the Arity of S = the Arity of S +* the Arity of S ;
A3: the ResultSort of S = the ResultSort of S +* the ResultSort of S ;
the carrier of S = the carrier of S \/ the carrier of S ;
hence S +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) by A1, A2, A3, Def2; :: thesis: verum