theorem Th65: :: ORDERS_5:54

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