let X be Function; :: thesis: ( X is empty implies X is disjoint_valued )
assume A1: X is empty ; :: thesis: X is disjoint_valued
X is disjoint_valued

proof

let x, y be set ; :: 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 by XBOOLE_1:65; :: thesis: verum

end;

hence X is disjoint_valued ; :: thesis: verum