:: deftheorem Def21 defines disjoint_valued POLNOT_1:def 13 :
for X, Y being set
for F being PartFunc of X,(bool Y) holds
( F is disjoint_valued iff for a, b being object st a in dom F & b in dom F & a <> b holds
F . a misses F . b );