set A = NFAlgebra R;
the Sorts of (NFAlgebra R) = NForms R by Def20;
hence the Sorts of (NFAlgebra R) is ManySortedSubset of the Sorts of (Free (S,X)) ; :: according to MSAFREE4:def 6 :: thesis: verum