let M be ManySortedSet of I; :: thesis: ( M is empty-yielding implies M is disjoint_valued )
assume A1: M is empty-yielding ; :: thesis: M is disjoint_valued
let x, y be object ; :: according to PROB_2:def 2 :: thesis: ( x = y or M . x misses M . y )
assume x <> y ; :: thesis: M . x misses M . y

per cases ( ( x in dom M & y in dom M ) or not x in dom M or not y in dom M ) ;

suppose ( x in dom M & y in dom M ) ; :: thesis: M . x misses M . y

M . x is empty by A1;
hence M . x misses M . y by XBOOLE_1:65; :: thesis: verum

end;

suppose ( not x in dom M or not y in dom M ) ; :: thesis: M . x misses M . y

then ( M . x = {} or M . y = {} ) by FUNCT_1:def 2;
hence M . x misses M . y by XBOOLE_1:65; :: thesis: verum

end;

end;