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

thus MSS_set A is MSS-membered :: thesis: verum

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

hence
not MSS_set A is empty
; :: thesis: MSS_set A is MSS-membered
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;( 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

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;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