:: deftheorem defines disjoint_valued PROB_2:def 2 :
for F being Function holds
( F is disjoint_valued iff for x, y being object st x <> y holds
F . x misses F . y );