set X = MSS_set A;
consider a being Element of A;
( dom ({a} --> a) = {a} & rng ({a} --> a) c= {a} ) by FUNCOP_1:19;
then reconsider g = {a} --> a as Function of {a},{a} by FUNCT_2:4;
a in {a} by TARSKI:def 1;
then <*a*> in {a} * by FUNCT_7:20;
then reconsider f = {a} --> <*a*> as Function of {a},({a} *) by FUNCOP_1:58;
A1: {a} c= A by ZFMISC_1:37;
ManySortedSign(# {a},{a},f,g #) in MSS_set A

proof

set SI = ManySortedSign(# {a},{a},f,g #);
( not ManySortedSign(# {a},{a},f,g #) is void & not ManySortedSign(# {a},{a},f,g #) is empty ) ;
hence ManySortedSign(# {a},{a},f,g #) in MSS_set A by A1, Def9; :: thesis: verum

end;

hence not MSS_set A is empty ; :: thesis: MSS_set A is MSS-membered
thus MSS_set A is MSS-membered :: thesis: verum

proof

let x be set ; :: according to MSALIMIT:def 7 :: thesis: ( x in MSS_set A implies x is non empty non void strict ManySortedSign )
assume x in MSS_set A ; :: thesis: x is non empty non void strict ManySortedSign
then ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) by Def9;
hence x is non empty non void strict ManySortedSign ; :: thesis: verum

end;