set v = the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));

take A = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #); :: thesis: A is X,S -terms

thus the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) :: according to MSAFREE4:def 6 :: thesis: verum

take A = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #); :: thesis: A is X,S -terms

thus the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) :: according to MSAFREE4:def 6 :: thesis: verum

proof end;