set X = the non-empty ManySortedSet of the carrier of S;
set O = the ManySortedFunction of ( the non-empty ManySortedSet of the carrier of S #) * the Arity of S, the non-empty ManySortedSet of the carrier of S * the ResultSort of S;
set f = the ManySortedMSSet of the non-empty ManySortedSet of the carrier of S, the non-empty ManySortedSet of the carrier of S;
take VarMSAlgebra(# the non-empty ManySortedSet of the carrier of S, the ManySortedFunction of ( the non-empty ManySortedSet of the carrier of S #) * the Arity of S, the non-empty ManySortedSet of the carrier of S * the ResultSort of S, the ManySortedMSSet of the non-empty ManySortedSet of the carrier of S, the non-empty ManySortedSet of the carrier of S #) ; :: thesis: VarMSAlgebra(# the non-empty ManySortedSet of the carrier of S, the ManySortedFunction of ( the non-empty ManySortedSet of the carrier of S #) * the Arity of S, the non-empty ManySortedSet of the carrier of S * the ResultSort of S, the ManySortedMSSet of the non-empty ManySortedSet of the carrier of S, the non-empty ManySortedSet of the carrier of S #) is non-empty
thus VarMSAlgebra(# the non-empty ManySortedSet of the carrier of S, the ManySortedFunction of ( the non-empty ManySortedSet of the carrier of S #) * the Arity of S, the non-empty ManySortedSet of the carrier of S * the ResultSort of S, the ManySortedMSSet of the non-empty ManySortedSet of the carrier of S, the non-empty ManySortedSet of the carrier of S #) is non-empty ; :: thesis: verum