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