let f be ManySortedSet of X; :: thesis: f is finite-support
( support f c= dom f & dom f = X ) by Th41, PBOOLE:def 3;
hence support f is finite ; :: according to POLYNOM1:def 8 :: thesis: verum