theorem :: MEASURE9:33

for X being non empty set
for F being FinSequence of X
for G being Function of NAT,X st ( for i being Nat holds F . i = G . i ) holds
( F is disjoint_valued iff G is disjoint_valued )