set X = MSS_set A;
set a = the Element of A;
( dom ({ the Element of A} --> the Element of A) = { the Element of A} & rng ({ the Element of A} --> the Element of A) c= { the Element of A} ) by FUNCOP_1:13;
then reconsider g = { the Element of A} --> the Element of A as Function of { the Element of A},{ the Element of A} by FUNCT_2:2;
the Element of A in { the Element of A} by TARSKI:def 1;
then <* the Element of A*> in { the Element of A} * by FUNCT_7:18;
then reconsider f = { the Element of A} --> <* the Element of A*> as Function of { the Element of A},({ the Element of A} *) by FUNCOP_1:46;
A1: { the Element of A} c= A by ZFMISC_1:31;
ManySortedSign(# { the Element of A},{ the Element of A},f,g #) in MSS_set A

proof

set SI = ManySortedSign(# { the Element of A},{ the Element of A},f,g #);
( not ManySortedSign(# { the Element of A},{ the Element of A},f,g #) is void & not ManySortedSign(# { the Element of A},{ the Element of A},f,g #) is empty ) ;
hence ManySortedSign(# { the Element of A},{ the Element of A},f,g #) in MSS_set A by A1, Def8; :: 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 Def8;
hence x is non empty non void strict ManySortedSign ; :: thesis: verum

end;