let X be ManySortedSubset of T; :: thesis: X is disjoint_valued
let x, y be object ; :: according to PROB_2:def 2 :: thesis: ( x = y or X . x misses X . y )
assume A1: x <> y ; :: thesis: X . x misses X . y
( ( x in S or x nin S ) & ( y in S or y nin S ) & X c= T & dom X = S ) by PBOOLE:def 18, PARTFUN1:def 2;
then ( ( X . x c= T . x or X . x = {} ) & ( X . y c= T . y or X . y = {} ) ) by FUNCT_1:def 2;
hence X . x misses X . y by A1, PROB_2:def 2, XBOOLE_1:64; :: thesis: verum