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