theorem Th61: :: ORDERS_5:50

for A being Order
for f being finite-support Function of A,REAL holds (eqSumOf f) * (proj A) = f