theorem Th67: :: ORDERS_5:56

for A being Preorder
for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
(proj A) .: (support f) = support (eqSumOf f)