let X be Function; :: thesis: ( X is empty implies X is disjoint_valued )
assume A1: X is empty ; :: 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 x <> y ; :: thesis: X . x misses X . y
X . x = {} by A1, FUNCT_1:def 2, RELAT_1:38;
hence X . x misses X . y ; :: thesis: verum