theorem :: ORDERS_5:55

for A being non empty set
for D being non empty a_partition of A
for f being finite-support Function of A,REAL st f is nonnegative-yielding holds
(proj D) .: (support f) = support (D eqSumOf f)