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