reconsider f = the carrier of S --> {0 } as ManySortedSet of ;
consider Ch being ManySortedFunction of (f # ) * the Arity of S,f * the ResultSort of S;
take MSAlgebra(# f,Ch #) ; :: thesis: the Sorts of MSAlgebra(# f,Ch #) = the carrier of S --> {0 }
thus the Sorts of MSAlgebra(# f,Ch #) = the carrier of S --> {0 } ; :: thesis: verum