consider a being Element of A;
dom (the carrier of S --> {a}) = the carrier of S by FUNCOP_1:19;
then reconsider f = the carrier of S --> {a} as ManySortedSet of the carrier of S by PARTFUN1:def 4;
consider Ch being ManySortedFunction of (f # ) * the Arity of S,f * the ResultSort of S;
set Ex = MSAlgebra(# f,Ch #);
reconsider Ex = MSAlgebra(# f,Ch #) as non-empty MSAlgebra of S by MSUALG_1:def 8;
reconsider Ex = Ex as strict feasible MSAlgebra of 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 set st
( i in the carrier of S & C = the Sorts of Ex . i ) by PBOOLE:150;
then C = {a} by FUNCOP_1:13;
hence C c= A by ZFMISC_1:37; :: thesis: verum

end;

hence not MSAlg_set S,A is empty by Def2; :: thesis: verum