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:31;
then A1: {x} \/ the carrier of S = the carrier of S by XBOOLE_1:12;
A2: {} \/ the carrier' of S = the carrier' of S ;
A3: the carrier of (SingleMSS x) = {x} by Def1;
A4: the ResultSort of (SingleMSS x) = {} ;
A5: the Arity of (SingleMSS x) = {} ;
A6: {} +* the ResultSort of S = the ResultSort of S ;
A7: {} +* the Arity of S = the Arity of S ;
A8: the carrier of ((SingleMSS x) +* S) = the carrier of S by A1, A3, CIRCCOMB:def 2;
A9: the carrier' of ((SingleMSS x) +* S) = the carrier' of S by A2, A4, CIRCCOMB:def 2;
the ResultSort of ((SingleMSS x) +* S) = the ResultSort of S by A4, A6, CIRCCOMB:def 2;
hence (SingleMSS x) +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) by A5, A7, A8, A9, CIRCCOMB:def 2; :: thesis: verum