set a = the Element of A;

reconsider f = the carrier of S --> { the Element of A} as ManySortedSet of the carrier of S ;

set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S;

set Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #);

reconsider Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) as non-empty MSAlgebra over S by MSUALG_1:def 3;

reconsider Ex = Ex as strict feasible MSAlgebra over S ;

for C being Component of the Sorts of Ex holds C c= A

reconsider f = the carrier of S --> { the Element of A} as ManySortedSet of the carrier of S ;

set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S;

set Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #);

reconsider Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) as non-empty MSAlgebra over S by MSUALG_1:def 3;

reconsider Ex = Ex as strict feasible MSAlgebra over S ;

for C being Component of the Sorts of Ex holds C c= A

proof

hence
not MSAlg_set (S,A) is empty
by Def2; :: thesis: verum
let C be Component of the Sorts of Ex; :: thesis: C c= A

ex i being object st

( i in the carrier of S & C = the Sorts of Ex . i ) by PBOOLE:138;

then C = { the Element of A} by FUNCOP_1:7;

hence C c= A by ZFMISC_1:31; :: thesis: verum

end;ex i being object st

( i in the carrier of S & C = the Sorts of Ex . i ) by PBOOLE:138;

then C = { the Element of A} by FUNCOP_1:7;

hence C c= A by ZFMISC_1:31; :: thesis: verum