:: deftheorem defines disjoint_valued PROB_3:def 4 :
for X being set
for A1 being SetSequence of X holds
( A1 is disjoint_valued iff for m, n being Nat st m <> n holds
A1 . m misses A1 . n );