for X being set
for F being FinSequence of X holds
( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j )