set A = the non-empty disjoint_valued MSAlgebra over S;
set v = the ManySortedMSSet of the Sorts of the non-empty disjoint_valued MSAlgebra over S, the Sorts of the non-empty disjoint_valued MSAlgebra over S;
take V = VarMSAlgebra(# the Sorts of the non-empty disjoint_valued MSAlgebra over S, the Charact of the non-empty disjoint_valued MSAlgebra over S, the ManySortedMSSet of the Sorts of the non-empty disjoint_valued MSAlgebra over S, the Sorts of the non-empty disjoint_valued MSAlgebra over S #); :: thesis: ( V is non-empty & V is disjoint_valued )
thus the Sorts of V is V2() ; :: according to MSUALG_1:def 3 :: thesis: V is disjoint_valued
thus the Sorts of V is disjoint_valued ; :: according to MSAFREE1:def 2 :: thesis: verum