let M be ManySortedSet of ; :: 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 set ; :: according to PROB_2:def 3 :: 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

then ( M . x is empty & M . y is empty ) by A1, FUNCT_1:def 14;
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 4;
hence M . x misses M . y by XBOOLE_1:65; :: thesis: verum

end;

end;