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
proof
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;
hence not MSAlg_set (S,A) is empty by Def2; :: thesis: verum