let x be set ; :: thesis: for S being non empty ManySortedSign st x in the carrier of S holds
(SingleMSS x) +* S = ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #)
let S be non empty ManySortedSign ; :: thesis: ( x in the carrier of S implies (SingleMSS x) +* S = ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) )
set T = (SingleMSS x) +* S;
assume x in the carrier of S ; :: thesis: (SingleMSS x) +* S = ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #)
then {x} c= the carrier of S by ZFMISC_1:37;
then A1: ( {x} \/ the carrier of S = the carrier of S & {} \/ the carrier' of S = the carrier' of S ) by XBOOLE_1:12;
A2: ( the carrier of (SingleMSS x) = {x} & the carrier' of (SingleMSS x) = {} ) by Def1;
( the ResultSort of (SingleMSS x) = {} & the Arity of (SingleMSS x) = {} & {} +* the ResultSort of S = the ResultSort of S & {} +* the Arity of S = the Arity of S ) by FUNCT_4:21;
then ( the carrier of ((SingleMSS x) +* S) = the carrier of S & the carrier' of ((SingleMSS x) +* S) = the carrier' of S & the ResultSort of ((SingleMSS x) +* S) = the ResultSort of S & the Arity of ((SingleMSS x) +* S) = the Arity of S ) by A1, A2, CIRCCOMB:def 2;
hence (SingleMSS x) +* S = ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) ; :: thesis: verum