let f be ManySortedSet of X; :: thesis: f is finite-support
( support f c= dom f & dom f = X ) by Th36, PARTFUN1:def 2;
hence support f is finite ; :: according to PRE_POLY:def 8 :: thesis: verum