let X be ManySortedSet of {} ; :: thesis: X = {}
dom X = {} by PARTFUN1:def 2;
hence X = {} by RELAT_1:41; :: thesis: verum